From 022a5e927ecab4f217b3f26529b09e569bd35d94 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 11 Jun 2012 11:43:55 +0000
Subject: [PATCH] Fixed bug 352

---
 src/theory/unconstrained_simplifier.cpp | 6 ++++--
 1 file 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();
   }
-- 
2.30.2