From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 6 Jun 2012 19:29:18 +0000 (+0000)
Subject: Fixed assertion failures
X-Git-Tag: cvc5-1.0.0~8116
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35dea35f309952919365ee85f991184bddfda514;p=cvc5.git

Fixed assertion failures
---

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 0c2cccfc6..70be74442 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -112,7 +112,7 @@ void UnconstrainedSimplifier::processUnconstrained()
   bool isSigned;
   bool strict;
   vector<TNode> delayQueueLeft;
-  vector<TNode> delayQueueRight;
+  vector<Node> delayQueueRight;
 
   TNode current = workList.back();
   workList.pop_back();
@@ -527,8 +527,13 @@ void UnconstrainedSimplifier::processUnconstrained()
                 !d_substitutions.hasSubstitution(parent)) {
               ++d_numUnconstrainedElim;
               if (parent[0] != current) {
-                Assert(d_substitutions.hasSubstitution(parent[0]));
-                currentSub = d_substitutions.apply(parent[0]);
+                if (parent[0].isVar()) {
+                  currentSub = parent[0];
+                }
+                else {
+                  Assert(d_substitutions.hasSubstitution(parent[0]));
+                  currentSub = d_substitutions.apply(parent[0]);
+                }
               }
               else if (currentSub.isNull()) {
                 currentSub = current;