diff --git a/ir/instr.cpp b/ir/instr.cpp
index 7402326ba..c21903acd 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -19,6 +19,8 @@ using namespace smt;
 using namespace util;
 using namespace std;
 
+bool useApprox = false;
+
 #define RAUW(val)    \
   if (val == &what)  \
     val = &with
@@ -846,26 +848,50 @@ StateValue FpBinOp::toSMT(State &s) const {
 
   switch (op) {
   case FAdd:
-    fn = [](const expr &a, const expr &b, const expr &rm) {
-      return a.fadd(b, rm);
+    fn = [&s](const expr &a, const expr &b, const expr &rm) {
+      if (useApprox) {
+        expr fadd = expr::mkUF("fadd_appprox", {a, b}, a);
+        s.doesApproximation("fadd_approx", fadd);
+        return fadd;
+      } else {
+        return a.fadd(b, rm);
+      }
     };
     break;
 
   case FSub:
-    fn = [](const expr &a, const expr &b, const expr &rm) {
-      return a.fsub(b, rm);
+    fn = [&s](const expr &a, const expr &b, const expr &rm) {
+      if (useApprox) {
+        expr fsub = expr::mkUF("fsub_appprox", {a, b}, a);
+        s.doesApproximation("fsub_approx", fsub);
+        return fsub;
+      } else {
+        return a.fsub(b, rm);
+      }
     };
     break;
 
   case FMul:
-    fn = [](const expr &a, const expr &b, const expr &rm) {
-      return a.fmul(b, rm);
+    fn = [&s](const expr &a, const expr &b, const expr &rm) {
+      if (useApprox) {
+        expr fmul = expr::mkUF("fmul_appprox", {a, b}, a);
+        s.doesApproximation("fsub_approx", fmul);
+        return fmul;
+      } else {
+        return a.fmul(b, rm);
+      }
     };
     break;
 
   case FDiv:
-    fn = [](const expr &a, const expr &b, const expr &rm) {
-      return a.fdiv(b, rm);
+    fn = [&s](const expr &a, const expr &b, const expr &rm) {
+      if (useApprox) {
+        expr fdiv = expr::mkUF("fdiv_approx", {a, b}, a);
+        s.doesApproximation("fdiv_approx", fdiv);
+        return fdiv;
+      } else {
+        return a.fdiv(b, rm);
+      }
     };
     break;
 
@@ -881,28 +907,53 @@ StateValue FpBinOp::toSMT(State &s) const {
   case FMin:
   case FMax:
     fn = [&](const expr &a, const expr &b, const expr &rm) {
-      expr ndet = s.getFreshNondetVar("maxminnondet", true);
-      expr cmp = op == FMin ? a.fole(b) : a.foge(b);
-      return expr::mkIf(a.isNaN(), b,
-                        expr::mkIf(b.isNaN(), a,
-                                   expr::mkIf(a.foeq(b),
-                                              expr::mkIf(ndet, a, b),
-                                              expr::mkIf(cmp, a, b))));
+      if (useApprox) {
+        expr fm = op == FMin ? expr::mkUF("fmin_approx", {a, b}, a)
+                             : expr::mkUF("fmax_approx", {a, b}, a);
+        if (op == FMin)
+          s.doesApproximation("fmin_approx", fm);
+        else
+          s.doesApproximation("fmax_approx", fm);
+
+        return fm;
+      } else {
+        expr ndet = s.getFreshNondetVar("maxminnondet", true);
+        auto ndz =
+            expr::mkIf(ndet, expr::mkNumber("0", a), expr::mkNumber("-0", a));
+
+        expr z = a.isFPZero() && b.isFPZero();
+        expr cmp = op == FMin ? a.fole(b) : a.foge(b);
+        return expr::mkIf(
+            a.isNaN(), b,
+            expr::mkIf(b.isNaN(), a,
+                       expr::mkIf(z, ndz, expr::mkIf(cmp, a, b))));
+      }
     };
     break;
 
   case FMinimum:
   case FMaximum:
     fn = [&](const expr &a, const expr &b, const expr &rm) {
-      expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
-      expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
-      expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
-                                     : (a.isFPNegative() && b.isFPNegative());
-      expr e = expr::mkIf(a.isFPZero() && b.isFPZero(),
-                          expr::mkIf(neg_cond, zneg, zpos),
-                          expr::mkIf(cmp, a, b));
-
-      return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e));
+      if (useApprox) {
+        expr fm = op == FMinimum ? expr::mkUF("fminimum_approx", {a, b}, a)
+                                 : expr::mkUF("fmaximum_approx", {a, b}, a);
+        if (op == FMinimum)
+          s.doesApproximation("fminimum_approx", fm);
+        else
+          s.doesApproximation("fmaximum_approx", fm);
+
+        return fm;
+      } else {
+        expr zpos = expr::mkNumber("0", a), zneg = expr::mkNumber("-0", a);
+        expr cmp = (op == FMinimum) ? a.fole(b) : a.foge(b);
+        expr neg_cond = op == FMinimum ? (a.isFPNegative() || b.isFPNegative())
+                                       : (a.isFPNegative() && b.isFPNegative());
+        expr e =
+            expr::mkIf(a.isFPZero() && b.isFPZero(),
+                       expr::mkIf(neg_cond, zneg, zpos), expr::mkIf(cmp, a, b));
+
+        return expr::mkIf(a.isNaN(), a, expr::mkIf(b.isNaN(), b, e));
+      }
     };
     break;
 
@@ -4932,6 +4983,742 @@ unique_ptr<Instr> ShuffleVector::dup(Function &f, const string &suffix) const {
                                     *v1, *v2, mask);
 }
 
+vector<Value *> FakeShuffle::operands() const {
+  return {v1, v2, mask};
+}
+
+bool FakeShuffle::propagatesPoison() const {
+  return false;
+}
+
+bool FakeShuffle::hasSideEffects() const {
+  return false;
+}
+
+void FakeShuffle::rauw(const Value &what, Value &with) {
+  RAUW(v1);
+  RAUW(v2);
+  RAUW(mask);
+}
+
+void FakeShuffle::print(ostream &os) const {
+  os << getName() << " = fakesv " << *v1 << ", " << *v2 << ", " << *mask;
+}
+
+StateValue FakeShuffle::toSMT(State &s) const {
+  auto vty =
+      static_cast<const VectorType *>(v1->getType().getAsAggregateType());
+  auto mty = mask->getType().getAsAggregateType();
+  auto sz = vty->numElementsConst();
+  vector<StateValue> vals;
+
+  for (unsigned i = 0, e = mty->numElementsConst(); i != e; ++i) {
+    auto [m_v, m_p] = mty->extract(s[*mask], i);
+    expr bound = expr::mkUInt(sz, m_v);
+    expr idx = m_v.urem(bound);
+    auto [v1v, v1p] = vty->extract(s[*v1], idx);
+    auto [v2v, v2p] = vty->extract(s[*v2], idx);
+    expr v = expr::mkIf(m_v.ult(bound), v1v, v2v);
+    expr np = expr::mkIf(m_v.ult(bound), v1p, v2p);
+    expr inbounds = m_v.ult(expr::mkUInt(vty->numElementsConst() * 2, m_v));
+
+    vals.emplace_back(std::move(v), inbounds && np);
+  }
+
+  return getType().getAsAggregateType()->aggregateVals(vals);
+}
+
+expr FakeShuffle::getTypeConstraints(const Function &f) const {
+  return Value::getTypeConstraints() &&
+         getType().enforceVectorTypeSameChildTy(v1->getType()) &&
+         getType().getAsAggregateType()->numElements() ==
+             mask->getType().getAsAggregateType()->numElements() &&
+         v1->getType().enforceVectorType() && v1->getType() == v2->getType() &&
+         mask->getType().enforceVectorType();
+}
+
+unique_ptr<Instr> FakeShuffle::dup(Function &f, const string &suffix) const {
+  return make_unique<FakeShuffle>(getType(), getName() + suffix, *v1, *v2,
+                                  *mask);
+}
+
+vector<Value *> X86IntrinBinOp::operands() const {
+  return {a, b};
+}
+
+bool X86IntrinBinOp::propagatesPoison() const {
+  return true;
+}
+
+bool X86IntrinBinOp::hasSideEffects() const {
+  return false;
+}
+
+void X86IntrinBinOp::rauw(const Value &what, Value &with) {
+  RAUW(a);
+  RAUW(b);
+}
+
+string X86IntrinBinOp::getOpName(Op op) {
+  switch (op) {
+#define PROCESS(NAME, A, B, C, D, E, F)                                        \
+  case NAME:                                                                   \
+    return #NAME;
+#include "intrinsics_binop.h"
+#undef PROCESS
+  }
+  UNREACHABLE();
+}
+
+void X86IntrinBinOp::print(ostream &os) const {
+  os << getName() << " = " << getOpName(op) << " " << *a << ", " << *b;
+}
+
+StateValue X86IntrinBinOp::toSMT(State &s) const {
+  auto rty = getType().getAsAggregateType();
+  auto aty = a->getType().getAsAggregateType();
+  auto bty = b->getType().getAsAggregateType();
+  auto &av = s[*a];
+  auto &bv = s[*b];
+
+  switch (op) {
+  // shift by one variable
+  case x86_sse2_psrl_w:
+  case x86_sse2_psrl_d:
+  case x86_sse2_psrl_q:
+  case x86_avx2_psrl_w:
+  case x86_avx2_psrl_d:
+  case x86_avx2_psrl_q:
+  case x86_avx512_psrl_w_512:
+  case x86_avx512_psrl_d_512:
+  case x86_avx512_psrl_q_512:
+  case x86_sse2_psra_w:
+  case x86_sse2_psra_d:
+  case x86_avx2_psra_w:
+  case x86_avx2_psra_d:
+  case x86_avx512_psra_q_128:
+  case x86_avx512_psra_q_256:
+  case x86_avx512_psra_w_512:
+  case x86_avx512_psra_d_512:
+  case x86_avx512_psra_q_512:
+  case x86_sse2_psll_w:
+  case x86_sse2_psll_d:
+  case x86_sse2_psll_q:
+  case x86_avx2_psll_w:
+  case x86_avx2_psll_d:
+  case x86_avx2_psll_q:
+  case x86_avx512_psll_w_512:
+  case x86_avx512_psll_d_512:
+  case x86_avx512_psll_q_512: {
+    vector<StateValue> vals;
+    unsigned elem_bw = bty->getChild(0).bits();
+
+    expr shift_np = true;
+    expr shift_v;
+    // extract lower 64 bits from b
+    for (unsigned i = 0, e = 64 / elem_bw; i != e; ++i) {
+      StateValue vv = bty->extract(bv, i);
+      shift_v = (i == 0) ? vv.value : vv.value.concat(shift_v);
+      // if any elements in lower 64 bits is poison, the result is poison
+      shift_np &= vv.non_poison;
+    }
+    function<expr(const expr &, const expr &)> fn;
+    switch (op) {
+    case x86_sse2_psrl_w:
+    case x86_sse2_psrl_d:
+    case x86_sse2_psrl_q:
+    case x86_avx2_psrl_w:
+    case x86_avx2_psrl_d:
+    case x86_avx2_psrl_q:
+    case x86_avx512_psrl_w_512:
+    case x86_avx512_psrl_d_512:
+    case x86_avx512_psrl_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        return expr::mkIf(shift_v.uge(expr::mkUInt(elem_bw, 64)),
+                          expr::mkUInt(0, elem_bw), a.lshr(b));
+      };
+      break;
+    case x86_sse2_psra_w:
+    case x86_sse2_psra_d:
+    case x86_avx2_psra_w:
+    case x86_avx2_psra_d:
+    case x86_avx512_psra_q_128:
+    case x86_avx512_psra_q_256:
+    case x86_avx512_psra_w_512:
+    case x86_avx512_psra_d_512:
+    case x86_avx512_psra_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        return expr::mkIf(shift_v.uge(expr::mkUInt(elem_bw, 64)),
+                          expr::mkIf(a.isNegative(), expr::mkUInt(-1, elem_bw),
+                                     expr::mkUInt(0, elem_bw)),
+                          a.ashr(b));
+      };
+      break;
+    case x86_sse2_psll_w:
+    case x86_sse2_psll_d:
+    case x86_sse2_psll_q:
+    case x86_avx2_psll_w:
+    case x86_avx2_psll_d:
+    case x86_avx2_psll_q:
+    case x86_avx512_psll_w_512:
+    case x86_avx512_psll_d_512:
+    case x86_avx512_psll_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        return expr::mkIf(shift_v.uge(expr::mkUInt(elem_bw, 64)),
+                          expr::mkUInt(0, elem_bw), a << b);
+      };
+      break;
+    default:
+      UNREACHABLE();
+    }
+    for (unsigned i = 0, e = aty->numElementsConst(); i != e; ++i) {
+      auto ai = aty->extract(av, i);
+      expr shift = fn(ai.value, shift_v.trunc(elem_bw));
+      vals.emplace_back(std::move(shift), shift_np && ai.non_poison);
+    }
+    return rty->aggregateVals(vals);
+  }
+  // vertical
+  case x86_sse2_pavg_w:
+  case x86_sse2_pavg_b:
+  case x86_avx2_pavg_w:
+  case x86_avx2_pavg_b:
+  case x86_avx512_pavg_w_512:
+  case x86_avx512_pavg_b_512:
+  case x86_ssse3_psign_b_128:
+  case x86_ssse3_psign_w_128:
+  case x86_ssse3_psign_d_128:
+  case x86_avx2_psign_b:
+  case x86_avx2_psign_w:
+  case x86_avx2_psign_d:
+  case x86_avx2_psrlv_d:
+  case x86_avx2_psrlv_d_256:
+  case x86_avx2_psrlv_q:
+  case x86_avx2_psrlv_q_256:
+  case x86_avx512_psrlv_d_512:
+  case x86_avx512_psrlv_q_512:
+  case x86_avx512_psrlv_w_128:
+  case x86_avx512_psrlv_w_256:
+  case x86_avx512_psrlv_w_512:
+  case x86_avx2_psrav_d:
+  case x86_avx2_psrav_d_256:
+  case x86_avx512_psrav_d_512:
+  case x86_avx512_psrav_q_128:
+  case x86_avx512_psrav_q_256:
+  case x86_avx512_psrav_q_512:
+  case x86_avx512_psrav_w_128:
+  case x86_avx512_psrav_w_256:
+  case x86_avx512_psrav_w_512:
+  case x86_avx2_psllv_d:
+  case x86_avx2_psllv_d_256:
+  case x86_avx2_psllv_q:
+  case x86_avx2_psllv_q_256:
+  case x86_avx512_psllv_d_512:
+  case x86_avx512_psllv_q_512:
+  case x86_avx512_psllv_w_128:
+  case x86_avx512_psllv_w_256:
+  case x86_avx512_psllv_w_512:
+  case x86_sse2_pmulh_w:
+  case x86_avx2_pmulh_w:
+  case x86_avx512_pmulh_w_512:
+  case x86_sse2_pmulhu_w:
+  case x86_avx2_pmulhu_w:
+  case x86_avx512_pmulhu_w_512: {
+    vector<StateValue> vals;
+    function<expr(const expr &, const expr &)> fn;
+    switch (op) {
+    case x86_sse2_pavg_w:
+    case x86_sse2_pavg_b:
+    case x86_avx2_pavg_w:
+    case x86_avx2_pavg_b:
+    case x86_avx512_pavg_w_512:
+    case x86_avx512_pavg_b_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned bw = a.bits();
+        return (a.zext(1) + b.zext(1) + expr::mkUInt(1, bw + 1))
+            .lshr(expr::mkUInt(1, bw + 1))
+            .trunc(bw);
+      };
+      break;
+    case x86_ssse3_psign_b_128:
+    case x86_ssse3_psign_w_128:
+    case x86_ssse3_psign_d_128:
+    case x86_avx2_psign_b:
+    case x86_avx2_psign_w:
+    case x86_avx2_psign_d:
+      fn = [&](auto a, auto b) -> expr {
+        return expr::mkIf(
+            b.isZero(), b,
+            expr::mkIf(b.isNegative(), expr::mkUInt(0, a.bits()) - a, a));
+      };
+      break;
+    case x86_avx2_psrlv_d:
+    case x86_avx2_psrlv_d_256:
+    case x86_avx2_psrlv_q:
+    case x86_avx2_psrlv_q_256:
+    case x86_avx512_psrlv_d_512:
+    case x86_avx512_psrlv_q_512:
+    case x86_avx512_psrlv_w_128:
+    case x86_avx512_psrlv_w_256:
+    case x86_avx512_psrlv_w_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned bw = a.bits();
+        return expr::mkIf(b.uge(expr::mkUInt(bw, bw)), expr::mkUInt(0, bw),
+                          a.lshr(b));
+      };
+      break;
+    case x86_avx2_psrav_d:
+    case x86_avx2_psrav_d_256:
+    case x86_avx512_psrav_d_512:
+    case x86_avx512_psrav_q_128:
+    case x86_avx512_psrav_q_256:
+    case x86_avx512_psrav_q_512:
+    case x86_avx512_psrav_w_128:
+    case x86_avx512_psrav_w_256:
+    case x86_avx512_psrav_w_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned bw = a.bits();
+        return expr::mkIf(b.uge(expr::mkUInt(bw, bw)),
+                          expr::mkIf(a.isNegative(), expr::mkUInt(-1, bw),
+                                     expr::mkUInt(0, bw)),
+                          a.ashr(b));
+      };
+      break;
+    case x86_avx2_psllv_d:
+    case x86_avx2_psllv_d_256:
+    case x86_avx2_psllv_q:
+    case x86_avx2_psllv_q_256:
+    case x86_avx512_psllv_d_512:
+    case x86_avx512_psllv_q_512:
+    case x86_avx512_psllv_w_128:
+    case x86_avx512_psllv_w_256:
+    case x86_avx512_psllv_w_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned bw = a.bits();
+        return expr::mkIf(b.uge(expr::mkUInt(bw, bw)), expr::mkUInt(0, bw),
+                          a << b);
+      };
+      break;
+    case x86_sse2_pmulh_w:
+    case x86_avx2_pmulh_w:
+    case x86_avx512_pmulh_w_512:
+      fn = [&](auto a, auto b) -> expr {
+        expr mul = a.sext(16) * b.sext(16);
+        return mul.extract(31, 16);
+      };
+      break;
+    case x86_sse2_pmulhu_w:
+    case x86_avx2_pmulhu_w:
+    case x86_avx512_pmulhu_w_512:
+      fn = [&](auto a, auto b) -> expr {
+        expr mul = a.zext(16) * b.zext(16);
+        return mul.extract(31, 16);
+      };
+      break;
+    default:
+      UNREACHABLE();
+    }
+    for (unsigned i = 0, e = rty->numElementsConst(); i != e; ++i) {
+      auto ai = aty->extract(av, i);
+      auto bi = bty->extract(bv, i);
+      vals.emplace_back(fn(ai.value, bi.value), ai.non_poison && bi.non_poison);
+    }
+    return rty->aggregateVals(vals);
+  }
+  // pshuf.b
+  case x86_ssse3_pshuf_b_128:
+  case x86_avx2_pshuf_b:
+  case x86_avx512_pshuf_b_512: {
+    auto avty = static_cast<const VectorType *>(aty);
+    vector<StateValue> vals;
+    unsigned laneCount = shape_ret[op].first;
+    for (unsigned i = 0; i != laneCount; ++i) {
+      auto [b, bp] = bty->extract(bv, i);
+      expr id = (b & expr::mkUInt(0x0F, 8)) + (expr::mkUInt(i & 0x30, 8));
+      auto [r, rp] = avty->extract(av, id);
+      auto ai = expr::mkIf(b.extract(7, 7) == expr::mkUInt(0, 1), r,
+                           expr::mkUInt(0, 8));
+
+      vals.emplace_back(std::move(ai), bp && rp);
+    }
+    return rty->aggregateVals(vals);
+  }
+  // horizontal
+  case x86_ssse3_phadd_w_128:
+  case x86_ssse3_phadd_d_128:
+  case x86_ssse3_phadd_sw_128:
+  case x86_avx2_phadd_w:
+  case x86_avx2_phadd_d:
+  case x86_avx2_phadd_sw:
+  case x86_ssse3_phsub_w_128:
+  case x86_ssse3_phsub_d_128:
+  case x86_ssse3_phsub_sw_128:
+  case x86_avx2_phsub_w:
+  case x86_avx2_phsub_d:
+  case x86_avx2_phsub_sw: {
+    vector<StateValue> vals;
+    unsigned laneCount = shape_ret[op].first;
+    unsigned groupsize = 128 / shape_ret[op].second;
+    function<expr(const expr &, const expr &)> fn;
+    switch (op) {
+    case x86_ssse3_phadd_w_128:
+    case x86_ssse3_phadd_d_128:
+    case x86_avx2_phadd_w:
+    case x86_avx2_phadd_d:
+      fn = [&](auto a, auto b) -> expr { return a + b; };
+      break;
+    case x86_ssse3_phadd_sw_128:
+    case x86_avx2_phadd_sw:
+      fn = [&](auto a, auto b) -> expr { return a.sadd_sat(b); };
+      break;
+    case x86_ssse3_phsub_w_128:
+    case x86_ssse3_phsub_d_128:
+    case x86_avx2_phsub_w:
+    case x86_avx2_phsub_d:
+      fn = [&](auto a, auto b) -> expr { return a - b; };
+      break;
+    case x86_ssse3_phsub_sw_128:
+    case x86_avx2_phsub_sw:
+      fn = [&](auto a, auto b) -> expr { return a.ssub_sat(b); };
+      break;
+    default:
+      UNREACHABLE();
+    }
+    for (unsigned j = 0; j != laneCount / groupsize; j++) {
+      for (unsigned i = 0; i != groupsize; i += 2) {
+        auto [a1, p1] = aty->extract(av, j * groupsize + i);
+        auto [a2, p2] = aty->extract(av, j * groupsize + i + 1);
+        vals.emplace_back(fn(a1, a2), p1 && p2);
+      }
+      for (unsigned i = 0; i != groupsize; i += 2) {
+        auto [b1, p1] = aty->extract(bv, j * groupsize + i);
+        auto [b2, p2] = aty->extract(bv, j * groupsize + i + 1);
+        vals.emplace_back(fn(b1, b2), p1 && p2);
+      }
+    }
+    return rty->aggregateVals(vals);
+  }
+  case x86_sse2_psrli_w:
+  case x86_sse2_psrli_d:
+  case x86_sse2_psrli_q:
+  case x86_avx2_psrli_w:
+  case x86_avx2_psrli_d:
+  case x86_avx2_psrli_q:
+  case x86_avx512_psrli_w_512:
+  case x86_avx512_psrli_d_512:
+  case x86_avx512_psrli_q_512:
+  case x86_sse2_psrai_w:
+  case x86_sse2_psrai_d:
+  case x86_avx2_psrai_w:
+  case x86_avx2_psrai_d:
+  case x86_avx512_psrai_w_512:
+  case x86_avx512_psrai_d_512:
+  case x86_avx512_psrai_q_128:
+  case x86_avx512_psrai_q_256:
+  case x86_avx512_psrai_q_512:
+  case x86_sse2_pslli_w:
+  case x86_sse2_pslli_d:
+  case x86_sse2_pslli_q:
+  case x86_avx2_pslli_w:
+  case x86_avx2_pslli_d:
+  case x86_avx2_pslli_q:
+  case x86_avx512_pslli_w_512:
+  case x86_avx512_pslli_d_512:
+  case x86_avx512_pslli_q_512: {
+    vector<StateValue> vals;
+    function<expr(const expr &, const expr &)> fn;
+    switch (op) {
+    case x86_sse2_psrai_w:
+    case x86_sse2_psrai_d:
+    case x86_avx2_psrai_w:
+    case x86_avx2_psrai_d:
+    case x86_avx512_psrai_w_512:
+    case x86_avx512_psrai_d_512:
+    case x86_avx512_psrai_q_128:
+    case x86_avx512_psrai_q_256:
+    case x86_avx512_psrai_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned sz_a = a.bits();
+        expr check = b.uge(expr::mkUInt(sz_a, 32));
+        expr outbounds = expr::mkIf(a.isNegative(), expr::mkInt(-1, sz_a),
+                                    expr::mkUInt(0, sz_a));
+        expr inbounds = a.ashr(b.zextOrTrunc(sz_a));
+        return expr::mkIf(std::move(check), std::move(outbounds),
+                          std::move(inbounds));
+      };
+      break;
+    case x86_sse2_psrli_w:
+    case x86_sse2_psrli_d:
+    case x86_sse2_psrli_q:
+    case x86_avx2_psrli_w:
+    case x86_avx2_psrli_d:
+    case x86_avx2_psrli_q:
+    case x86_avx512_psrli_w_512:
+    case x86_avx512_psrli_d_512:
+    case x86_avx512_psrli_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned sz_a = a.bits();
+        expr check = b.uge(expr::mkUInt(sz_a, 32));
+        expr outbounds = expr::mkUInt(0, sz_a);
+        expr inbounds = a.lshr(b.zextOrTrunc(sz_a));
+        return expr::mkIf(std::move(check), std::move(outbounds),
+                          std::move(inbounds));
+      };
+      break;
+    case x86_sse2_pslli_w:
+    case x86_sse2_pslli_d:
+    case x86_sse2_pslli_q:
+    case x86_avx2_pslli_w:
+    case x86_avx2_pslli_d:
+    case x86_avx2_pslli_q:
+    case x86_avx512_pslli_w_512:
+    case x86_avx512_pslli_d_512:
+    case x86_avx512_pslli_q_512:
+      fn = [&](auto a, auto b) -> expr {
+        unsigned sz_a = a.bits();
+        expr check = b.uge(expr::mkUInt(sz_a, 32));
+        expr outbounds = expr::mkUInt(0, sz_a);
+        expr inbounds = a << b.zextOrTrunc(sz_a);
+        return expr::mkIf(std::move(check), std::move(outbounds),
+                          std::move(inbounds));
+      };
+      break;
+    default:
+      UNREACHABLE();
+    }
+    for (unsigned i = 0, e = rty->numElementsConst(); i != e; ++i) {
+      auto ai = aty->extract(av, i);
+      vals.emplace_back(fn(ai.value, bv.value), ai.non_poison && bv.non_poison);
+    }
+    return rty->aggregateVals(vals);
+  }
+  case x86_sse2_pmadd_wd:
+  case x86_avx2_pmadd_wd:
+  case x86_avx512_pmaddw_d_512:
+  case x86_ssse3_pmadd_ub_sw_128:
+  case x86_avx2_pmadd_ub_sw:
+  case x86_avx512_pmaddubs_w_512: {
+    vector<StateValue> vals;
+    for (unsigned i = 0, e = shape_ret[op].first; i != e; ++i) {
+      auto [a1, a1p] = aty->extract(av, i * 2);
+      auto [a2, a2p] = aty->extract(av, i * 2 + 1);
+      auto [b1, b1p] = bty->extract(bv, i * 2);
+      auto [b2, b2p] = bty->extract(bv, i * 2 + 1);
+
+      auto np = a1p && a2p && b1p && b2p;
+
+      if (op == x86_sse2_pmadd_wd || op == x86_avx2_pmadd_wd ||
+          op == x86_avx512_pmaddw_d_512) {
+        expr v = a1.sext(16) * b1.sext(16) + a2.sext(16) * b2.sext(16);
+        vals.emplace_back(std::move(v), std::move(np));
+      } else {
+        expr v = (a1.zext(8) * b1.sext(8)).sadd_sat(a2.zext(8) * b2.sext(8));
+        vals.emplace_back(std::move(v), std::move(np));
+      }
+    }
+    return rty->aggregateVals(vals);
+  }
+  case x86_sse2_packsswb_128:
+  case x86_avx2_packsswb:
+  case x86_avx512_packsswb_512:
+  case x86_sse2_packuswb_128:
+  case x86_avx2_packuswb:
+  case x86_avx512_packuswb_512:
+  case x86_sse2_packssdw_128:
+  case x86_avx2_packssdw:
+  case x86_avx512_packssdw_512:
+  case x86_sse41_packusdw:
+  case x86_avx2_packusdw:
+  case x86_avx512_packusdw_512: {
+    vector<StateValue> vals;
+    function<expr(const expr &)> fn;
+    if (op == x86_sse2_packsswb_128 || op == x86_avx2_packsswb ||
+        op == x86_avx512_packsswb_512 || op == x86_sse2_packssdw_128 ||
+        op == x86_avx2_packssdw || op == x86_avx512_packssdw_512) {
+      fn = [&](auto a) -> expr {
+        unsigned bw = a.bits() / 2;
+        auto min = expr::IntSMin(bw);
+        auto max = expr::IntSMax(bw);
+        return expr::mkIf(a.sle(min.sext(bw)), min,
+                          expr::mkIf(a.sge(max.sext(bw)), max, a.trunc(bw)));
+      };
+    } else {
+      fn = [&](auto a) -> expr {
+        unsigned bw = a.bits() / 2;
+        auto max = expr::IntUMax(bw);
+        auto zero = expr::mkUInt(0, bw);
+        return expr::mkIf(a.sle(zero.zext(bw)), zero,
+                          expr::mkIf(a.sge(max.zext(bw)), max, a.trunc(bw)));
+      };
+    }
+
+    unsigned groupsize = 128 / shape_op1[op].second;
+    unsigned laneCount = shape_op1[op].first;
+    for (unsigned j = 0; j != laneCount / groupsize; j++) {
+      for (unsigned i = 0; i != groupsize; i++) {
+        auto [a1, p1] = aty->extract(av, j * groupsize + i);
+        vals.emplace_back(fn(std::move(a1)), std::move(p1));
+      }
+      for (unsigned i = 0; i != groupsize; i++) {
+        auto [b1, p1] = aty->extract(bv, j * groupsize + i);
+        vals.emplace_back(fn(std::move(b1)), std::move(p1));
+      }
+    }
+    return rty->aggregateVals(vals);
+  }
+  case x86_sse2_psad_bw:
+  case x86_avx2_psad_bw:
+  case x86_avx512_psad_bw_512: {
+    unsigned ngroup = shape_ret[op].first;
+    vector<StateValue> vals;
+    for (unsigned j = 0; j < ngroup; ++j) {
+      expr np = true;
+      expr v;
+      for (unsigned i = 0; i < 8; ++i) {
+        auto [a, ap] = aty->extract(av, 8 * j + i);
+        auto [b, bp] = bty->extract(bv, 8 * j + i);
+        np = np && ap && bp;
+        if (i == 0)
+          v = (a.zext(8) - b.zext(8)).abs();
+        else
+          v = v + (a.zext(8) - b.zext(8)).abs();
+      }
+      vals.emplace_back(v.zext(48), std::move(np));
+    }
+    return rty->aggregateVals(vals);
+  }
+  // TODO: add semantic for other intrinsics
+  default:
+    UNREACHABLE();
+  }
+}
+
+expr X86IntrinBinOp::getTypeConstraints(const Function &f) const {
+  return Value::getTypeConstraints() &&
+         (shape_op0[op].first != 1
+              ? a->getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_op0[op].second);
+                }) &&
+                    a->getType().getAsAggregateType()->numElements() ==
+                        shape_op0[op].first
+              : a->getType().enforceIntType(shape_op0[op].second)) &&
+         (shape_op1[op].first != 1
+              ? b->getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_op1[op].second);
+                }) &&
+                    b->getType().getAsAggregateType()->numElements() ==
+                        shape_op1[op].first
+              : b->getType().enforceIntType(shape_op1[op].second)) &&
+         (shape_ret[op].first != 1
+              ? getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_ret[op].second);
+                }) &&
+                    getType().getAsAggregateType()->numElements() ==
+                        shape_ret[op].first
+              : getType().enforceIntType(shape_ret[op].second));
+}
+
+unique_ptr<Instr> X86IntrinBinOp::dup(Function &f, const string &suffix) const {
+  return make_unique<X86IntrinBinOp>(getType(), getName() + suffix, *a, *b, op);
+}
+
+string X86IntrinTerOp::getOpName(Op op) {
+  switch (op) {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H)                                  \
+  case NAME:                                                                   \
+    return #NAME;
+#include "intrinsics_terop.h"
+#undef PROCESS
+  }
+  UNREACHABLE();
+}
+
+void X86IntrinTerOp::print(ostream &os) const {
+  os << getName() << " = " << getOpName(op) << " " << *a << ", " << *b;
+}
+
+StateValue X86IntrinTerOp::toSMT(State &s) const {
+  auto rty = getType().getAsAggregateType();
+  auto aty = a->getType().getAsAggregateType();
+  auto bty = b->getType().getAsAggregateType();
+  auto cty = c->getType().getAsAggregateType();
+  auto &av = s[*a];
+  auto &bv = s[*b];
+  auto &cv = s[*c];
+
+  switch (op) {
+  case x86_avx2_pblendvb: {
+    vector<StateValue> vals;
+
+    for (int i = 0; i < 32; ++i) {
+      auto [a, ap] = aty->extract(av, i);
+      auto [b, bp] = bty->extract(bv, i);
+      auto [c, cp] = cty->extract(cv, i);
+      auto v = expr::mkIf(c.extract(7, 7) == expr::mkUInt(0, 1), a, b);
+      vals.emplace_back(std::move(v), ap && bp && cp);
+    }
+    return rty->aggregateVals(vals);
+  }
+  // TODO: add semantic for other intrinsics
+  default:
+    UNREACHABLE();
+  }
+}
+
+expr X86IntrinTerOp::getTypeConstraints(const Function &f) const {
+  return Value::getTypeConstraints() &&
+         (shape_op0[op].first != 1
+              ? a->getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_op0[op].second);
+                }) &&
+                    a->getType().getAsAggregateType()->numElements() ==
+                        shape_op0[op].first
+              : a->getType().enforceIntType(shape_op0[op].second)) &&
+         (shape_op1[op].first != 1
+              ? b->getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_op1[op].second);
+                }) &&
+                    b->getType().getAsAggregateType()->numElements() ==
+                        shape_op1[op].first
+              : b->getType().enforceIntType(shape_op1[op].second)) &&
+         (shape_op2[op].first != 1
+              ? b->getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_op2[op].second);
+                }) &&
+                    b->getType().getAsAggregateType()->numElements() ==
+                        shape_op2[op].first
+              : b->getType().enforceIntType(shape_op2[op].second)) &&
+         (shape_ret[op].first != 1
+              ? getType().enforceVectorType([this](auto &ty) {
+                  return ty.enforceIntType(shape_ret[op].second);
+                }) &&
+                    getType().getAsAggregateType()->numElements() ==
+                        shape_ret[op].first
+              : getType().enforceIntType(shape_ret[op].second));
+}
+
+unique_ptr<Instr> X86IntrinTerOp::dup(Function &f, const string &suffix) const {
+  return make_unique<X86IntrinTerOp>(getType(), getName() + suffix, *a, *b, *c,
+                                     op);
+}
+
+vector<Value *> X86IntrinTerOp::operands() const {
+  return {a, b, c};
+}
+
+bool X86IntrinTerOp::propagatesPoison() const {
+  return true;
+}
+
+bool X86IntrinTerOp::hasSideEffects() const {
+  return false;
+}
+
+void X86IntrinTerOp::rauw(const Value &what, Value &with) {
+  RAUW(a);
+  RAUW(b);
+  RAUW(c);
+}
 
 const ConversionOp* isCast(ConversionOp::Op op, const Value &v) {
   auto c = dynamic_cast<const ConversionOp*>(&v);
diff --git a/ir/instr.h b/ir/instr.h
index d77ad38c1..473fb4d86 100644
--- a/ir/instr.h
+++ b/ir/instr.h
@@ -532,8 +532,8 @@ class Phi final : public Instr {
   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;
+  std::unique_ptr<Instr> dup(Function &f,
+                             const std::string &suffix) const override;
 };
 
 
@@ -1286,6 +1286,141 @@ class ShuffleVector final : public Instr {
     dup(Function &f, const std::string &suffix) const override;
 };
 
+class FakeShuffle final : public Instr {
+  Value *v1, *v2, *mask;
+
+public:
+  FakeShuffle(Type &type, std::string &&name, Value &v1, Value &v2, Value &mask)
+      : Instr(type, std::move(name)), v1(&v1), v2(&v2), mask(&mask) {}
+  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 X86IntrinBinOp final : public Instr {
+public:
+  static constexpr unsigned numOfX86Intrinsics = 135;
+  enum Op {
+#define PROCESS(NAME, A, B, C, D, E, F) NAME,
+#include "intrinsics_binop.h"
+#undef PROCESS
+  };
+
+  // the shape of a vector is stored as <# of lanes, element bits>
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_op0 = {
+#define PROCESS(NAME, A, B, C, D, E, F) std::make_pair(C, D),
+#include "intrinsics_binop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_op1 = {
+#define PROCESS(NAME, A, B, C, D, E, F) std::make_pair(E, F),
+#include "intrinsics_binop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_ret = {
+#define PROCESS(NAME, A, B, C, D, E, F) std::make_pair(A, B),
+#include "intrinsics_binop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<unsigned, numOfX86Intrinsics> ret_width = {
+#define PROCESS(NAME, A, B, C, D, E, F) A *B,
+#include "intrinsics_binop.h"
+#undef PROCESS
+  };
+
+private:
+  Value *a, *b;
+  Op op;
+
+public:
+  static unsigned getRetWidth(Op op) {
+    return ret_width[op];
+  }
+  X86IntrinBinOp(Type &type, std::string &&name, Value &a, Value &b, Op op)
+      : Instr(type, std::move(name)), a(&a), b(&b), op(op) {}
+  std::vector<Value *> operands() const override;
+  bool propagatesPoison() const override;
+  bool hasSideEffects() const override;
+  void rauw(const Value &what, Value &with) override;
+  static std::string getOpName(Op op);
+  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 X86IntrinTerOp final : public Instr {
+public:
+  static constexpr unsigned numOfX86Intrinsics = 1;
+  enum Op {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) NAME,
+#include "intrinsics_terop.h"
+#undef PROCESS
+  };
+
+  // the shape of a vector is stored as <# of lanes, element bits>
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_op0 = {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) std::make_pair(C, D),
+#include "intrinsics_terop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_op1 = {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) std::make_pair(E, F),
+#include "intrinsics_terop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_op2 = {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) std::make_pair(G, H),
+#include "intrinsics_terop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<std::pair<unsigned, unsigned>, numOfX86Intrinsics>
+      shape_ret = {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) std::make_pair(A, B),
+#include "intrinsics_terop.h"
+#undef PROCESS
+      };
+  static constexpr std::array<unsigned, numOfX86Intrinsics> ret_width = {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) A *B,
+#include "intrinsics_terop.h"
+#undef PROCESS
+  };
+
+private:
+  Value *a, *b, *c;
+  Op op;
+
+public:
+  static unsigned getRetWidth(Op op) {
+    return ret_width[op];
+  }
+  X86IntrinTerOp(Type &type, std::string &&name, Value &a, Value &b, Value &c,
+                 Op op)
+      : Instr(type, std::move(name)), a(&a), b(&b), c(&c), op(op) {}
+  std::vector<Value *> operands() const override;
+  bool propagatesPoison() const override;
+  bool hasSideEffects() const override;
+  void rauw(const Value &what, Value &with) override;
+  static std::string getOpName(Op op);
+  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;
+};
 
 const ConversionOp *isCast(ConversionOp::Op op, const Value &v);
 Value *isNoOp(const Value &v);
