Fixed bug 352

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 70be74442806a1ba5e2dc5ef3fa64ea0f3610dc4..b310de425a28b15b64014e5f37c8be7c95e1bfe2 100644 (file)
--- 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();
   }