diff --git a/ir/function.cpp b/ir/function.cpp
index fb1c1085d..9883e66e3 100644
--- a/ir/function.cpp
+++ b/ir/function.cpp
@@ -3,6 +3,8 @@
 
 #include "ir/function.h"
 #include "ir/instr.h"
+#include "ir/type.h"
+#include "util/config.h"
 #include "util/errors.h"
 #include "util/hash.h"
 #include "util/sort.h"
@@ -168,9 +170,14 @@ expr Function::getTypeConstraints() const {
       t &= v.getTypeConstraints();
     }
   }
+
   return t;
 }
 
+expr Function::getVScaleExpr() const {
+  return VectorType::getVScaleVar();
+}
+
 void Function::rauw(const Value &what, Value &with) {
   for (auto bb : getBBs())
     bb->rauw(what, with);
diff --git a/ir/function.h b/ir/function.h
index 3f840f866..0d04202bb 100644
--- a/ir/function.h
+++ b/ir/function.h
@@ -183,6 +183,7 @@ class Function final {
   bool hasReturn() const;
   unsigned bitsPointers() const { return bits_pointers; }
   unsigned bitsPtrOffset() const { return bits_ptr_offset; }
+  smt::expr getVScaleExpr() const;
   bool isLittleEndian() const { return little_endian; }
   bool isVarArgs() const { return is_var_args; }
 
diff --git a/ir/instr.cpp b/ir/instr.cpp
index 7dab68ab0..22bbb5ad7 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -974,6 +974,35 @@ unique_ptr<Instr> FpBinOp::dup(Function &f, const string &suffix) const {
 }
 
 
+vector<Value*> VScale::operands() const {
+  return {};
+}
+
+bool VScale::propagatesPoison() const { return false; }
+
+bool VScale::hasSideEffects() const { return false; }
+
+void VScale::rauw(const Value &what, Value &with) {}
+
+void VScale::print(ostream &os) const {
+  os << getName() << " = vscale";
+}
+
+StateValue VScale::toSMT(State &s) const {
+  auto e = s.getFn().getVScaleExpr();
+  return { e.zextOrTrunc(bits()), true };
+}
+
+expr VScale::getTypeConstraints(const Function &f) const {
+  return Value::getTypeConstraints() &&
+         getType().enforceIntType();
+}
+
+unique_ptr<Instr> VScale::dup(Function &f, const string &suffix) const {
+  return make_unique<VScale>(getType(), getName() + suffix);
+}
+
+
 vector<Value*> UnaryOp::operands() const {
   return { val };
 }
diff --git a/ir/instr.h b/ir/instr.h
index ed2f3bf5c..bca96c081 100644
--- a/ir/instr.h
+++ b/ir/instr.h
@@ -102,6 +102,23 @@ class FpBinOp final : public Instr {
 };
 
 
+class VScale final : public Instr {
+public:
+  VScale(Type &type, std::string &&name)
+    : Instr(type, std::move(name)) {}
+
+  std::vector<Value*> operands() const override;
+  bool propagatesPoison() const override;
+  bool hasSideEffects() const override;
+  void rauw(const Value &what, Value &with) override;
+  void print(std::ostream &os) const override;
+  StateValue toSMT(State &s) const override;
+  smt::expr getTypeConstraints(const Function &f) const override;
+  std::unique_ptr<Instr>
+    dup(Function &f, const std::string &suffix) const override;
+};
+
+
 class UnaryOp final : public Instr {
 public:
   enum Op {
diff --git a/ir/type.cpp b/ir/type.cpp
index 720ca44d6..d80b5c039 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -6,6 +6,7 @@
 #include "ir/state.h"
 #include "smt/solver.h"
 #include "util/compiler.h"
+#include "util/config.h"
 #include <array>
 #include <cassert>
 #include <numeric>
@@ -1089,12 +1090,26 @@ void ArrayType::print(ostream &os) const {
 }
 
 
-VectorType::VectorType(string &&name, unsigned elements, Type &elementTy)
-  : AggregateType(std::move(name), false) {
-  assert(elements != 0);
-  this->elements = elements;
+expr VectorType::getVScaleVar() {
+  return expr::mkVar("vscale", var_vector_elements);
+}
+
+expr VectorType::vscale() const {
+  if (!scalable)
+    return expr::mkUInt(1, var_vector_elements);
+  return defined ? expr::mkUInt(vscale_value, var_vector_elements)
+                 : getVScaleVar();
+}
+
+VectorType::VectorType(string &&name, unsigned elems, Type &elTy, bool scal)
+  : AggregateType(std::move(name), false), scalable(scal), min_elements(elems),
+    vscale_value(scal ? util::config::vscale_value : 1) {
+  assert(elems != 0);
+  if (scalable)
+    elems *= vscale_value;
+  this->elements = elems;
   defined = true;
-  children.resize(elements, &elementTy);
+  children.resize(elements, &elTy);
   is_padding.resize(elements, false);
 }
 
@@ -1157,6 +1172,12 @@ expr VectorType::getTypeConstraints() const {
     r &= numElements().ugt(i).implies(elementTy == *children[i]);
   }
 
+  if (scalable && defined) {
+    r &= vscale() == expr::mkUInt(vscale_value, var_vector_elements);
+  } else if (scalable) {
+    r &= vscale().uge(expr::mkUInt(1, var_vector_elements));
+  }
+
   return r;
 }
 
@@ -1172,14 +1193,25 @@ bool VectorType::isVectorType() const {
   return true;
 }
 
+void VectorType::fixup(const Model &m) {
+  if (!defined && scalable)
+    vscale_value = m.getUInt(vscale());
+  AggregateType::fixup(m);
+}
+
 expr VectorType::enforceVectorType(
     const function<expr(const Type&)> &enforceElem) const {
   return enforceElem(*children[0]);
 }
 
 void VectorType::print(ostream &os) const {
-  if (elements)
-    os << '<' << elements << " x " << *children[0] << '>';
+  if (!elements)
+    return;
+  os << '<';
+  if (scalable) {
+    os << "vscale" << ":" << vscale_value << " x ";
+  }
+  os << min_elements << " x " << *children[0] << '>';
 }
 
 
diff --git a/ir/type.h b/ir/type.h
index d732490c6..2ace86fda 100644
--- a/ir/type.h
+++ b/ir/type.h
@@ -5,6 +5,7 @@
 
 #include "ir/attrs.h"
 #include "smt/expr.h"
+#include "util/config.h"
 
 #include <functional>
 #include <memory>
@@ -335,9 +336,19 @@ class ArrayType final : public AggregateType {
 
 
 class VectorType final : public AggregateType {
+private:
+  bool scalable = false;
+  unsigned min_elements, vscale_value;
+
 public:
+  smt::expr vscale() const;
+  static smt::expr getVScaleVar();
+
+  bool isScalable() const { return scalable; }
+  unsigned getMinElements() const { return min_elements; }
+
   VectorType(std::string &&name) : AggregateType(std::move(name)) {}
-  VectorType(std::string &&name, unsigned elements, Type &elementTy);
+  VectorType(std::string &&name, unsigned elems, Type &elemTy, bool scalable);
 
   IR::StateValue extract(const IR::StateValue &vector,
                          const smt::expr &index) const;
@@ -348,6 +359,7 @@ class VectorType final : public AggregateType {
   unsigned maxSubBitAccess() const override;
   smt::expr scalarSize() const override;
   bool isVectorType() const override;
+  void fixup(const smt::Model &m) override;
   smt::expr enforceVectorType(
     const std::function<smt::expr(const Type&)> &enforceElem) const override;
   void print(std::ostream &os) const override;
diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h
index fd4443bc6..4865f753e 100644
--- a/llvm_util/cmd_args_def.h
+++ b/llvm_util/cmd_args_def.h
@@ -24,6 +24,7 @@ config::debug = opt_debug;
 config::quiet = opt_quiet;
 config::max_offset_bits = opt_max_offset_in_bits;
 config::max_sizet_bits  = opt_max_sizet_in_bits;
+config::vscale_value = opt_vscale;
 
 if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) {
   config::disable_undef_input = true;
diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h
index b732ec92a..853deb6b1 100644
--- a/llvm_util/cmd_args_list.h
+++ b/llvm_util/cmd_args_list.h
@@ -185,4 +185,9 @@ 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_vscale(LLVM_ARGS_PREFIX "vscale",
+  llvm::cl::desc("Set vscale value for scalable vectors (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 307c6437f..da4b24b69 100644
--- a/llvm_util/llvm2alive.cpp
+++ b/llvm_util/llvm2alive.cpp
@@ -2,6 +2,7 @@
 // Distributed under the MIT license that can be found in the LICENSE file.
 
 #include "llvm_util/llvm2alive.h"
+#include "ir/type.h"
 #include "ir/x86_intrinsics.h"
 #include "llvm_util/known_fns.h"
 #include "llvm_util/utils.h"
@@ -1224,6 +1225,12 @@ 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);
+      return make_unique<VScale>(*ty, value_name(i));
+    }
 
     // do nothing intrinsics
     case llvm::Intrinsic::dbg_declare:
@@ -1335,8 +1342,17 @@ 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 = 1;
+    if (i.getType()->isScalableTy()) {
+      replicate = config::vscale_value;
+    }
+
+    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));
   }
diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp
index 604926f63..f440bc489 100644
--- a/llvm_util/utils.cpp
+++ b/llvm_util/utils.cpp
@@ -203,7 +203,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);
@@ -212,7 +213,7 @@ Type* llvm_type2alive(const llvm::Type *ty) {
       if (!ety || elems > 1024)
         return nullptr;
       cache = make_unique<VectorType>("ty_" + to_string(type_id_counter++),
-                                      elems, *ety);
+                                      elems, *ety, vty->isScalableTy());
     }
     return cache.get();
   }
diff --git a/tests/alive-tv/vector/scalable/insert-loop1.ll b/tests/alive-tv/vector/scalable/insert-loop1.ll
new file mode 100644
index 000000000..29d7d79c3
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/insert-loop1.ll
@@ -0,0 +1,29 @@
+define i32 @src() {
+  ret i32 1
+}
+
+define i32 @tgt() {
+entry:
+  %vs = call i32 @llvm.vscale.i32()
+  %len = mul i32 %vs, 2
+  %init_vec = insertelement <vscale x 2 x i32> poison, i32 0, i32 0
+  br label %for.cond
+
+for.cond:
+  %i = phi i32 [ 0, %entry ], [ %inc, %for.body ]
+  %vec = phi <vscale x 2 x i32> [ %init_vec, %entry ], [ %new_vec, %for.body ]
+  %cmp = icmp slt i32 %i, %len
+  br i1 %cmp, label %for.body, label %exit
+
+for.body:
+  %new_vec = insertelement <vscale x 2 x i32> %vec, i32 %i, i32 %i
+  %inc = add i32 %i, 1
+  br label %for.cond
+
+exit:
+  %last_idx = sub i32 %len, 1
+  %result = extractelement <vscale x 2 x i32> %vec, i32 %last_idx
+  ret i32 %result
+}
+
+; TEST-ARGS: --vscale=1 -tgt-unroll=2
diff --git a/tests/alive-tv/vector/scalable/insert-loop2.ll b/tests/alive-tv/vector/scalable/insert-loop2.ll
new file mode 100644
index 000000000..5358deb8a
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/insert-loop2.ll
@@ -0,0 +1,28 @@
+define i32 @src() {
+  ret i32 3
+}
+define i32 @tgt() {
+entry:
+  %vs = call i32 @llvm.vscale.i32()
+  %len = mul i32 %vs, 2
+  %init_vec = insertelement <vscale x 2 x i32> poison, i32 0, i32 0
+  br label %for.cond
+
+for.cond:
+  %i = phi i32 [ 0, %entry ], [ %inc, %for.body ]
+  %vec = phi <vscale x 2 x i32> [ %init_vec, %entry ], [ %new_vec, %for.body ]
+  %cmp = icmp slt i32 %i, %len
+  br i1 %cmp, label %for.body, label %exit
+
+for.body:
+  %new_vec = insertelement <vscale x 2 x i32> %vec, i32 %i, i32 %i
+  %inc = add i32 %i, 1
+  br label %for.cond
+
+exit:
+  %last_idx = sub i32 %len, 1
+  %result = extractelement <vscale x 2 x i32> %vec, i32 %last_idx
+  ret i32 %result
+}
+
+; TEST-ARGS: --vscale=2 -tgt-unroll=4
diff --git a/tests/alive-tv/vector/scalable/insert-loop3.ll b/tests/alive-tv/vector/scalable/insert-loop3.ll
new file mode 100644
index 000000000..7c5afca99
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/insert-loop3.ll
@@ -0,0 +1,28 @@
+define i32 @src() {
+  ret i32 5
+}
+define i32 @tgt() {
+entry:
+  %vs = call i32 @llvm.vscale.i32()
+  %len = mul i32 %vs, 2
+  %init_vec = insertelement <vscale x 2 x i32> poison, i32 0, i32 0
+  br label %for.cond
+
+for.cond:
+  %i = phi i32 [ 0, %entry ], [ %inc, %for.body ]
+  %vec = phi <vscale x 2 x i32> [ %init_vec, %entry ], [ %new_vec, %for.body ]
+  %cmp = icmp slt i32 %i, %len
+  br i1 %cmp, label %for.body, label %exit
+
+for.body:
+  %new_vec = insertelement <vscale x 2 x i32> %vec, i32 %i, i32 %i
+  %inc = add i32 %i, 1
+  br label %for.cond
+
+exit:
+  %last_idx = sub i32 %len, 1
+  %result = extractelement <vscale x 2 x i32> %vec, i32 %last_idx
+  ret i32 %result
+}
+
+; TEST-ARGS: --vscale=3 -tgt-unroll=6
diff --git a/tests/alive-tv/vector/scalable/shufflevector-poison1.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector-poison1.srctgt.ll
new file mode 100644
index 000000000..ef31ad7dc
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector-poison1.srctgt.ll
@@ -0,0 +1,11 @@
+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> poison
+  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> poison
+}
+
+; TEST-ARGS: --vscale=1
diff --git a/tests/alive-tv/vector/scalable/shufflevector-poison2.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector-poison2.srctgt.ll
new file mode 100644
index 000000000..318f7e737
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector-poison2.srctgt.ll
@@ -0,0 +1,11 @@
+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> poison
+  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> poison
+}
+
+; TEST-ARGS: --vscale=2
diff --git a/tests/alive-tv/vector/scalable/shufflevector-poison3.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector-poison3.srctgt.ll
new file mode 100644
index 000000000..0c7ea7b71
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector-poison3.srctgt.ll
@@ -0,0 +1,11 @@
+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> poison
+  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> poison
+}
+
+; TEST-ARGS: --vscale=3
diff --git a/tests/alive-tv/vector/scalable/shufflevector1.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector1.srctgt.ll
new file mode 100644
index 000000000..5511ebece
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector1.srctgt.ll
@@ -0,0 +1,11 @@
+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
+}
+
+; TEST-ARGS: --vscale=1
diff --git a/tests/alive-tv/vector/scalable/shufflevector2.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector2.srctgt.ll
new file mode 100644
index 000000000..1a1a8679c
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector2.srctgt.ll
@@ -0,0 +1,11 @@
+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
+}
+
+; TEST-ARGS: --vscale=2
diff --git a/tests/alive-tv/vector/scalable/shufflevector3.srctgt.ll b/tests/alive-tv/vector/scalable/shufflevector3.srctgt.ll
new file mode 100644
index 000000000..dd8307b55
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/shufflevector3.srctgt.ll
@@ -0,0 +1,11 @@
+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
+}
+
+; TEST-ARGS: --vscale=3
diff --git a/tests/alive-tv/vector/scalable/splat_with_insertelement1.srctgt.ll b/tests/alive-tv/vector/scalable/splat_with_insertelement1.srctgt.ll
new file mode 100644
index 000000000..409437536
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/splat_with_insertelement1.srctgt.ll
@@ -0,0 +1,13 @@
+define <vscale x 2 x i32> @src(<vscale x 2 x i32> %vec, i32 %val) {
+  %vec1 = insertelement <vscale x 2 x i32> %vec, i32 0, i32 0
+  %vec2 = insertelement <vscale x 2 x i32> %vec1, i32 0, i32 1
+  %vec3 = insertelement <vscale x 2 x i32> %vec2, i32 0, i32 2
+  %result = insertelement <vscale x 2 x i32> %vec3, i32 0, i32 3
+  ret <vscale x 2 x i32> %result
+}
+
+define <vscale x 2 x i32> @tgt(<vscale x 2 x i32> %vec, i32 %val) {
+  ret <vscale x 2 x i32> poison
+}
+
+; TEST-ARGS: --vscale=1
diff --git a/tests/alive-tv/vector/scalable/splat_with_insertelement2.srctgt.ll b/tests/alive-tv/vector/scalable/splat_with_insertelement2.srctgt.ll
new file mode 100644
index 000000000..08556c098
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/splat_with_insertelement2.srctgt.ll
@@ -0,0 +1,13 @@
+define <vscale x 2 x i32> @src(<vscale x 2 x i32> %vec, i32 %val) {
+  %vec1 = insertelement <vscale x 2 x i32> %vec, i32 0, i32 0
+  %vec2 = insertelement <vscale x 2 x i32> %vec1, i32 0, i32 1
+  %vec3 = insertelement <vscale x 2 x i32> %vec2, i32 0, i32 2
+  %result = insertelement <vscale x 2 x i32> %vec3, i32 0, i32 3
+  ret <vscale x 2 x i32> %result
+}
+
+define <vscale x 2 x i32> @tgt(<vscale x 2 x i32> %vec, i32 %val) {
+  ret <vscale x 2 x i32> zeroinitializer
+}
+
+; TEST-ARGS: --vscale=2
diff --git a/tests/alive-tv/vector/scalable/splat_with_insertelement3.srctgt.ll b/tests/alive-tv/vector/scalable/splat_with_insertelement3.srctgt.ll
new file mode 100644
index 000000000..69fcea4ed
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/splat_with_insertelement3.srctgt.ll
@@ -0,0 +1,14 @@
+define <vscale x 2 x i32> @src(<vscale x 2 x i32> %vec, i32 %val) {
+  %vec1 = insertelement <vscale x 2 x i32> %vec, i32 0, i32 0
+  %vec2 = insertelement <vscale x 2 x i32> %vec1, i32 0, i32 1
+  %vec3 = insertelement <vscale x 2 x i32> %vec2, i32 0, i32 2
+  %result = insertelement <vscale x 2 x i32> %vec3, i32 0, i32 3
+  ret <vscale x 2 x i32> %result
+}
+
+define <vscale x 2 x i32> @tgt(<vscale x 2 x i32> %vec, i32 %val) {
+  ret <vscale x 2 x i32> zeroinitializer
+}
+
+; TEST-ARGS: --vscale=3
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-1.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-1.srctgt.ll
new file mode 100644
index 000000000..a137f0342
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-1.srctgt.ll
@@ -0,0 +1,13 @@
+declare i32 @llvm.vscale.i32()
+
+define i32 @src() {
+  %v = call i32 @llvm.vscale.i32()
+  ret i32 %v
+}
+
+define i32 @tgt() {
+  ret i32 1
+}
+
+
+; TEST-ARGS: --vscale=1
diff --git a/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-2.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-2.srctgt.ll
new file mode 100644
index 000000000..396ec367c
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-2.srctgt.ll
@@ -0,0 +1,13 @@
+declare i32 @llvm.vscale.i32()
+
+define i32 @src() {
+  %v = call i32 @llvm.vscale.i32()
+  ret i32 %v
+}
+
+define i32 @tgt() {
+  ret i32 2
+}
+
+
+; TEST-ARGS: --vscale=2
diff --git a/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-3.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-3.srctgt.ll
new file mode 100644
index 000000000..1911e0c92
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i32-intrinsic-3.srctgt.ll
@@ -0,0 +1,13 @@
+declare i32 @llvm.vscale.i32()
+
+define i32 @src() {
+  %v = call i32 @llvm.vscale.i32()
+  ret i32 %v
+}
+
+define i32 @tgt() {
+  ret i32 3
+}
+
+
+; TEST-ARGS: --vscale=3
diff --git a/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-1.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-1.srctgt.ll
new file mode 100644
index 000000000..6b51c8c30
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-1.srctgt.ll
@@ -0,0 +1,13 @@
+declare i64 @llvm.vscale.i64()
+
+define i64 @src() {
+  %v = call i64 @llvm.vscale.i64()
+  ret i64 %v
+}
+
+define i64 @tgt() {
+  ret i64 1
+}
+
+
+; TEST-ARGS: --vscale=1
diff --git a/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-2.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-2.srctgt.ll
new file mode 100644
index 000000000..919f9717c
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-2.srctgt.ll
@@ -0,0 +1,13 @@
+declare i64 @llvm.vscale.i64()
+
+define i64 @src() {
+  %v = call i64 @llvm.vscale.i64()
+  ret i64 %v
+}
+
+define i64 @tgt() {
+  ret i64 2
+}
+
+
+; TEST-ARGS: --vscale=2
diff --git a/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-3.srctgt.ll b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-3.srctgt.ll
new file mode 100644
index 000000000..7a8b68805
--- /dev/null
+++ b/tests/alive-tv/vector/scalable/vscale-i64-intrinsic-3.srctgt.ll
@@ -0,0 +1,13 @@
+declare i64 @llvm.vscale.i64()
+
+define i64 @src() {
+  %v = call i64 @llvm.vscale.i64()
+  ret i64 %v
+}
+
+define i64 @tgt() {
+  ret i64 3
+}
+
+
+; TEST-ARGS: --vscale=3
diff --git a/tests/unit/vector/scalablevector1.opt b/tests/unit/vector/scalablevector1.opt
new file mode 100644
index 000000000..fdfa22135
--- /dev/null
+++ b/tests/unit/vector/scalablevector1.opt
@@ -0,0 +1,76 @@
+Name: scalable vector add - identity
+%r = add <vscale x 2 x i4> %a, %b
+  =>
+%r = add <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector add - commutative
+%r = add <vscale x 2 x i4> %a, %b
+  =>
+%r = add <vscale x 2 x i4> %b, %a
+
+
+Name: scalable vector mul - identity
+%r = mul <vscale x 2 x i4> %a, %b
+  =>
+%r = mul <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector mul - commutative
+%r = mul <vscale x 2 x i4> %a, %b
+  =>
+%r = mul <vscale x 2 x i4> %b, %a
+
+
+Name: scalable vector extract - identity
+%r = extractelement <vscale x 2 x i4> %vec, i32 %idx
+  =>
+%r = extractelement <vscale x 2 x i4> %vec, i32 %idx
+
+
+Name: scalable vector insert - identity
+%r = insertelement <vscale x 2 x i4> %vec, i4 %val, i32 %idx
+  =>
+%r = insertelement <vscale x 2 x i4> %vec, i4 %val, i32 %idx
+
+
+Name: scalable vector sub - identity
+%r = sub <vscale x 2 x i4> %a, %b
+  =>
+%r = sub <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector and - identity
+%r = and <vscale x 2 x i4> %a, %b
+  =>
+%r = and <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector or - identity
+%r = or <vscale x 2 x i4> %a, %b
+  =>
+%r = or <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector xor - identity
+%r = xor <vscale x 2 x i4> %a, %b
+  =>
+%r = xor <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector shl - identity
+%r = shl <vscale x 2 x i4> %a, %b
+  =>
+%r = shl <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector lshr - identity
+%r = lshr <vscale x 2 x i4> %a, %b
+  =>
+%r = lshr <vscale x 2 x i4> %a, %b
+
+
+Name: scalable vector ashr - identity
+%r = ashr <vscale x 2 x i4> %a, %b
+  =>
+%r = ashr <vscale x 2 x i4> %a, %b
diff --git a/tests/unit/vector/scalablevector2.opt b/tests/unit/vector/scalablevector2.opt
new file mode 100644
index 000000000..adec151c2
--- /dev/null
+++ b/tests/unit/vector/scalablevector2.opt
@@ -0,0 +1,15 @@
+; TEST-ARGS: -vscale:2
+Name: insert and extract on same location
+%t = insertelement <vscale x 2 x i4> %vec, i4 %x, i64 3
+%r = extractelement <vscale x 2 x i4> %t, i64 3
+  =>
+%r = i4 %x
+
+
+Name: insert and extract on different location
+%t = insertelement <vscale x 2 x i4> %vec, i4 %x, i64 3
+%r = extractelement <vscale x 2 x i4> %t, i64 0
+  =>
+%r = i4 %x
+
+; ERROR: Target is more poisonous than source for i4 %r
diff --git a/tools/alive.cpp b/tools/alive.cpp
index 1ca919f21..75fe31b0c 100644
--- a/tools/alive.cpp
+++ b/tools/alive.cpp
@@ -36,6 +36,7 @@ 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"
           " -h / --help / -v / --version\tShow this help\n";
 }
 
