fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.

1 files changed, 4 insertions, 8 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index ba607526f..18a525f2d 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -284,8 +284,8 @@ private:
    */
   ApplicationIdsMap d_applicationLookup;
 
-  /** Map from ids to the nodes */
-  std::vector<TNode> d_nodes;
+  /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */
+  std::vector<Node> d_nodes;
 
   /** A context-dependents count of nodes */
   context::CDO<size_t> d_nodesCount;
@@ -302,9 +302,6 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
-  /** Context dependent size of the use-list memory */
-  context::CDO<size_t> d_useListNodeSize;
-
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -444,7 +441,7 @@ private:
   /**
    * Vector of original equalities of the triggers.
    */
-  std::vector<TNode> d_equalityTriggersOriginal;
+  std::vector<Node> d_equalityTriggersOriginal;
 
   /**
    * Context dependent count of triggers
@@ -497,7 +494,7 @@ private:
   /**
    * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
-   * else. TODO: mark the phantom equalities (skolems).
+   * else. 
    */
   void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
 
@@ -517,7 +514,6 @@ public:
     d_notify(notify),
     d_nodesCount(context, 0),
     d_assertedEqualitiesCount(context, 0),
-    d_useListNodeSize(context, 0),
     d_equalityTriggersCount(context, 0),
     d_stats(name)
   {