From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 11 Jun 2012 11:43:55 +0000 (+0000)
Subject: Fixed bug 352
X-Git-Tag: cvc5-1.0.0~8090
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=022a5e927ecab4f217b3f26529b09e569bd35d94;p=cvc5.git

Fixed bug 352
---

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();
   }