From 249f3ff2221d88c28faf17e56846009326455606 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 1 Jun 2010 16:39:02 +0000 Subject: [PATCH] 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. --- src/expr/node_builder.h | 2 +- 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& 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(); -- 2.30.2