diff --git a/ir/intrinsics_binop.h b/ir/intrinsics_binop.h
new file mode 100644
index 000000000..ab0483932
--- /dev/null
+++ b/ir/intrinsics_binop.h
@@ -0,0 +1,135 @@
+PROCESS(x86_sse2_pavg_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_sse2_pavg_b, 16, 8, 16, 8, 16, 8)
+PROCESS(x86_avx2_pavg_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx2_pavg_b, 32, 8, 32, 8, 32, 8)
+PROCESS(x86_avx512_pavg_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_avx512_pavg_b_512, 64, 8, 64, 8, 64, 8)
+PROCESS(x86_avx2_pshuf_b, 32, 8, 32, 8, 32, 8)
+PROCESS(x86_ssse3_pshuf_b_128, 16, 8, 16, 8, 16, 8)
+PROCESS(x86_avx512_pshuf_b_512, 64, 8, 64, 8, 64, 8)
+PROCESS(x86_sse2_psrl_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_sse2_psrl_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_sse2_psrl_q, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx2_psrl_w, 16, 16, 16, 16, 8, 16)
+PROCESS(x86_avx2_psrl_d, 8, 32, 8, 32, 4, 32)
+PROCESS(x86_avx2_psrl_q, 4, 64, 4, 64, 2, 64)
+PROCESS(x86_avx512_psrl_w_512, 32, 16, 32, 16, 8, 16)
+PROCESS(x86_avx512_psrl_d_512, 16, 32, 16, 32, 4, 32)
+PROCESS(x86_avx512_psrl_q_512, 8, 64, 8, 64, 2, 64)
+PROCESS(x86_sse2_psrli_w, 8, 16, 8, 16, 1, 32)
+PROCESS(x86_sse2_psrli_d, 4, 32, 4, 32, 1, 32)
+PROCESS(x86_sse2_psrli_q, 2, 64, 2, 64, 1, 32)
+PROCESS(x86_avx2_psrli_w, 16, 16, 16, 16, 1, 32)
+PROCESS(x86_avx2_psrli_d, 8, 32, 8, 32, 1, 32)
+PROCESS(x86_avx2_psrli_q, 4, 64, 4, 64, 1, 32)
+PROCESS(x86_avx512_psrli_w_512, 32, 16, 32, 16, 1, 32)
+PROCESS(x86_avx512_psrli_d_512, 16, 32, 16, 32, 1, 32)
+PROCESS(x86_avx512_psrli_q_512, 8, 64, 8, 64, 1, 32)
+PROCESS(x86_avx2_psrlv_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_avx2_psrlv_d_256, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_avx2_psrlv_q, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx2_psrlv_q_256, 4, 64, 4, 64, 4, 64)
+PROCESS(x86_avx512_psrlv_d_512, 16, 32, 16, 32, 16, 32)
+PROCESS(x86_avx512_psrlv_q_512, 8, 64, 8, 64, 8, 64)
+PROCESS(x86_avx512_psrlv_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx512_psrlv_w_256, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx512_psrlv_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_sse2_psra_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_sse2_psra_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_avx2_psra_w, 16, 16, 16, 16, 8, 16)
+PROCESS(x86_avx2_psra_d, 8, 32, 8, 32, 4, 32)
+PROCESS(x86_avx512_psra_q_128, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx512_psra_q_256, 4, 64, 4, 64, 2, 64)
+PROCESS(x86_avx512_psra_w_512, 32, 16, 32, 16, 8, 16)
+PROCESS(x86_avx512_psra_d_512, 16, 32, 16, 32, 4, 32)
+PROCESS(x86_avx512_psra_q_512, 8, 64, 8, 64, 2, 64)
+PROCESS(x86_sse2_psrai_w, 8, 16, 8, 16, 1, 32)
+PROCESS(x86_sse2_psrai_d, 4, 32, 4, 32, 1, 32)
+PROCESS(x86_avx2_psrai_w, 16, 16, 16, 16, 1, 32)
+PROCESS(x86_avx2_psrai_d, 8, 32, 8, 32, 1, 32)
+PROCESS(x86_avx512_psrai_w_512, 32, 16, 32, 16, 1, 32)
+PROCESS(x86_avx512_psrai_d_512, 16, 32, 16, 32, 1, 32)
+PROCESS(x86_avx512_psrai_q_128, 2, 64, 2, 64, 1, 32)
+PROCESS(x86_avx512_psrai_q_256, 4, 64, 4, 64, 1, 32)
+PROCESS(x86_avx512_psrai_q_512, 8, 64, 8, 64, 1, 32)
+PROCESS(x86_avx2_psrav_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_avx2_psrav_d_256, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_avx512_psrav_d_512, 16, 32, 16, 32, 16, 32)
+PROCESS(x86_avx512_psrav_q_128, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx512_psrav_q_256, 4, 64, 4, 64, 4, 64)
+PROCESS(x86_avx512_psrav_q_512, 8, 64, 8, 64, 8, 64)
+PROCESS(x86_avx512_psrav_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx512_psrav_w_256, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx512_psrav_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_sse2_psll_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_sse2_psll_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_sse2_psll_q, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx2_psll_w, 16, 16, 16, 16, 8, 16)
+PROCESS(x86_avx2_psll_d, 8, 32, 8, 32, 4, 32)
+PROCESS(x86_avx2_psll_q, 4, 64, 4, 64, 2, 64)
+PROCESS(x86_avx512_psll_w_512, 32, 16, 32, 16, 8, 16)
+PROCESS(x86_avx512_psll_d_512, 16, 32, 16, 32, 4, 32)
+PROCESS(x86_avx512_psll_q_512, 8, 64, 8, 64, 2, 64)
+PROCESS(x86_sse2_pslli_w, 8, 16, 8, 16, 1, 32)
+PROCESS(x86_sse2_pslli_d, 4, 32, 4, 32, 1, 32)
+PROCESS(x86_sse2_pslli_q, 2, 64, 2, 64, 1, 32)
+PROCESS(x86_avx2_pslli_w, 16, 16, 16, 16, 1, 32)
+PROCESS(x86_avx2_pslli_d, 8, 32, 8, 32, 1, 32)
+PROCESS(x86_avx2_pslli_q, 4, 64, 4, 64, 1, 32)
+PROCESS(x86_avx512_pslli_w_512, 32, 16, 32, 16, 1, 32)
+PROCESS(x86_avx512_pslli_d_512, 16, 32, 16, 32, 1, 32)
+PROCESS(x86_avx512_pslli_q_512, 8, 64, 8, 64, 1, 32)
+PROCESS(x86_avx2_psllv_d, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_avx2_psllv_d_256, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_avx2_psllv_q, 2, 64, 2, 64, 2, 64)
+PROCESS(x86_avx2_psllv_q_256, 4, 64, 4, 64, 4, 64)
+PROCESS(x86_avx512_psllv_d_512, 16, 32, 16, 32, 16, 32)
+PROCESS(x86_avx512_psllv_q_512, 8, 64, 8, 64, 8, 64)
+PROCESS(x86_avx512_psllv_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx512_psllv_w_256, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx512_psllv_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_ssse3_psign_b_128, 16, 8, 16, 8, 16, 8)
+PROCESS(x86_ssse3_psign_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_ssse3_psign_d_128, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_avx2_psign_b, 32, 8, 32, 8, 32, 8)
+PROCESS(x86_avx2_psign_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx2_psign_d, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_ssse3_phadd_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_ssse3_phadd_d_128, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_ssse3_phadd_sw_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx2_phadd_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx2_phadd_d, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_avx2_phadd_sw, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_ssse3_phsub_w_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_ssse3_phsub_d_128, 4, 32, 4, 32, 4, 32)
+PROCESS(x86_ssse3_phsub_sw_128, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx2_phsub_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx2_phsub_d, 8, 32, 8, 32, 8, 32)
+PROCESS(x86_avx2_phsub_sw, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_sse2_pmulh_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx2_pmulh_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx512_pmulh_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_sse2_pmulhu_w, 8, 16, 8, 16, 8, 16)
+PROCESS(x86_avx2_pmulhu_w, 16, 16, 16, 16, 16, 16)
+PROCESS(x86_avx512_pmulhu_w_512, 32, 16, 32, 16, 32, 16)
+PROCESS(x86_sse2_pmadd_wd, 4, 32, 8, 16, 8, 16)
+PROCESS(x86_avx2_pmadd_wd, 8, 32, 16, 16, 16, 16)
+PROCESS(x86_avx512_pmaddw_d_512, 16, 32, 32, 16, 32, 16)
+PROCESS(x86_ssse3_pmadd_ub_sw_128, 8, 16, 16, 8, 16, 8)
+PROCESS(x86_avx2_pmadd_ub_sw, 16, 16, 32, 8, 32, 8)
+PROCESS(x86_avx512_pmaddubs_w_512, 32, 16, 64, 8, 64, 8)
+PROCESS(x86_sse2_packsswb_128, 16, 8, 8, 16, 8, 16)
+PROCESS(x86_avx2_packsswb, 32, 8, 16, 16, 16, 16)
+PROCESS(x86_avx512_packsswb_512, 64, 8, 32, 16, 32, 16)
+PROCESS(x86_sse2_packuswb_128, 16, 8, 8, 16, 8, 16)
+PROCESS(x86_avx2_packuswb, 32, 8, 16, 16, 16, 16)
+PROCESS(x86_avx512_packuswb_512, 64, 8, 32, 16, 32, 16)
+PROCESS(x86_sse2_packssdw_128, 8, 16, 4, 32, 4, 32)
+PROCESS(x86_avx2_packssdw, 16, 16, 8, 32, 8, 32)
+PROCESS(x86_avx512_packssdw_512, 32, 16, 16, 32, 16, 32)
+PROCESS(x86_sse41_packusdw, 8, 16, 4, 32, 4, 32)
+PROCESS(x86_avx2_packusdw, 16, 16, 8, 32, 8, 32)
+PROCESS(x86_avx512_packusdw_512, 32, 16, 16, 32, 16, 32)
+PROCESS(x86_sse2_psad_bw, 2, 64, 16, 8, 16, 8)
+PROCESS(x86_avx2_psad_bw, 4, 64, 32, 8, 32, 8)
+PROCESS(x86_avx512_psad_bw_512, 8, 64, 64, 8, 64, 8)
\ No newline at end of file
diff --git a/ir/intrinsics_terop.h b/ir/intrinsics_terop.h
new file mode 100644
index 000000000..9d0265d02
--- /dev/null
+++ b/ir/intrinsics_terop.h
@@ -0,0 +1 @@
+PROCESS(x86_avx2_pblendvb, 32, 8, 32, 8, 32, 8, 32, 8)
\ No newline at end of file
diff --git a/ir/type.cpp b/ir/type.cpp
index ee7c1e805..ad3d530d1 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>
@@ -447,6 +448,9 @@ expr FloatType::getFloat(const expr &v) const {
 expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0,
                           unsigned nary, const expr &a, const expr &b,
                           const expr &c) const {
+  if (config::use_exact_fp)
+    return fp.float2BV();
+
   expr isnan = fp.isNaN();
   expr val = fp.float2BV();
 
diff --git a/llvm_util/known_fns.cpp b/llvm_util/known_fns.cpp
index 440dcb384..bd74109fd 100644
--- a/llvm_util/known_fns.cpp
+++ b/llvm_util/known_fns.cpp
@@ -516,6 +516,12 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
     RETURN_EXACT();
 
   auto decl = i.getCalledFunction();
+
+  if (decl && decl->hasName() && decl->getName().starts_with("__fksv")) {
+    RETURN_VAL(make_unique<FakeShuffle>(*ty, value_name(i), *args[0], *args[1],
+                                        *args[2]));
+  }
+
   llvm::LibFunc libfn;
   if (!decl || !TLI.getLibFunc(*decl, libfn))
     RETURN_EXACT();
diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp
index 928e47a26..eb6905777 100644
--- a/llvm_util/llvm2alive.cpp
+++ b/llvm_util/llvm2alive.cpp
@@ -15,6 +15,7 @@
 #include "llvm/IR/InstVisitor.h"
 #include "llvm/IR/InstrTypes.h"
 #include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicsX86.h"
 #include "llvm/IR/Operator.h"
 #include "llvm/Support/ModRef.h"
 #include <sstream>
@@ -1222,6 +1223,45 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
     case llvm::Intrinsic::prefetch:
       return NOP(i);
 
+      // intel x86 intrinsics
+#define PROCESS(NAME, A, B, C, D, E, F) case llvm::Intrinsic::NAME:
+#include "ir/intrinsics_binop.h"
+#undef PROCESS
+      {
+        PARSE_BINOP();
+        X86IntrinBinOp::Op op;
+        switch (i.getIntrinsicID()) {
+#define PROCESS(NAME, A, B, C, D, E, F)                                        \
+  case llvm::Intrinsic::NAME:                                                  \
+    op = X86IntrinBinOp::NAME;                                                 \
+    break;
+#include "ir/intrinsics_binop.h"
+#undef PROCESS
+        default:
+          UNREACHABLE();
+        }
+        return make_unique<X86IntrinBinOp>(*ty, value_name(i), *a, *b, op);
+      }
+
+#define PROCESS(NAME, A, B, C, D, E, F, G, H) case llvm::Intrinsic::NAME:
+#include "ir/intrinsics_terop.h"
+#undef PROCESS
+      {
+        PARSE_TRIOP();
+        X86IntrinTerOp::Op op;
+        switch (i.getIntrinsicID()) {
+#define PROCESS(NAME, A, B, C, D, E, F, G, H)                                  \
+  case llvm::Intrinsic::NAME:                                                  \
+    op = X86IntrinTerOp::NAME;                                                 \
+    break;
+#include "ir/intrinsics_terop.h"
+#undef PROCESS
+        default:
+          UNREACHABLE();
+        }
+        return make_unique<X86IntrinTerOp>(*ty, value_name(i), *a, *b, *c, op);
+      }
+
     default:
       break;
     }
