From: Dejan Jovanovic <dejan@csl.sri.com>
Date: Fri, 19 Jul 2013 21:27:40 +0000 (-0700)
Subject: possible fix for bug 521
X-Git-Tag: cvc5-1.0.0~7287^2~55
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6587cf5f516f1ee632d06b13e0e1f874dfc96afb;p=cvc5.git

possible fix for bug 521
---

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7f0f79ebc..199581b98 100644
--- 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 206fb61c7..6962f0c69 100644
--- 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;