From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 9 Feb 2012 21:25:00 +0000 (+0000)
Subject: fixing antoher small bug in backtracking
X-Git-Tag: cvc5-1.0.0~8338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d31ba827811ac3267366496eb3d893b65962bedc;p=cvc5.git

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 10131a805..f30006cb9 100644
--- 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