diff --git a/llvm_util/utils.cpp b/llvm_util/utils.cpp
index a359edea0..4012cead3 100644
--- a/llvm_util/utils.cpp
+++ b/llvm_util/utils.cpp
@@ -205,7 +205,7 @@ Type* llvm_type2alive(const llvm::Type *ty) {
       auto vty = cast<llvm::VectorType>(ty);
       auto elems = vty->getElementCount().getKnownMinValue();
       auto ety = llvm_type2alive(vty->getElementType());
-      if (!ety || elems > 1024)
+      if (!ety || elems > 2048)
         return nullptr;
       cache = make_unique<VectorType>("ty_" + to_string(type_id_counter++),
                                       elems, *ety);
diff --git a/tests/alive-tv/vector/x86/avx2_psign_w-0.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psign_w-0.srctgt.ll
new file mode 100644
index 000000000..fc0b1aa36
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psign_w-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32> %v, <8 x i32>  zeroinitializer)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> zeroinitializer
+}
+
+declare <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32>, <8 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psign_w-1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psign_w-1.srctgt.ll
new file mode 100644
index 000000000..cc4406a27
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psign_w-1.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32> %v, <8 x i32> <i32 8, i32 8, i32 8, i32 8, i32 8, i32 8, i32 8, i32 8>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> %v
+}
+
+declare <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32>, <8 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psign_w-2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psign_w-2.srctgt.ll
new file mode 100644
index 000000000..5c28e9b95
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psign_w-2.srctgt.ll
@@ -0,0 +1,11 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32> %v, <8 x i32> <i32 -8, i32 -8, i32 -8, i32 -8, i32 -8, i32 -8, i32 -8, i32 -8>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  %neg = sub  <8 x i32> zeroinitializer, %v
+  ret <8 x i32> %neg
+}
+
+declare <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32>, <8 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psign_w-3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psign_w-3.srctgt.ll
new file mode 100644
index 000000000..246786752
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psign_w-3.srctgt.ll
@@ -0,0 +1,12 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32> %v, <8 x i32> <i32 -8, i32 1, i32 -8, i32 1, i32 -8, i32 1, i32 -8, i32 1>)
+  %2 = call <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32> %1, <8 x i32> <i32 1, i32 -1, i32 1, i32 -1, i32 1, i32 -1, i32 1, i32 -1>)
+  ret <8 x i32> %2
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  %neg = sub  <8 x i32> zeroinitializer, %v
+  ret <8 x i32> %neg
+}
+
+declare <8 x i32> @llvm.x86.avx2.psign.d(<8 x i32>, <8 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-0.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-0.srctgt.ll
new file mode 100644
index 000000000..32ce38d0c
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32>  zeroinitializer)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> %v
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-15.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-15.srctgt.ll
new file mode 100644
index 000000000..dc39ecc52
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 15, i32 0, i32 9999, i32 9999>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  %tmp = lshr <8 x i32> %v, <i32 15, i32 15, i32 15, i32 15, i32 15, i32 15, i32 15, i32 15>
+  ret <8 x i32> %tmp
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-3.srctgt.ll
new file mode 100644
index 000000000..7365b7355
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 3, i32 0, i32 9999, i32 9999>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  %tmp = lshr <8 x i32> %v, <i32 5, i32 5, i32 5, i32 5, i32 5, i32 5, i32 5, i32 5>
+  ret <8 x i32> %tmp
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow1.srctgt.ll
new file mode 100644
index 000000000..4e454a092
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 15, i32 15, i32 15, i32 15>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> zeroinitializer
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow2.srctgt.ll
new file mode 100644
index 000000000..a5d6914b9
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 0, i32 1, i32 0, i32 0>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> zeroinitializer
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow3.srctgt.ll
new file mode 100644
index 000000000..1e9fd5c72
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 32, i32 0, i32 0, i32 0>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> zeroinitializer
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow4.srctgt.ll
new file mode 100644
index 000000000..dcae58ef7
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow4.srctgt.ll
@@ -0,0 +1,13 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 0, i32 1, i32 0, i32 0>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> %v
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow5.srctgt.ll
new file mode 100644
index 000000000..83e9468ee
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-overflow5.srctgt.ll
@@ -0,0 +1,14 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 15, i32 15, i32 9999, i32 9999>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  %tmp = lshr <8 x i32> %v, <i32 15, i32 15, i32 15, i32 15, i32 15, i32 15, i32 15, i32 15>
+  ret <8 x i32> %tmp
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-poison1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-poison1.srctgt.ll
new file mode 100644
index 000000000..3f6994fba
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 0, i32 poison, i32 0, i32 0>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> poison
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_d-poison2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_d-poison2.srctgt.ll
new file mode 100644
index 000000000..ea86f827a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_d-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i32> @src(<8 x i32> %v) {
+  %1 = call <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32> %v, <4 x i32> <i32 0, i32 0, i32 poison, i32 0>)
+  ret <8 x i32> %1
+}
+
+define <8 x i32> @tgt(<8 x i32> %v) {
+  ret <8 x i32> %v
+}
+
+declare <8 x i32> @llvm.x86.avx2.psrl.d(<8 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-0.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-0.srctgt.ll
new file mode 100644
index 000000000..4f23a76a3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  zeroinitializer)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> %v
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-15.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-15.srctgt.ll
new file mode 100644
index 000000000..e56cf907f
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 5, i64 9999>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  %tmp = lshr <4 x i64> %v, <i64 5, i64 5, i64 5, i64 5>
+  ret <4 x i64> %tmp
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-3.srctgt.ll
new file mode 100644
index 000000000..00437e136
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 3, i64 9999>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  %tmp = lshr <4 x i64> %v, <i64 5, i64 5, i64 5, i64 5>
+  ret <4 x i64> %tmp
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow1.srctgt.ll
new file mode 100644
index 000000000..abb3c758a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 -1, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> zeroinitializer
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow2.srctgt.ll
new file mode 100644
index 000000000..a675c22df
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 72, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> zeroinitializer
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow3.srctgt.ll
new file mode 100644
index 000000000..66bec3e8a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 64, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> zeroinitializer
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow4.srctgt.ll
new file mode 100644
index 000000000..10d8981e4
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow4.srctgt.ll
@@ -0,0 +1,13 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 64, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> %v
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow5.srctgt.ll
new file mode 100644
index 000000000..807017d24
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-overflow5.srctgt.ll
@@ -0,0 +1,13 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 128, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> %v
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-poison1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-poison1.srctgt.ll
new file mode 100644
index 000000000..5636e4de3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 poison, i64 0>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> poison
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_q-poison2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_q-poison2.srctgt.ll
new file mode 100644
index 000000000..236ef23c1
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_q-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i64> @src(<4 x i64> %v) {
+  %1 = call <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64> %v, <2 x i64>  <i64 0, i64 poison>)
+  ret <4 x i64> %1
+}
+
+define <4 x i64> @tgt(<4 x i64> %v) {
+  ret <4 x i64> %v
+}
+
+declare <4 x i64> @llvm.x86.avx2.psrl.q(<4 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-0.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-0.srctgt.ll
new file mode 100644
index 000000000..a299a1b67
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16>  zeroinitializer)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> %v
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-15.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-15.srctgt.ll
new file mode 100644
index 000000000..7f2e6a60b
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 15, i16 0, i16 0, i16 0, i16 9999, i16 9999, i16 9999, i16 9999>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  %tmp = lshr <16 x i16> %v, <i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15>
+  ret <16 x i16> %tmp
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-3.srctgt.ll
new file mode 100644
index 000000000..193f599c9
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 3, i16 0, i16 0, i16 0, i16 9999, i16 9999, i16 9999, i16 9999>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  %tmp = lshr <16 x i16> %v, <i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5>
+  ret <16 x i16> %tmp
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow1.srctgt.ll
new file mode 100644
index 000000000..26e70e2cd
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> zeroinitializer
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow2.srctgt.ll
new file mode 100644
index 000000000..3f1154eb2
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 0, i16 0, i16 0, i16 1, i16 0, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> zeroinitializer
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow3.srctgt.ll
new file mode 100644
index 000000000..a15297fab
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 16, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> zeroinitializer
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow4.srctgt.ll
new file mode 100644
index 000000000..0b1a429b0
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow4.srctgt.ll
@@ -0,0 +1,14 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 0, i16 0, i16 1, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> %v
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
+
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow5.srctgt.ll
new file mode 100644
index 000000000..9a8d45ad5
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-overflow5.srctgt.ll
@@ -0,0 +1,13 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 15, i16 15, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> %v
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-poison1.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-poison1.srctgt.ll
new file mode 100644
index 000000000..79ced610a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 0, i16 0, i16 poison, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> poison
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/avx2_psrl_w-poison2.srctgt.ll b/tests/alive-tv/vector/x86/avx2_psrl_w-poison2.srctgt.ll
new file mode 100644
index 000000000..2d0ac7d6e
--- /dev/null
+++ b/tests/alive-tv/vector/x86/avx2_psrl_w-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <16 x i16> @src(<16 x i16> %v) {
+  %1 = call <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16> %v, <8 x i16> <i16 0, i16 0, i16 0, i16 0, i16 poison, i16 0, i16 0, i16 0>)
+  ret <16 x i16> %1
+}
+
+define <16 x i16> @tgt(<16 x i16> %v) {
+  ret <16 x i16> %v
+}
+
+declare <16 x i16> @llvm.x86.avx2.psrl.w(<16 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/regression-feb-8-01.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-8-01.srctgt.ll
new file mode 100644
index 000000000..d7e55fa87
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-8-01.srctgt.ll
@@ -0,0 +1,16 @@
+
+
+define <32 x i8> @tgt() {
+entry:
+  ret <32 x i8> <i8 -41, i8 -41, i8 0, i8 9, i8 -102, i8 -105, i8 -7, i8 -43, i8 -22, i8 103, i8 -105, i8 4, i8 123, i8 -105, i8 0, i8 -96, i8 -96, i8 57, i8 -82, i8 -116, i8 -96, i8 34, i8 -116, i8 114, i8 -114, i8 -38, i8 -96, i8 -38, i8 30, i8 83, i8 -90, i8 83>
+}
+define <32 x i8> @src() {
+entry:
+  %calltmp = call <32 x i8> @llvm.x86.avx2.pshuf.b(<32 x i8> <i8 -41, i8 9, i8 88, i8 0, i8 65, i8 -96, i8 -41, i8 103, i8 -7, i8 -105, i8 -22, i8 123, i8 4, i8 -71, i8 -102, i8 -43, i8 83, i8 -116, i8 -114, i8 -38, i8 -82, i8 -96, i8 30, i8 57, i8 34, i8 -90, i8 -116, i8 114, i8 -96, i8 9, i8 -33, i8 100>, <32 x i8> <i8 32, i8 38, i8 3, i8 33, i8 14, i8 9, i8 8, i8 15, i8 10, i8 23, i8 25, i8 28, i8 27, i8 25, i8 35, i8 37, i8 5, i8 23, i8 20, i8 1, i8 37, i8 8, i8 17, i8 11, i8 34, i8 19, i8 28, i8 19, i8 38, i8 0, i8 25, i8 0>)
+  ret <32 x i8> %calltmp
+}
+
+
+declare <32 x i8> @llvm.x86.avx2.pshuf.b(<32 x i8>,  <32 x i8>)
+
+
diff --git a/tests/alive-tv/vector/x86/regression-feb-8-02.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-8-02.srctgt.ll
new file mode 100644
index 000000000..244451bd2
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-8-02.srctgt.ll
@@ -0,0 +1,11 @@
+
+define <64 x i8> @tgt() {
+entry:
+  ret <64 x i8> <i8 57, i8 28, i8 66, i8 70, i8 32, i8 113, i8 114, i8 58, i8 109, i8 9, i8 54, i8 57, i8 101, i8 13, i8 60, i8 37, i8 48, i8 66, i8 115, i8 20, i8 60, i8 35, i8 77, i8 41, i8 -115, i8 112, i8 105, i8 26, i8 43, i8 81, i8 41, i8 117, i8 15, i8 88, i8 29, i8 56, i8 13, i8 116, i8 109, i8 -126, i8 38, i8 93, i8 93, i8 101, i8 33, i8 35, i8 31, i8 57, i8 97, i8 34, i8 104, i8 -124, i8 76, i8 121, i8 69, i8 92, i8 32, i8 86, i8 43, i8 112, i8 89, i8 109, i8 81, i8 9>
+}
+define <64 x i8> @src() {
+entry:
+  %calltmp = call <64 x i8> @llvm.x86.avx512.pavg.b.512(<64 x i8> <i8 79, i8 52, i8 101, i8 -124, i8 34, i8 -45, i8 -59, i8 104, i8 -63, i8 7, i8 75, i8 94, i8 -94, i8 7, i8 116, i8 67, i8 73, i8 126, i8 -55, i8 5, i8 115, i8 40, i8 -124, i8 69, i8 -4, i8 -40, i8 -48, i8 30, i8 81, i8 -97, i8 73, i8 -34, i8 19, i8 -82, i8 35, i8 86, i8 8, i8 -37, i8 -39, i8 -5, i8 51, i8 -81, i8 -84, i8 -85, i8 43, i8 41, i8 40, i8 113, i8 -67, i8 45, i8 -54, i8 -29, i8 -125, i8 -53, i8 -124, i8 -101, i8 49, i8 -121, i8 81, i8 -50, i8 -109, i8 -48, i8 -101, i8 11>, <64 x i8> <i8 34, i8 3, i8 30, i8 7, i8 29, i8 15, i8 30, i8 11, i8 25, i8 10, i8 32, i8 19, i8 39, i8 19, i8 4, i8 7, i8 22, i8 6, i8 29, i8 35, i8 5, i8 29, i8 21, i8 12, i8 30, i8 7, i8 1, i8 22, i8 4, i8 2, i8 8, i8 11, i8 11, i8 1, i8 23, i8 26, i8 18, i8 12, i8 1, i8 8, i8 25, i8 10, i8 14, i8 30, i8 22, i8 29, i8 22, i8 1, i8 4, i8 22, i8 5, i8 36, i8 21, i8 39, i8 5, i8 29, i8 14, i8 37, i8 5, i8 17, i8 31, i8 10, i8 6, i8 6>)
+    ret <64 x i8> %calltmp
+}
+declare  <64 x i8> @llvm.x86.avx512.pavg.b.512 (<64 x i8>, <64 x i8>)
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-01.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-01.srctgt.ll
new file mode 100644
index 000000000..825752f25
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-01.srctgt.ll
@@ -0,0 +1,11 @@
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.psra.w(<16 x i16> <i16 -4649, i16 10503, i16 28854, i16 -704, i16 -11691, i16 -10953, i16 15674, i16 25715, i16 28534, i16 -15426, i16 5651, i16 -27134, i16 30580, i16 17528, i16 -17404, i16 -5397>, <8 x i16> <i16 11, i16 20, i16 32, i16 16, i16 2, i16 26, i16 34, i16 14>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 -1, i16 0, i16 0, i16 -1, i16 -1, i16 -1, i16 0, i16 0, i16 0, i16 -1, i16 0, i16 -1, i16 0, i16 0, i16 -1, i16 -1>
+}
+
+declare <16 x i16> @llvm.x86.avx2.psra.w(<16 x i16>, <8 x i16>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-02.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-02.srctgt.ll
new file mode 100644
index 000000000..736243a6c
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-02.srctgt.ll
@@ -0,0 +1,11 @@
+define <8 x i32> @src() {
+entry:
+  %calltmp = call <8 x i32> @llvm.x86.avx2.psra.d(<8 x i32> <i32 -1216751044, i32 1436703847, i32 1582383160, i32 -1379019227, i32 -1448759623, i32 500738486, i32 -615243513, i32 -729809403>, <4 x i32> <i32 2, i32 2, i32 38, i32 11>)
+  ret <8 x i32> %calltmp
+}
+define <8 x i32> @tgt() {
+entry:
+  ret <8 x i32> <i32 -1, i32 0, i32 0, i32 -1, i32 -1, i32 0, i32 -1, i32 -1>
+}
+
+declare <8 x i32> @llvm.x86.avx2.psra.d(<8 x i32>, <4 x i32>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-03.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-03.srctgt.ll
new file mode 100644
index 000000000..890add5b3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-03.srctgt.ll
@@ -0,0 +1,11 @@
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.phadd.w(<16 x i16> <i16 -23974, i16 -14890, i16 -25912, i16 30689, i16 -5316, i16 12682, i16 25468, i16 30283, i16 19045, i16 2503, i16 -13296, i16 26823, i16 -6801, i16 3895, i16 -15459, i16 -29275>, <16 x i16> <i16 39, i16 35, i16 15, i16 26, i16 11, i16 35, i16 6, i16 12, i16 22, i16 29, i16 32, i16 30, i16 17, i16 2, i16 21, i16 35>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 26672, i16 4777, i16 7366, i16 -9785, i16 74, i16 41, i16 46, i16 18, i16 21548, i16 13527, i16 -2906, i16 20802, i16 51, i16 62, i16 19, i16 56>
+}
+
+declare <16 x i16> @llvm.x86.avx2.phadd.w(<16 x i16>, <16 x i16>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-04.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-04.srctgt.ll
new file mode 100644
index 000000000..ca2da0440
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-04.srctgt.ll
@@ -0,0 +1,11 @@
+define <8 x i32> @src() {
+entry:
+  %calltmp = call <8 x i32> @llvm.x86.avx2.phadd.d(<8 x i32> <i32 1722070598, i32 302159761, i32 -203316396, i32 -2123912179, i32 1892339105, i32 -1274131692, i32 744247972, i32 2066006689>, <8 x i32> <i32 21, i32 17, i32 38, i32 31, i32 39, i32 16, i32 32, i32 16>)
+  ret <8 x i32> %calltmp
+}
+define <8 x i32> @tgt() {
+entry:
+  ret <8 x i32> <i32 2024230359, i32 1967738721, i32 38, i32 69, i32 618207413, i32 -1484712635, i32 55, i32 48>
+}
+
+declare <8 x i32> @llvm.x86.avx2.phadd.d(<8 x i32>, <8 x i32>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-05.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-05.srctgt.ll
new file mode 100644
index 000000000..b9ca1e0e3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-05.srctgt.ll
@@ -0,0 +1,11 @@
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.phadd.sw(<16 x i16> <i16 15539, i16 27789, i16 20819, i16 -22928, i16 -2898, i16 31193, i16 20033, i16 -24598, i16 27029, i16 -11096, i16 -24697, i16 30251, i16 -26094, i16 6319, i16 17091, i16 -13189>, <16 x i16> <i16 4, i16 21, i16 5, i16 35, i16 17, i16 30, i16 33, i16 27, i16 14, i16 21, i16 7, i16 34, i16 26, i16 20, i16 28, i16 39>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 32767, i16 -2109, i16 28295, i16 -4565, i16 25, i16 40, i16 47, i16 60, i16 15933, i16 5554, i16 -19775, i16 3902, i16 35, i16 41, i16 46, i16 67>
+}
+
+declare <16 x i16> @llvm.x86.avx2.phadd.sw(<16 x i16>, <16 x i16>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-06.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-06.srctgt.ll
new file mode 100644
index 000000000..827d20c56
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-06.srctgt.ll
@@ -0,0 +1,11 @@
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.phsub.w(<16 x i16> <i16 29913, i16 18877, i16 -5940, i16 22954, i16 -7751, i16 -2118, i16 -24244, i16 -20010, i16 -29467, i16 13671, i16 -3601, i16 -25726, i16 -1313, i16 -15489, i16 -30581, i16 21294>, <16 x i16> <i16 35, i16 12, i16 8, i16 34, i16 38, i16 16, i16 0, i16 7, i16 23, i16 32, i16 12, i16 17, i16 0, i16 22, i16 15, i16 6>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 11036, i16 -28894, i16 -5633, i16 -4234, i16 23, i16 -26, i16 22, i16 -7, i16 22398, i16 22125, i16 14176, i16 13661, i16 -9, i16 -5, i16 -22, i16 9>
+}
+
+declare <16 x i16> @llvm.x86.avx2.phsub.w(<16 x i16>, <16 x i16>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-07.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-07.srctgt.ll
new file mode 100644
index 000000000..9951d2b1b
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-07.srctgt.ll
@@ -0,0 +1,11 @@
+define <8 x i32> @src() {
+entry:
+  %calltmp = call <8 x i32> @llvm.x86.avx2.phsub.d(<8 x i32> <i32 -1306389437, i32 -1699807924, i32 -1725376897, i32 -995818298, i32 759098485, i32 -1239181406, i32 1140698766, i32 -2138096067>, <8 x i32> <i32 17, i32 18, i32 9, i32 2, i32 25, i32 29, i32 31, i32 4>)
+  ret <8 x i32> %calltmp
+}
+define <8 x i32> @tgt() {
+entry:
+  ret <8 x i32> <i32 393418487, i32 -729558599, i32 -1, i32 7, i32 1998279891, i32 -1016172463, i32 -4, i32 27>
+}
+
+declare <8 x i32> @llvm.x86.avx2.phsub.d(<8 x i32>, <8 x i32>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-08.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-08.srctgt.ll
new file mode 100644
index 000000000..7c98d69d3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-08.srctgt.ll
@@ -0,0 +1,11 @@
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.phsub.sw(<16 x i16> <i16 24924, i16 -25507, i16 2987, i16 -13944, i16 11726, i16 -10060, i16 32351, i16 -28323, i16 1089, i16 1322, i16 3373, i16 -18952, i16 -20008, i16 -29103, i16 -29017, i16 -24248>, <16 x i16> <i16 15, i16 26, i16 29, i16 22, i16 17, i16 16, i16 14, i16 5, i16 25, i16 8, i16 18, i16 19, i16 20, i16 33, i16 28, i16 28>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 32767, i16 16931, i16 21786, i16 32767, i16 -11, i16 7, i16 1, i16 9, i16 -233, i16 22325, i16 9095, i16 -4769, i16 17, i16 -1, i16 -13, i16 0>
+}
+
+declare <16 x i16> @llvm.x86.avx2.phsub.sw(<16 x i16>, <16 x i16>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-09.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-09.srctgt.ll
new file mode 100644
index 000000000..4cadbdd64
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-09.srctgt.ll
@@ -0,0 +1,11 @@
+define <8 x i16> @src() {
+entry:
+  %calltmp = call <8 x i16> @llvm.x86.ssse3.pmadd.ub.sw.128(<16 x i8> <i8 25, i8 87, i8 -119, i8 -75, i8 8, i8 -7, i8 -57, i8 70, i8 -5, i8 19, i8 89, i8 29, i8 11, i8 19, i8 -48, i8 -111>, <16 x i8> <i8 25, i8 32, i8 12, i8 30, i8 14, i8 16, i8 12, i8 2, i8 8, i8 22, i8 28, i8 12, i8 22, i8 8, i8 6, i8 5>)
+  ret <8 x i16> %calltmp
+}
+define <8 x i16> @tgt() {
+entry:
+  ret <8 x i16> <i16 3409, i16 7074, i16 4096, i16 2528, i16 2426, i16 2840, i16 394, i16 1973>
+}
+
+declare <8 x i16> @llvm.x86.ssse3.pmadd.ub.sw.128(<16 x i8>, <16 x i8>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-10.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-10.srctgt.ll
new file mode 100644
index 000000000..465e03347
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-10.srctgt.ll
@@ -0,0 +1,12 @@
+
+define <16 x i16> @src() {
+entry:
+  %calltmp = call <16 x i16> @llvm.x86.avx2.pmadd.ub.sw(<32 x i8> <i8 -82, i8 -58, i8 92, i8 -13, i8 -51, i8 -87, i8 -94, i8 -115, i8 -82, i8 -12, i8 -104, i8 -40, i8 -123, i8 -26, i8 122, i8 -24, i8 -123, i8 25, i8 23, i8 -4, i8 -10, i8 -112, i8 44, i8 -115, i8 -102, i8 120, i8 30, i8 -58, i8 -84, i8 59, i8 -109, i8 -96>, <32 x i8> <i8 31, i8 24, i8 9, i8 22, i8 14, i8 27, i8 23, i8 6, i8 24, i8 5, i8 28, i8 33, i8 18, i8 28, i8 39, i8 31, i8 3, i8 31, i8 26, i8 7, i8 0, i8 15, i8 23, i8 11, i8 36, i8 5, i8 9, i8 21, i8 6, i8 19, i8 35, i8 34>)
+  ret <16 x i16> %calltmp
+}
+define <16 x i16> @tgt() {
+entry:
+  ret <16 x i16> <i16 10146, i16 6174, i16 7433, i16 4572, i16 5396, i16 11384, i16 8834, i16 11950, i16 1174, i16 2362, i16 2160, i16 2563, i16 6144, i16 4428, i16 2153, i16 10585>
+}
+
+declare  <16 x i16> @llvm.x86.avx2.pmadd.ub.sw(<32 x i8>, <32 x i8>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/regression-feb-9-11.srctgt.ll b/tests/alive-tv/vector/x86/regression-feb-9-11.srctgt.ll
new file mode 100644
index 000000000..3f6def4bc
--- /dev/null
+++ b/tests/alive-tv/vector/x86/regression-feb-9-11.srctgt.ll
@@ -0,0 +1,11 @@
+define <32 x i16> @src() {
+entry:
+  %calltmp = call <32 x i16> @llvm.x86.avx512.pmaddubs.w.512(<64 x i8> <i8 -70, i8 -80, i8 -88, i8 -107, i8 -112, i8 -59, i8 118, i8 -70, i8 -97, i8 116, i8 104, i8 114, i8 45, i8 -103, i8 104, i8 -53, i8 -20, i8 -45, i8 -105, i8 53, i8 -66, i8 -91, i8 110, i8 93, i8 85, i8 -107, i8 -99, i8 10, i8 80, i8 -123, i8 -68, i8 -87, i8 -19, i8 -76, i8 32, i8 -89, i8 -47, i8 104, i8 -32, i8 116, i8 -67, i8 -44, i8 84, i8 89, i8 98, i8 126, i8 63, i8 37, i8 28, i8 109, i8 113, i8 20, i8 -3, i8 -95, i8 -34, i8 -48, i8 -89, i8 -101, i8 -4, i8 122, i8 -1, i8 -90, i8 -89, i8 31>, <64 x i8> <i8 39, i8 3, i8 25, i8 13, i8 35, i8 4, i8 2, i8 34, i8 6, i8 18, i8 27, i8 8, i8 35, i8 15, i8 10, i8 5, i8 23, i8 38, i8 29, i8 26, i8 20, i8 30, i8 37, i8 4, i8 8, i8 14, i8 18, i8 19, i8 3, i8 20, i8 23, i8 35, i8 23, i8 21, i8 10, i8 5, i8 30, i8 6, i8 26, i8 23, i8 2, i8 36, i8 11, i8 11, i8 29, i8 37, i8 5, i8 12, i8 23, i8 26, i8 25, i8 1, i8 36, i8 32, i8 9, i8 22, i8 6, i8 5, i8 29, i8 4, i8 18, i8 32, i8 26, i8 13>)
+  ret <32 x i16> %calltmp
+}
+define <32 x i16> @tgt() {
+entry:
+  ret <32 x i16> <i16 7782, i16 6137, i16 5828, i16 6560, i16 3042, i16 3720, i16 3870, i16 2055, i16 13446, i16 5757, i16 8750, i16 4442, i16 2766, i16 3016, i16 2900, i16 10239, i16 9231, i16 1155, i16 6894, i16 8492, i16 8010, i16 1903, i16 7504, i16 759, i16 3478, i16 2845, i16 14260, i16 6574, i16 1777, i16 7796, i16 9902, i16 4745>
+}
+
+declare <32 x i16> @llvm.x86.avx512.pmaddubs.w.512(<64 x i8>, <64 x i8>)
\ No newline at end of file
diff --git a/tests/alive-tv/vector/x86/sse2_pavg_w_0-failed.srctgt.ll b/tests/alive-tv/vector/x86/sse2_pavg_w_0-failed.srctgt.ll
new file mode 100644
index 000000000..469f6abae
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_pavg_w_0-failed.srctgt.ll
@@ -0,0 +1,12 @@
+; ERROR: Value mismatch
+
+; test found by Stefan's random tester
+
+define <8 x i16> @src() {
+  %calltmp = call <8 x i16> @llvm.x86.sse2.pavg.w(<8 x i16> <i16 5292, i16 65516, i16 4810, i16 37856, i16 55071, i16 1957, i16 49088, i16 24990 >, <8 x i16> <i16 37, i16 21, i16 36, i16 21, i16 10, i16 27, i16 1, i16 9 >)
+  ret <8 x i16> %calltmp
+}
+define <8 x i16> @tgt() {
+  ret <8 x i16> <i16 2665, i16 1, i16 2423, i16 18939, i16 27541, i16 992, i16 24545, i16 12500 >
+}
+declare <8 x i16> @llvm.x86.sse2.pavg.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_pavg_w_0.srctgt.ll b/tests/alive-tv/vector/x86/sse2_pavg_w_0.srctgt.ll
new file mode 100644
index 000000000..42abb8ef7
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_pavg_w_0.srctgt.ll
@@ -0,0 +1,10 @@
+; test found by Stefan's random tester
+
+define <8 x i16> @src() {
+  %calltmp = call <8 x i16> @llvm.x86.sse2.pavg.w(<8 x i16> <i16 5292, i16 65516, i16 4810, i16 37856, i16 55071, i16 1957, i16 49088, i16 24990 >, <8 x i16> <i16 37, i16 21, i16 36, i16 21, i16 10, i16 27, i16 1, i16 9 >)
+  ret <8 x i16> %calltmp
+}
+define <8 x i16> @tgt() {
+  ret <8 x i16> <i16 2665, i16 32769, i16 2423, i16 18939, i16 27541, i16 992, i16 24545, i16 12500 >
+}
+declare <8 x i16> @llvm.x86.sse2.pavg.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-0.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-0.srctgt.ll
new file mode 100644
index 000000000..8a39bd30e
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32>  zeroinitializer)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> %v
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-15.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-15.srctgt.ll
new file mode 100644
index 000000000..65e2d153a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 15, i32 0, i32 9999, i32 9999>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  %tmp = lshr <4 x i32> %v, <i32 15, i32 15, i32 15, i32 15>
+  ret <4 x i32> %tmp
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-3.srctgt.ll
new file mode 100644
index 000000000..4f1ffb526
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 3, i32 0, i32 9999, i32 9999>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  %tmp = lshr <4 x i32> %v, <i32 5, i32 5, i32 5, i32 5>
+  ret <4 x i32> %tmp
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow1.srctgt.ll
new file mode 100644
index 000000000..074634471
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 15, i32 15, i32 15, i32 15>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> zeroinitializer
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow2.srctgt.ll
new file mode 100644
index 000000000..51300dca4
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 0, i32 1, i32 0, i32 0>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> zeroinitializer
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow3.srctgt.ll
new file mode 100644
index 000000000..da506e2c3
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 32, i32 0, i32 0, i32 0>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> zeroinitializer
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow4.srctgt.ll
new file mode 100644
index 000000000..288736109
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow4.srctgt.ll
@@ -0,0 +1,13 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 0, i32 1, i32 0, i32 0>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> %v
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow5.srctgt.ll
new file mode 100644
index 000000000..290b11284
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-overflow5.srctgt.ll
@@ -0,0 +1,14 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 15, i32 15, i32 9999, i32 9999>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  %tmp = lshr <4 x i32> %v, <i32 15, i32 15, i32 15, i32 15>
+  ret <4 x i32> %tmp
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-poison1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-poison1.srctgt.ll
new file mode 100644
index 000000000..5c5449aa1
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 0, i32 poison, i32 0, i32 0>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> poison
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_d-poison2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_d-poison2.srctgt.ll
new file mode 100644
index 000000000..3152e1440
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_d-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <4 x i32> @src(<4 x i32> %v) {
+  %1 = call <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32> %v, <4 x i32> <i32 0, i32 0, i32 poison, i32 0>)
+  ret <4 x i32> %1
+}
+
+define <4 x i32> @tgt(<4 x i32> %v) {
+  ret <4 x i32> %v
+}
+
+declare <4 x i32> @llvm.x86.sse2.psrl.d(<4 x i32>, <4 x i32>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-0.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-0.srctgt.ll
new file mode 100644
index 000000000..9b8319a4d
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  zeroinitializer)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> %v
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-15.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-15.srctgt.ll
new file mode 100644
index 000000000..0dff78493
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 5, i64 9999>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  %tmp = lshr <2 x i64> %v, <i64 5, i64 5>
+  ret <2 x i64> %tmp
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-3.srctgt.ll
new file mode 100644
index 000000000..7f1b08191
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 3, i64 9999>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  %tmp = lshr <2 x i64> %v, <i64 5, i64 5>
+  ret <2 x i64> %tmp
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow1.srctgt.ll
new file mode 100644
index 000000000..51e949fd8
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 -1, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> zeroinitializer
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow2.srctgt.ll
new file mode 100644
index 000000000..3198d8831
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 72, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> zeroinitializer
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow3.srctgt.ll
new file mode 100644
index 000000000..1edd0efeb
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 64, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> zeroinitializer
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow4.srctgt.ll
new file mode 100644
index 000000000..c539ea9fb
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow4.srctgt.ll
@@ -0,0 +1,13 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 64, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> %v
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow5.srctgt.ll
new file mode 100644
index 000000000..8bdf0cc5a
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-overflow5.srctgt.ll
@@ -0,0 +1,13 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 128, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> %v
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-poison1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-poison1.srctgt.ll
new file mode 100644
index 000000000..127443d74
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 poison, i64 0>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> poison
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_q-poison2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_q-poison2.srctgt.ll
new file mode 100644
index 000000000..78e237a4c
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_q-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <2 x i64> @src(<2 x i64> %v) {
+  %1 = call <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64> %v, <2 x i64>  <i64 0, i64 poison>)
+  ret <2 x i64> %1
+}
+
+define <2 x i64> @tgt(<2 x i64> %v) {
+  ret <2 x i64> %v
+}
+
+declare <2 x i64> @llvm.x86.sse2.psrl.q(<2 x i64>, <2 x i64>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-0.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-0.srctgt.ll
new file mode 100644
index 000000000..51e8ba278
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-0.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16>  zeroinitializer)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> %v
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-15.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-15.srctgt.ll
new file mode 100644
index 000000000..893d69653
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-15.srctgt.ll
@@ -0,0 +1,14 @@
+; TEST-ARGS: -disable-undef-input
+; disabled undef inputs to accelerate the verification
+
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 15, i16 0, i16 0, i16 0, i16 9999, i16 9999, i16 9999, i16 9999>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  %tmp = lshr <8 x i16> %v, <i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15>
+  ret <8 x i16> %tmp
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-3.srctgt.ll
new file mode 100644
index 000000000..81c57f18f
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-3.srctgt.ll
@@ -0,0 +1,13 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 3, i16 0, i16 0, i16 0, i16 9999, i16 9999, i16 9999, i16 9999>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  %tmp = lshr <8 x i16> %v, <i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5, i16 5>
+  ret <8 x i16> %tmp
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
+
+; ERROR: Value mismatch
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-overflow1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow1.srctgt.ll
new file mode 100644
index 000000000..24c2a90e0
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow1.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15, i16 15>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> zeroinitializer
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-overflow2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow2.srctgt.ll
new file mode 100644
index 000000000..33a2a9d38
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow2.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 0, i16 0, i16 0, i16 1, i16 0, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> zeroinitializer
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-overflow3.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow3.srctgt.ll
new file mode 100644
index 000000000..caa32b663
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow3.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 16, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> zeroinitializer
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-overflow4.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow4.srctgt.ll
new file mode 100644
index 000000000..afbc266ea
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow4.srctgt.ll
@@ -0,0 +1,14 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 0, i16 0, i16 1, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> %v
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
+
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-overflow5.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow5.srctgt.ll
new file mode 100644
index 000000000..6d82e3d49
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-overflow5.srctgt.ll
@@ -0,0 +1,13 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 15, i16 15, i16 0, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> %v
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
+
+; source = <0, 0, 0 ... >, tgt = <undef, 0, 0, ...> when %input = <undef, 0, 0, ...> 
+; ERROR: Target's return value is more undefined
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-poison1.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-poison1.srctgt.ll
new file mode 100644
index 000000000..bc03df188
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-poison1.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 0, i16 0, i16 poison, i16 0, i16 0, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> poison
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/tests/alive-tv/vector/x86/sse2_psrl_w-poison2.srctgt.ll b/tests/alive-tv/vector/x86/sse2_psrl_w-poison2.srctgt.ll
new file mode 100644
index 000000000..29e04d604
--- /dev/null
+++ b/tests/alive-tv/vector/x86/sse2_psrl_w-poison2.srctgt.ll
@@ -0,0 +1,10 @@
+define <8 x i16> @src(<8 x i16> %v) {
+  %1 = call <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16> %v, <8 x i16> <i16 0, i16 0, i16 0, i16 0, i16 poison, i16 0, i16 0, i16 0>)
+  ret <8 x i16> %1
+}
+
+define <8 x i16> @tgt(<8 x i16> %v) {
+  ret <8 x i16> %v
+}
+
+declare <8 x i16> @llvm.x86.sse2.psrl.w(<8 x i16>, <8 x i16>)
diff --git a/util/config.cpp b/util/config.cpp
index 82ab5f66a..dd11aac72 100644
--- a/util/config.cpp
+++ b/util/config.cpp
@@ -15,6 +15,7 @@ bool skip_smt = false;
 string smt_benchmark_dir;
 bool disable_poison_input = false;
 bool disable_undef_input = false;
+bool use_exact_fp = false;
 bool tgt_is_asm = false;
 bool fail_if_src_is_ub = false;
 bool disallow_ub_exploitation = false;
diff --git a/util/config.h b/util/config.h
index 57f58c888..397168875 100644
--- a/util/config.h
+++ b/util/config.h
@@ -19,6 +19,8 @@ extern bool disable_poison_input;
 
 extern bool disable_undef_input;
 
+extern bool use_exact_fp;
+
 extern bool tgt_is_asm;
 
 extern bool fail_if_src_is_ub;