diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-02-14 18:45:21 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-02-14 18:45:21 +0000 |
| commit | 6e4e74b99a199ead458b0b919286d667bd8e8f28 (patch) | |
| tree | 1ed4ba4cc639b178f16d8a56bd75799d5033904e /lib/Solver/STPBuilder.cpp | |
| parent | e70cd5b0764fe50f1e081a7d3e8e81fd623aa090 (diff) | |
| download | klee-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/STPBuilder.cpp')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 6 |
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; |