From 6587cf5f516f1ee632d06b13e0e1f874dfc96afb Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Fri, 19 Jul 2013 14:27:40 -0700 Subject: [PATCH] possible fix for bug 521 --- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/equality_engine.h | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) 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 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 d_nodes; -- 2.30.2