about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2013-12-12 17:55:13 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2013-12-12 17:55:13 +0000
commitea338e4a774c513d078ffb183f86d1389b912227 (patch)
tree25bf08b446e21e187ae62924b769eccedc4e464a
parenta45df61f6641ed0f6b92919bf377ce2ef1f1d839 (diff)
downloadklee-ea338e4a774c513d078ffb183f86d1389b912227.tar.gz
Patch by Daniel Lupei, fixing a performance bug with the
counterexample cache.  (This is an old patch, reported at
http://llvm.org/bugs/show_bug.cgi?id=11435, on KLEE's old bug tracking
system.)
-rw-r--r--include/klee/Expr.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 4bebd521..f893c6cc 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -197,8 +197,10 @@ public:
   typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > ExprEquivSet;
   int compare(const Expr &b, ExprEquivSet &equivs) const;
   int compare(const Expr &b) const {
-    ExprEquivSet equivs;
-    return compare(b, equivs);
+    static ExprEquivSet equivs;
+    int r = compare(b, equivs);
+    equivs.clear();
+    return r;
   }
   virtual int compareContents(const Expr &b) const { return 0; }