From 39ee90e08fd60bfc31218a5dcfbd4dadf8845921 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 23 Oct 2015 15:43:27 -0700 Subject: [PATCH] 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. --- src/theory/unconstrained_simplifier.cpp | 6 +++--- 1 file 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()) { -- 2.30.2