Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.

3 files changed, 9 insertions, 10 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index c1596dddc..4555aac51 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -43,8 +43,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
   d_tt(),
   d_ffDt(),
   d_ttDt(),
-  d_varCache(),
-  d_termCache(),
+  d_varCache(smt.d_userContext),
+  d_termCache(smt.d_userContext),
   d_typeCache(),
   d_datatypeCache() {
 
@@ -640,7 +640,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           if(dt != dt2) {
             Assert(d_varCache.find(top) != d_varCache.end(),
                    "constructor `%s' not in cache", top.toString().c_str());
-            result.top() << d_varCache[top];
+            result.top() << d_varCache[top].get();
             worklist.pop();
             goto next_worklist;
           }
@@ -658,7 +658,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           if(dt != dt2) {
             Assert(d_varCache.find(top) != d_varCache.end(),
                    "tester or selector `%s' not in cache", top.toString().c_str());
-            result.top() << d_varCache[top];
+            result.top() << d_varCache[top].get();
             worklist.pop();
             goto next_worklist;
           } else {
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index 89611f5ea..b289e3469 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -36,12 +36,12 @@ typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
 
 class BooleanTermConverter {
   /** The type of the Boolean term conversion variable cache */
-  typedef std::hash_map<Node, Node, NodeHashFunction> BooleanTermVarCache;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> BooleanTermVarCache;
 
   /** The type of the Boolean term conversion cache */
-  typedef std::hash_map< std::pair<Node, theory::TheoryId>, Node,
-                         PairHashFunction< Node, bool,
-                                           NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
+  typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node,
+                              PairHashFunction< Node, bool,
+                                                NodeHashFunction, std::hash<size_t> > > BooleanTermCache;
   /** The type of the Boolean term conversion type cache */
   typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode,
                          PairHashFunction< TypeNode, bool,
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 328a20c28..7aebb60f6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1877,8 +1877,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
       d_assertionsToCheck[d_substitutionsIndex] =
         Rewriter::rewrite(Node(substitutionsBuilder));
     }
-  }
-  else {
+  } else {
     // If not in incremental mode, must add substitutions to model
     TheoryModel* m = d_smt.d_theoryEngine->getModel();
     if(m != NULL) {