about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-08-18 15:07:27 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-09-07 16:00:07 +0100
commit9912da3912436a71949b1b97d96975bddcb169e3 (patch)
treea612483a15af1c7e0efd54fab80f73fc7590edf7
parent7082eafd05b4f268132ab94772c0243dbebf5087 (diff)
downloadklee-9912da3912436a71949b1b97d96975bddcb169e3.tar.gz
Remove broken experimental optimisation for validity (--cex-cache-exp)
-rw-r--r--lib/Solver/CexCachingSolver.cpp19
1 files changed, 0 insertions, 19 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index dbbd3516..87e6169c 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -48,11 +48,6 @@ cl::opt<bool>
                               "before asking the SMT solver (default=false)"),
                      cl::cat(SolvingCat));
 
-cl::opt<bool> CexCacheExperimental(
-    "cex-cache-exp", cl::init(false),
-    cl::desc("Optimization for validity queries (default=false)"),
-    cl::cat(SolvingCat));
-
 } // namespace
 
 ///
@@ -302,20 +297,6 @@ bool CexCachingSolver::computeTruth(const Query& query,
                                     bool &isValid) {
   TimerStatIncrementer t(stats::cexCacheTime);
 
-  // There is a small amount of redundancy here. We only need to know
-  // truth and do not really need to compute an assignment. This means
-  // that we could check the cache to see if we already know that
-  // state ^ query has no assignment. In that case, by the validity of
-  // state, we know that state ^ !query must have an assignment, and
-  // so query cannot be true (valid). This does get hits, but doesn't
-  // really seem to be worth the overhead.
-
-  if (CexCacheExperimental) {
-    Assignment *a;
-    if (lookupAssignment(query.negateExpr(), a) && !a)
-      return false;
-  }
-
   Assignment *a;
   if (!getAssignment(query, a))
     return false;