Fixed bug 352

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 70be74442..b310de425 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -665,8 +665,10 @@ void UnconstrainedSimplifier::processUnconstrained()
   // back-substitution and cache-invalidation.  So we do these last.
   while (!delayQueueLeft.empty()) {
     left = delayQueueLeft.back();
-    right = d_substitutions.apply(delayQueueRight.back());
-    d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false);
+    if (!d_substitutions.hasSubstitution(left)) {
+      right = d_substitutions.apply(delayQueueRight.back());
+      d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false);
+    }
     delayQueueLeft.pop_back();
     delayQueueRight.pop_back();
   }