diff --git a/ir/type.cpp b/ir/type.cpp
index 66ee2588e..f6d7841ee 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -20,7 +20,8 @@ using namespace std;
 
 static constexpr unsigned var_type_bits = 3;
 static constexpr unsigned var_bw_bits = 11;
-static constexpr unsigned var_vector_elements = 16;
+static constexpr unsigned var_elements_bits = 16;
+static_assert(IR::max_vector_elements == (1u << var_elements_bits) - 1);
 
 
 namespace IR {
@@ -808,8 +809,8 @@ AggregateType::AggregateType(string &&name, vector<Type*> &&vchildren,
 }
 
 expr AggregateType::numElements() const {
-  return defined ? expr::mkUInt(elements, var_vector_elements) :
-                   var("elements", var_vector_elements);
+  return defined ? expr::mkUInt(elements, var_elements_bits) :
+                   var("elements", var_elements_bits);
 }
 
 unsigned AggregateType::numPaddingsConst() const {
diff --git a/ir/type.h b/ir/type.h
index 009ee5811..46eb9994f 100644
--- a/ir/type.h
+++ b/ir/type.h
@@ -18,6 +18,8 @@ namespace smt { class Model; }
 
 namespace IR {
 
+static constexpr unsigned max_vector_elements = 65535;
+
 class AggregateType;
 class FloatType;
 class IntType;
diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h
index fd4443bc6..5ecbee14b 100644
--- a/llvm_util/cmd_args_def.h
+++ b/llvm_util/cmd_args_def.h
@@ -1,6 +1,8 @@
 // Copyright (c) 2018-present The Alive2 Authors.
 // Distributed under the MIT license that can be found in the LICENSE file.
 
+#include <bit>
+
 #ifdef ARGS_SRC_TGT
 config::src_unroll_cnt = opt_src_unrolling_factor;
 config::tgt_unroll_cnt = opt_tgt_unrolling_factor;
@@ -25,6 +27,13 @@ config::quiet = opt_quiet;
 config::max_offset_bits = opt_max_offset_in_bits;
 config::max_sizet_bits  = opt_max_sizet_in_bits;
 
+if (!std::has_single_bit(opt_single_vscale)) {
+  cerr << "Alive2: " LLVM_ARGS_PREFIX
+          "single-vscale must be a positive power of two!" << endl;
+  exit(1);
+}
+config::vscale_value = opt_single_vscale;
+
 if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) {
   config::disable_undef_input = true;
   config::disable_poison_input = true;
diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h
index 49fbd01a5..efa5ccb16 100644
--- a/llvm_util/cmd_args_list.h
+++ b/llvm_util/cmd_args_list.h
@@ -185,4 +185,10 @@ llvm::cl::opt<bool> opt_disallow_ub_exploitation(
   llvm::cl::desc("Disallow UB exploitation by optimizations (default=allow)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
+llvm::cl::opt<unsigned> opt_single_vscale(LLVM_ARGS_PREFIX "single-vscale",
+  llvm::cl::desc("Check scalable vectors at this one concrete vscale, "
+                 "which must be a power of two (default=2)"),
+  llvm::cl::init(2), llvm::cl::value_desc("value"),
+  llvm::cl::cat(alive_cmdargs));
+
 }
diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp
index c79ddf3c1..e7d61a0dc 100644
--- a/llvm_util/llvm2alive.cpp
+++ b/llvm_util/llvm2alive.cpp
@@ -5,6 +5,7 @@
 #include "ir/x86_intrinsics.h"
 #include "llvm_util/known_fns.h"
 #include "llvm_util/utils.h"
+#include "util/config.h"
 #include "util/sort.h"
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Analysis/MemoryBuiltins.h"
@@ -604,7 +605,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
     }
 
     auto typesz = DL().getTypeAllocSize(i.getAllocatedType());
-    if (typesz.isScalable()) // TODO: scalable vectors not supported
+    // TODO: scalable alloca
+    if (typesz.isScalable())
       return error(i);
 
     auto size = make_intconst(typesz, 64);
@@ -640,7 +642,9 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
         auto ofs_ty = llvm::IntegerType::get(i.getContext(), 64);
 
         if (auto opvty = dyn_cast<llvm::VectorType>(opty)) {
-          assert(!isa<llvm::ScalableVectorType>(opvty));
+          // TODO: scalable splat struct indices
+          if (isa<llvm::ScalableVectorType>(opvty))
+            return error(i);
           vector<llvm::Constant *> offsets;
 
           for (unsigned i = 0; i < opvty->getElementCount().getKnownMinValue();
@@ -668,7 +672,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
         continue;
       }
 
-      gep->addIdx(I.getSequentialElementStride(DL()).getKnownMinValue(), *op);
+      auto stride = I.getSequentialElementStride(DL());
+      auto size = stride.getKnownMinValue();
+      if (stride.isScalable())
+        size *= uint64_t(config::vscale_value);
+      gep->addIdx(size, *op);
     }
     return gep;
   }
@@ -1235,6 +1243,21 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
       addNoundefAssumes(i, {a, b});
       return make_unique<VaCopy>(*a, *b);
     }
+    case llvm::Intrinsic::vscale: {
+      auto ty = llvm_type2alive(i.getType());
+      if (!ty)
+        return error(i);
+      llvm::Constant *constant;
+      if (ty->bits() < 32 && (config::vscale_value >> ty->bits()) != 0)
+        constant = llvm::PoisonValue::get(i.getType());
+      else
+        constant = llvm::ConstantInt::get(i.getType(), config::vscale_value);
+      auto val = get_operand(constant);
+      if (!val)
+        return error(i);
+      ret = make_unique<UnaryOp>(*ty, value_name(i), *val, UnaryOp::Copy);
+      break;
+    }
 
     // do nothing intrinsics
     case llvm::Intrinsic::dbg_declare:
@@ -1346,8 +1369,11 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
   RetTy visitShuffleVectorInst(llvm::ShuffleVectorInst &i) {
     PARSE_BINOP();
     vector<unsigned> mask;
-    for (auto m : i.getShuffleMask())
-      mask.push_back(m);
+
+    unsigned replicate = i.getType()->isScalableTy() ? config::vscale_value : 1;
+    auto sm = i.getShuffleMask();
+    for (unsigned j = 0; j < replicate; ++j)
+      mask.insert(mask.end(), sm.begin(), sm.end());
     return
       make_unique<ShuffleVector>(*ty, value_name(i), *a, *b, std::move(mask));
   }
@@ -1599,7 +1625,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
         attrs.set(ParamAttrs::ByVal);
         auto ty = aset.getByValType();
         auto asz = DL().getTypeAllocSize(ty);
-        attrs.blockSize = max(attrs.blockSize, asz.getKnownMinValue());
+        auto size = asz.getKnownMinValue();
+        if (asz.isScalable())
+          size *= uint64_t(config::vscale_value);
+        attrs.blockSize = max(attrs.blockSize, size);
 
         attrs.set(ParamAttrs::Align);
         attrs.align = max(attrs.align, DL().getABITypeAlign(ty).value());
diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp
index 502d388fe..5fd00268a 100644
--- a/llvm_util/utils.cpp
+++ b/llvm_util/utils.cpp
@@ -4,6 +4,8 @@
 #include "llvm_util/utils.h"
 #include "ir/constant.h"
 #include "ir/function.h"
+#include "ir/type.h"
+#include "util/config.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/DataLayout.h"
@@ -207,8 +209,8 @@ Type* llvm_type2alive(const llvm::Type *ty) {
     }
     return cache.get();
   }
