diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-06 19:29:18 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-06 19:29:18 +0000 |
commit | 35dea35f309952919365ee85f991184bddfda514 (patch) | |
tree | 6d4336e070e050abb577175b1e61d5950cf877cf /src/theory/unconstrained_simplifier.cpp | |
parent | 27ccab68a41bb39f08d7867b53da2215f251144d (diff) |
Fixed assertion failures
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
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; |