about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-02-14 18:45:21 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-02-14 18:45:21 +0000
commit6e4e74b99a199ead458b0b919286d667bd8e8f28 (patch)
tree1ed4ba4cc639b178f16d8a56bd75799d5033904e /lib/Solver
parente70cd5b0764fe50f1e081a7d3e8e81fd623aa090 (diff)
downloadklee-6e4e74b99a199ead458b0b919286d667bd8e8f28.tar.gz
Explicitly get the width of the "shift" expression rather than assuming
that is the samw width of the "expr" expression.

It probably is the same width (it defintely is in SMT-LIB but I'm not
sure about STP) but it is probably better to be explicit.
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;