Fixed a bug in partial_model.cpp where the data was immediately deallocated before being used. Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.

2 files changed, 4 insertions, 9 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index cefeb2fe2..fcc6bb364 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -372,8 +372,8 @@ protected:
         // NodeBuilder.
         throw std::bad_alloc();
       }
-      d_nvMaxChildren = d_nv->d_nchildren;
       d_nv = newBlock;
+      d_nvMaxChildren = d_nv->d_nchildren;
     }
   }
 
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index c5eb0ad1d..4b113257c 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -203,20 +203,15 @@ void ArithPartialModel::beginRecordingAssignments(){
 void ArithPartialModel::stopRecordingAssignments(bool revert){
   Assert(d_savingAssignments);
 
-  d_savingAssignments = false;
+  d_savingAssignments = false; //
 
   if(revert){
     while(!d_history.empty()){
       pair<TNode, DeltaRational>& curr = d_history.back();
-      d_history.pop_back();
-
-      TNode x = curr.first;
 
-      DeltaRational* c;
-      bool hasAssignment = x.getAttribute(partial_model::Assignment(), c);
-      Assert(hasAssignment);
+      setAssignment(curr.first,curr.second);
 
-      *c = curr.second;
+      d_history.pop_back();
     }
   }else{
     d_history.clear();