From 6e4e74b99a199ead458b0b919286d667bd8e8f28 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 14 Feb 2014 18:45:21 +0000 Subject: 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. --- lib/Solver/STPBuilder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/Solver') 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; -- cgit 1.4.1