diff options
| -rw-r--r-- | src/expr/node_builder.h | 2 | ||||
| -rw-r--r-- | src/theory/arith/partial_model.cpp | 11 |
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(); |