fixing antoher small bug in backtracking

diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 10131a805af7564e7015d4b7e4985bdab020e327..f30006cb9dac0d64873a285f42306b5fffe090a8 100644 (file)
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -375,6 +375,8 @@ void EqualityEngine<NotifyClass>::undoMerge(EqualityNode& class1, EqualityNode&
 template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::backtrack() {
 
+  Debug("equality::backtrack") << "backtracking" << std::endl;
+
   // If we need to backtrack then do it
   if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
 
@@ -429,6 +431,7 @@ void EqualityEngine<NotifyClass>::backtrack() {
     for (int i = d_applicationLookups.size() - 1, i_end = (int) d_applicationLookupsCount; i >= i_end; -- i) {
       d_applicationLookup.erase(d_applicationLookups[i]);
     }
+    d_applicationLookups.resize(d_applicationLookupsCount);
   }
 
   if (d_nodes.size() > d_nodesCount) {
@@ -449,7 +452,6 @@ void EqualityEngine<NotifyClass>::backtrack() {
 
     // Now get rid of the nodes and the rest
     d_nodes.resize(d_nodesCount);
-    d_applicationLookups.resize(d_applicationLookupsCount);
     d_applications.resize(d_nodesCount);
     d_nodeTriggers.resize(d_nodesCount);
     d_nodeIndividualTrigger.resize(d_nodesCount);
@@ -866,6 +868,9 @@ void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& fu
   d_applicationLookup[funNormalized] = funId;
   d_applicationLookups.push_back(funNormalized);
   d_applicationLookupsCount = d_applicationLookupsCount + 1;
+  Debug("equality::backtrack") << "d_applicationLookupsCount = " << d_applicationLookupsCount << std::endl;
+  Debug("equality::backtrack") << "d_applicationLookups.size() = " << d_applicationLookups.size() << std::endl;
+  Assert(d_applicationLookupsCount == d_applicationLookups.size());
 }
 
 } // Namespace uf