diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-01 16:39:02 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-01 16:39:02 +0000 |
commit | 249f3ff2221d88c28faf17e56846009326455606 (patch) | |
tree | fc6160a300c23a40478c900b1782fc018833fee5 | |
parent | aad6d724f09fe523d7c1d53e2db959801f28fc3e (diff) |
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.
-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(); |