Fixed a bug in partial_model.cpp where the data was immediately deallocated before...

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index cefeb2fe2d82971d04f098cc5e371406d0555da0..fcc6bb3645691ae1a8e362bd8f07bf4e63217c55 100644 (file)
--- 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 c5eb0ad1d4ebafd4113ac8ee7ee5cfddd582554c..4b113257c657a2dcf2d7249bb6b9bf531eb56726 100644 (file)
--- 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();