2 files changed, 23 insertions, 18 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index df7fffc5..d51c1695 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -35,6 +35,11 @@ namespace {
                  cl::init(false));
 
   cl::opt<bool>
+  CexCacheSuperSet("cex-cache-superset",
+                 cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"),
+                 cl::init(false));
+
+  cl::opt<bool>
   CexCacheExperimental("cex-cache-exp", cl::init(false));
 
 }
@@ -124,8 +129,10 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
   if (CexCacheTryAll) {
     // Look for a satisfying assignment for a superset, which is trivially an
     // assignment for any subset.
-    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
-    
+    Assignment **lookup = 0;
+    if (CexCacheSuperSet)
+      lookup = cache.findSuperset(key, NonNullAssignment());
+
     // Otherwise, look for a subset which is unsatisfiable, see below.
     if (!lookup) 
       lookup = cache.findSubset(key, NullAssignment());
@@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
 
     // Look for a satisfying assignment for a superset, which is trivially an
     // assignment for any subset.
-    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
+    Assignment **lookup = 0;
+    if (CexCacheSuperSet)
+      lookup = cache.findSuperset(key, NonNullAssignment());
 
     // Otherwise, look for a subset which is unsatisfiable -- if the subset is
     // unsatisfiable then no additional constraints can produce a valid
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6d7dd8b7..a5e4c5ad 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -51,11 +51,6 @@ namespace {
 
 
 STPArrayExprHash::~STPArrayExprHash() {
-  
-  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
-  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
-  
-   /*
   for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
     ::VCExpr array_expr = it->second;
     if (array_expr) {
@@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() {
       array_expr = 0;
     }
   }
-  
-  
-  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
+
+
+  for (UpdateNodeHashConstIter it = _update_node_hash.begin();
+      it != _update_node_hash.end(); ++it) {
     ::VCExpr un_expr = it->second;
     if (un_expr) {
       ::vc_DeleteExpr(un_expr);
       un_expr = 0;
     }
   }
-  */
 }
 
 /***/
@@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
-  res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
-                   res,
-                   bvZero(width));
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
+
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
@@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
@@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;