possible fix for bug 521

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7f0f79ebc0c0e38dbb3332d026c261cdb951f760..199581b989b0b7ed5fabea03a5aa57172a81cd5b 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1348,7 +1348,7 @@ void EqualityEngine::propagate() {
     }
 
     // If not merging internal nodes, notify the master
-    if (d_masterEqualityEngine && !d_isInternal[mergeInto]) {
+    if (d_masterEqualityEngine && !d_isInternal[t1classId] && !d_isInternal[t2classId]) {
       d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
       d_masterEqualityEngine->propagate();
     }

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 206fb61c72eceb83b00c1c880376279a64a20f42..6962f0c69ce996d8a6150541157ca15a8da2855b 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -211,11 +211,6 @@ public:
     }
   };/* struct EqualityEngine::statistics */
 
-  /**
-   * Store the application lookup, with enough information to backtrack
-   */
-  void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
-
 private:
 
   /** The context we are using */
@@ -254,6 +249,11 @@ private:
   /** Number of application lookups, for backtracking.  */
   context::CDO<DefaultSizeType> d_applicationLookupsCount;
 
+  /**
+   * Store the application lookup, with enough information to backtrack
+   */
+  void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
+
   /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */
   std::vector<Node> d_nodes;