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.

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()) {