about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2014-12-09 09:37:33 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2014-12-09 09:37:33 +0000
commit3ab04308ff9bf756284a773137254fe0240d2cab (patch)
tree53ea8655ebbe556103c532f40698369a9c87e24e /lib
parent3c042be7a340972c41165a2394702a4f613ef1f9 (diff)
parentbc7ddafc93f1b30fa39e7f47f62b41ae3ed6a07b (diff)
downloadklee-3ab04308ff9bf756284a773137254fe0240d2cab.tar.gz
Merge pull request #186 from paulmar/fixshift
Fix overshift check
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/MetaSMTBuilder.h2
-rw-r--r--lib/Solver/STPBuilder.cpp2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 458c55ba..6da1b492 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -284,7 +284,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShr
     if (shift == 0) {
         res = expr;
     }
-    else if (shift >= width - 1) {
+    else if (shift >= width) {
         res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width)));
     }
     else {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 34ce0ede..6d7dd8b7 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -283,7 +283,7 @@ ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
 
   if (shift==0) {
     return expr;
-  } else if (shift>=width-1) {
+  } else if (shift>=width) {
     return bvZero(width); // Overshift to zero
   } else {
     return vc_iteExpr(vc,