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.

1 files changed, 3 insertions, 8 deletions

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