diff options
author | Tim King <taking@google.com> | 2015-10-23 15:43:27 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-10-23 19:14:18 -0700 |
commit | 39ee90e08fd60bfc31218a5dcfbd4dadf8845921 (patch) | |
tree | b7728388ac5579089262371a22eadc0eee0a30ef /src/theory/unconstrained_simplifier.cpp | |
parent | 3a67d649379f20000b2416b02860aa057ac38607 (diff) |
This removes a bug for reading data that has been popped from the back of a vector using a stale reference in the unconstrained simplifier.
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 244cb303d..997c998e6 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -57,9 +57,9 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) while (!toVisit.empty()) { // The current node we are processing - unc_preprocess_stack_element& stackHead = toVisit.back(); + TNode current = toVisit.back().node; + TNode parent = toVisit.back().parent; toVisit.pop_back(); - TNode current = stackHead.node; TNodeCountMap::iterator find = d_visited.find(current); if (find != d_visited.end()) { @@ -74,7 +74,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) } d_visited[current] = 1; - d_visitedOnce[current] = stackHead.parent; + d_visitedOnce[current] = parent; if (current.getNumChildren() == 0) { if (current.isVar()) { |