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 /src/theory/arith/partial_model.cpp | |
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.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 11 |
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(); |