-  // TODO: non-fixed sized vectors
-  case llvm::Type::FixedVectorTyID: {
+  case llvm::Type::FixedVectorTyID:
+  case llvm::Type::ScalableVectorTyID: {
     auto &cache = type_cache[ty];
     if (!cache) {
       auto vty = cast<llvm::VectorType>(ty);
@@ -216,8 +218,15 @@ Type* llvm_type2alive(const llvm::Type *ty) {
       auto ety = llvm_type2alive(vty->getElementType());
       if (!ety || elems > 1024)
         return nullptr;
+      uint64_t count = elems;
+      if (vty->isScalableTy())
+        count *= util::config::vscale_value;
+      if (!count || count > max_vector_elements) {
+        *out << "ERROR: Vector type is too large\n";
+        return nullptr;
+      }
       cache = make_unique<VectorType>("ty_" + to_string(type_id_counter++),
-                                      elems, *ety);
+                                      elems, *ety, vty->isScalableTy());
     }
     return cache.get();
   }
@@ -303,7 +312,7 @@ Value* get_operand(llvm::Value *v,
     return nullptr;
 
   // automatic splat of constant values
-  if (auto vty = dyn_cast<llvm::FixedVectorType>(v->getType());
+  if (auto vty = dyn_cast<llvm::VectorType>(v->getType());
       vty && isa<llvm::ConstantInt, llvm::ConstantFP>(v)) {
     llvm::Value *llvm_splat = nullptr;
     if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
@@ -320,7 +329,7 @@ Value* get_operand(llvm::Value *v,
     if (!splat)
       return nullptr;
 
-    vector<Value*> vals(vty->getNumElements(), splat);
+    vector<Value*> vals(ty->getAsAggregateType()->numElementsConst(), splat);
     auto val = make_unique<AggregateValue>(*ty, std::move(vals));
     auto ret = val.get();
     current_fn->addConstant(std::move(val));
diff --git a/tests/alive-tv/vector/scalable/byval-call.srctgt.ll b/tests/alive-tv/vector/scalable/byval-call.srctgt.ll
new file mode 100644
index 000000000..374f005eb
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/byval-call.srctgt.ll
@@ -0,0 +1,15 @@
+; TEST-ARGS: --single-vscale=2
+; CHECK: Transformation seems to be correct!
+; CHECK-NOT: ERROR:
+
+declare void @consume(ptr)
+
+define void @src(ptr %p) {
+  call void @consume(ptr byval(<vscale x 4 x i32>) %p)
+  ret void
+}
+
+define void @tgt(ptr %p) {
+  call void @consume(ptr byval([32 x i8]) align 16 %p)
+  ret void
+}
diff --git a/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll b/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll
new file mode 100644
index 000000000..db5ab9067
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/gep-stride.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --single-vscale=2
+; CHECK: Transformation seems to be correct!
+
+define ptr @src(ptr %p) {
+  %q = getelementptr <vscale x 2 x i32>, ptr %p, i64 1, i64 1
+  ret ptr %q
+}
+
+define ptr @tgt(ptr %p) {
+  %q = getelementptr i8, ptr %p, i64 20
+  ret ptr %q
+}
diff --git a/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll b/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll
new file mode 100644
index 000000000..36b0251dd
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/large-vector-cap.srctgt.ll
@@ -0,0 +1,11 @@
+; TEST-ARGS: --single-vscale=2048
+; SKIP-IDENTITY
+; ERROR: Vector type is too large
+
+define <vscale x 64 x i1> @src(<vscale x 64 x i1> %v) {
+  ret <vscale x 64 x i1> %v
+}
+
+define <vscale x 64 x i1> @tgt(<vscale x 64 x i1> %v) {
+  ret <vscale x 64 x i1> %v
+}
diff --git a/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll
new file mode 100644
index 000000000..d310ff079
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector-splat.srctgt.ll
@@ -0,0 +1,12 @@
+; TEST-ARGS: --single-vscale=4
+; CHECK: Transformation seems to be correct!
+
+define <vscale x 2 x i32> @src(<vscale x 2 x i32> %vec) {
+  %insert = insertelement <vscale x 2 x i32> %vec, i32 0, i32 0
+  %shuf = shufflevector <vscale x 2 x i32> %insert, <vscale x 2 x i32> poison, <vscale x 2 x i32> zeroinitializer
+  ret <vscale x 2 x i32> %shuf
+}
+
+define <vscale x 2 x i32> @tgt(<vscale x 2 x i32> %vec) {
+  ret <vscale x 2 x i32> zeroinitializer
+}
diff --git a/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll
new file mode 100644
index 000000000..d7aa4cbd0
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-intrinsic.srctgt.ll
@@ -0,0 +1,13 @@
+; TEST-ARGS: --single-vscale=4
+; CHECK: Transformation seems to be correct!
+
+declare i64 @llvm.vscale.i64()
+
+define i64 @src() {
+  %v = call i64 @llvm.vscale.i64()
+  ret i64 %v
+}
+
+define i64 @tgt() {
+  ret i64 4
+}
diff --git a/tests/unit/vector/scalablevector2.opt b/tests/unit/vector/scalablevector2.opt
index a9e76241b..6941b4a28 100644
--- a/tests/unit/vector/scalablevector2.opt
+++ b/tests/unit/vector/scalablevector2.opt
@@ -1,4 +1,4 @@
-; TEST-ARGS: -vscale:2
+; TEST-ARGS: -single-vscale:2
 ; CHECK: <vscale:2 x 2 x i4>
 ; CHECK: Transformation seems to be correct!
 
diff --git a/tests/unit/vector/scalablevector3.opt b/tests/unit/vector/scalablevector3.opt
index e4c49c840..0e862bd11 100644
--- a/tests/unit/vector/scalablevector3.opt
+++ b/tests/unit/vector/scalablevector3.opt
@@ -1,4 +1,4 @@
-; TEST-ARGS: -vscale:1
+; TEST-ARGS: -single-vscale:1
 ; CHECK: <vscale:1 x 2 x i4>
 ; ERROR: Target is more poisonous than source for i4 %r
 
diff --git a/tools/alive.cpp b/tools/alive.cpp
index 6d9a71dd1..4e3c20188 100644
--- a/tools/alive.cpp
+++ b/tools/alive.cpp
@@ -36,7 +36,8 @@ static void show_help() {
           " -skip-smt\t\tSkip all SMT queries\n"
           " -disable-poison-input\tAssume input variables can never be poison\n"
           " -disable-undef-input\tAssume input variables can never be undef\n"
-          " -vscale:x\t\tSet vscale value for scalable vectors (default: 1)\n"
+          " -single-vscale:x\tCheck scalable vectors at this one concrete vscale,\n"
+          "\t\t\ta power of two (default: 2)\n"
           " -h / --help / -v / --version\tShow this help\n";
 }
 
@@ -77,8 +78,15 @@ int main(int argc, char **argv) {
       config::disable_undef_input = true;
     else if (arg == "-disable-poison-input")
       config::disable_poison_input = true;
-    else if (arg.compare(0, 8, "-vscale:") == 0 && arg.size() > 8)
-      config::vscale_value = strtoul(arg.substr(8).data(), nullptr, 10);
+    else if (arg.compare(0, 15, "-single-vscale:") == 0 && arg.size() > 15) {
+      config::vscale_value = strtoul(arg.substr(15).data(), nullptr, 10);
+      if (config::vscale_value == 0 ||
+          (config::vscale_value & (config::vscale_value - 1)) != 0) {
+        cerr << "single-vscale must be a positive power of two!\n\n";
+        show_help();
+        return -1;
+      }
+    }
     else if (arg == "-h" || arg == "--help" || arg == "-v" ||
              arg == "--version") {
       show_help();
diff --git a/tools/alive_parser.cpp b/tools/alive_parser.cpp
index 0427504e4..dbf55a1ed 100644
--- a/tools/alive_parser.cpp
+++ b/tools/alive_parser.cpp
@@ -4,9 +4,11 @@
 #include "tools/alive_parser.h"
 #include "ir/constant.h"
 #include "ir/precondition.h"
+#include "ir/type.h"
 #include "ir/value.h"
 #include "tools/alive_lexer.h"
 #include "util/compiler.h"
+#include "util/config.h"
 #include <cassert>
 #include <memory>
 #include <unordered_map>
@@ -377,6 +379,15 @@ static Type& parse_vector_type() {
   unsigned elements = yylval.num;
   Type &elemTy = parse_scalar_type();
   tokenizer.ensure(CSGT);
+
+  uint64_t count = elements;
+  if (scalable)
+    count *= util::config::vscale_value;
+  if (count == 0 || count > max_vector_elements)
+    error("Vector type must have between 1 and " +
+          to_string(max_vector_elements) + " elements; got: " +
+          to_string(count));
+
   return *vector_types.emplace_back(
     make_unique<VectorType>("vty_" + to_string(vector_types.size()),
                             elements, elemTy, scalable)).get();