about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/STPBuilder.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 9e3a9862..ad0df3c2 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -220,7 +220,7 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;
@@ -241,7 +241,7 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;
@@ -271,7 +271,7 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
 
   // If overshifting, shift to zero
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(width, width)),
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
                    res,
                    bvZero(width));
   return res;