@@ -76,6 +77,8 @@ 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 == "-h" || arg == "--help" || arg == "-v" ||
              arg == "--version") {
       show_help();
diff --git a/tools/alive_lexer.re b/tools/alive_lexer.re
index 0b5784373..3d5ff35ce 100644
--- a/tools/alive_lexer.re
+++ b/tools/alive_lexer.re
@@ -105,9 +105,14 @@ space+ {
   return INT_TYPE;
 }
 
+"<vscale" space* "x" space* @tag1 [1-9][0-9]* space* "x" {
+  yylval.num = strtoull((char*)tag1, nullptr, 10);
+  return SCALABLE_VECTOR_TYPE_PREFIX;
+}
+
 "<" space* @tag1 [1-9][0-9]* space* "x" {
   yylval.num = strtoull((char*)tag1, nullptr, 10);
-  return VECTOR_TYPE_PREFIX;
+  return FIXED_VECTOR_TYPE_PREFIX;
 }
 
 "[" space* @tag1 [0-9]+ space* "x" {
diff --git a/tools/alive_parser.cpp b/tools/alive_parser.cpp
index a9ddb752e..83a2eb701 100644
--- a/tools/alive_parser.cpp
+++ b/tools/alive_parser.cpp
@@ -143,7 +143,7 @@ struct tokenizer_t {
   }
 
   bool isVectorType() {
-    return peek() == VECTOR_TYPE_PREFIX;
+    return peek() == FIXED_VECTOR_TYPE_PREFIX || peek() == SCALABLE_VECTOR_TYPE_PREFIX;
   }
 
   bool isArrayType() {
@@ -369,15 +369,17 @@ static Type& parse_scalar_type() {
 }
 
 static Type& parse_vector_type() {
-  tokenizer.ensure(VECTOR_TYPE_PREFIX);
-  unsigned elements = yylval.num;
+  bool scalable = tokenizer.consumeIf(SCALABLE_VECTOR_TYPE_PREFIX);
 
-  Type &elemTy = parse_scalar_type();
+  if (!scalable)
+    tokenizer.ensure(FIXED_VECTOR_TYPE_PREFIX);
 
+  unsigned elements = yylval.num;
+  Type &elemTy = parse_scalar_type();
   tokenizer.ensure(CSGT);
   return *vector_types.emplace_back(
     make_unique<VectorType>("vty_" + to_string(vector_types.size()),
-                            elements, elemTy)).get();
+                            elements, elemTy, scalable)).get();
 }
 
 static Type& parse_array_type();
@@ -1357,7 +1359,8 @@ static unique_ptr<Instr> parse_instr(string_view name) {
   case HALF:
   case FLOAT:
   case DOUBLE:
-  case VECTOR_TYPE_PREFIX:
+  case FIXED_VECTOR_TYPE_PREFIX:
+  case SCALABLE_VECTOR_TYPE_PREFIX:
   case LBRACE:
   case NUM:
   case FP_NUM:
diff --git a/tools/tokens.h b/tools/tokens.h
index aee48bbd2..8390c314c 100644
--- a/tools/tokens.h
+++ b/tools/tokens.h
@@ -168,7 +168,8 @@ TOKEN(UREM)
 TOKEN(USUB_OVERFLOW)
 TOKEN(USUB_SAT)
 TOKEN(USHL_SAT)
-TOKEN(VECTOR_TYPE_PREFIX)
+TOKEN(FIXED_VECTOR_TYPE_PREFIX)
+TOKEN(SCALABLE_VECTOR_TYPE_PREFIX)
 TOKEN(WRITE)
 TOKEN(XOR)
 TOKEN(ZEXT)
diff --git a/tools/transform.cpp b/tools/transform.cpp
index ee5810678..7a773d673 100644
--- a/tools/transform.cpp
+++ b/tools/transform.cpp
@@ -4,6 +4,7 @@
 #include "tools/transform.h"
 #include "ir/globals.h"
 #include "ir/state.h"
+#include "ir/type.h"
 #include "smt/expr.h"
 #include "smt/smt.h"
 #include "smt/solver.h"
@@ -1397,6 +1398,12 @@ pair<unique_ptr<State>, unique_ptr<State>> TransformVerify::exec() const {
 
   auto src_state = make_unique<State>(t.src, true);
   auto tgt_state = make_unique<State>(t.tgt, false);
+
+  if (config::vscale_value) {
+    auto vs = VectorType::getVScaleVar();
+    src_state->addPre(vs == expr::mkUInt(config::vscale_value, vs));
+  }
+
   sym_exec(*src_state);
   tgt_state->syncSEdataWithSrc(*src_state);
   src_state->cleanup();
diff --git a/util/config.cpp b/util/config.cpp
index 632b72561..41306c111 100644
--- a/util/config.cpp
+++ b/util/config.cpp
@@ -24,6 +24,7 @@ unsigned src_unroll_cnt = 0;
 unsigned tgt_unroll_cnt = 0;
 unsigned max_offset_bits = 64;
 unsigned max_sizet_bits = 64;
+unsigned vscale_value = 2;
 
 ostream &dbg() {
   return *debug_os;
diff --git a/util/config.h b/util/config.h
index 6cf2314ff..5b1baf468 100644
--- a/util/config.h
+++ b/util/config.h
@@ -46,6 +46,9 @@ extern unsigned max_offset_bits;
 // size and size of pointers (not to be confused with program pointer size).
 extern unsigned max_sizet_bits;
 
+// The vscale value for scalable vectors.
+extern unsigned vscale_value;
+
 std::ostream &dbg();
 void set_debug(std::ostream &os);