diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-09 18:20:04 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-09 18:53:29 -0500 |
| commit | 36ff166f3d2976ad13536de8c699e86d1ff99e65 (patch) | |
| tree | 9b1a3f7ec92dec0ce6b77316355c48f134e36ac2 /src/smt | |
| parent | 90ef0ab1a4e468b47835561118c32bc81bb44b37 (diff) | |
Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ea52f43a7..12ddaee2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3605,8 +3605,8 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { vector<SExpr> sexprs; TypeNode boolType = d_nodeManager->booleanType(); TheoryModel* m = d_theoryEngine->getModel(); - for(AssignmentSet::const_iterator i = d_assignments->begin(), - iend = d_assignments->end(); + for(AssignmentSet::key_iterator i = d_assignments->key_begin(), + iend = d_assignments->key_end(); i != iend; ++i) { Assert((*i).getType() == boolType); |