From: Tim King <taking@google.com>
Date: Fri, 23 Oct 2015 22:43:27 +0000 (-0700)
Subject: This removes a bug for reading data that has been popped from the back of a vector... 
X-Git-Tag: cvc5-1.0.0~6191
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39ee90e08fd60bfc31218a5dcfbd4dadf8845921;p=cvc5.git

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.
---

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