diff --git a/runtime/qsym_backend/Runtime.cpp b/runtime/qsym_backend/Runtime.cpp
index 68b093bd..3a13aabe 100644
--- a/runtime/qsym_backend/Runtime.cpp
+++ b/runtime/qsym_backend/Runtime.cpp
@@ -232,7 +232,7 @@ DEF_BINARY_EXPR_BUILDER(signed_div, SDiv)
 DEF_BINARY_EXPR_BUILDER(unsigned_rem, URem)
 DEF_BINARY_EXPR_BUILDER(signed_rem, SRem)
 
-DEF_BINARY_EXPR_BUILDER(shift_left, Shl)
+// DEF_BINARY_EXPR_BUILDER(shift_left, Shl)
 DEF_BINARY_EXPR_BUILDER(logical_shift_right, LShr)
 DEF_BINARY_EXPR_BUILDER(arithmetic_shift_right, AShr)
 
@@ -256,6 +256,13 @@ DEF_BINARY_EXPR_BUILDER(xor, Xor)
 
 #undef DEF_BINARY_EXPR_BUILDER
 
+SymExpr _sym_build_shift_left(SymExpr a, SymExpr b) {
+  return registerExpression(
+    g_expr_builder->createShl(allocatedExpressions.at(a), 
+      g_expr_builder->createAnd(allocatedExpressions.at(b),
+      allocatedExpressions.at(_sym_build_integer(31, 32)))));
+}
+
 SymExpr _sym_build_neg(SymExpr expr) {
   return registerExpression(
       g_expr_builder->createNeg(allocatedExpressions.at(expr)));
diff --git a/runtime/simple_backend/Runtime.cpp b/runtime/simple_backend/Runtime.cpp
index d7ef5f20..078eefdd 100644
--- a/runtime/simple_backend/Runtime.cpp
+++ b/runtime/simple_backend/Runtime.cpp
@@ -214,7 +214,7 @@ DEF_BINARY_EXPR_BUILDER(unsigned_div, bvudiv)
 DEF_BINARY_EXPR_BUILDER(signed_div, bvsdiv)
 DEF_BINARY_EXPR_BUILDER(unsigned_rem, bvurem)
 DEF_BINARY_EXPR_BUILDER(signed_rem, bvsrem)
-DEF_BINARY_EXPR_BUILDER(shift_left, bvshl)
+// DEF_BINARY_EXPR_BUILDER(shift_left, bvshl)
 DEF_BINARY_EXPR_BUILDER(logical_shift_right, bvlshr)
 DEF_BINARY_EXPR_BUILDER(arithmetic_shift_right, bvashr)
 
@@ -241,6 +241,10 @@ DEF_BINARY_EXPR_BUILDER(float_ordered_equal, fpa_eq)
 
 #undef DEF_BINARY_EXPR_BUILDER
 
+SymExpr _sym_build_shift_left(SymExpr a, SymExpr b) {
+  return registerExpression(Z3_mk_bvshl(g_context, a, Z3_mk_bvand(g_context, b, _sym_build_integer(31, 32))));
+}
+
 Z3_ast _sym_build_fp_add(Z3_ast a, Z3_ast b) {
   return registerExpression(Z3_mk_fpa_add(g_context, g_rounding_mode, a, b));
 }