From 36ff166f3d2976ad13536de8c699e86d1ff99e65 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 9 Nov 2014 18:20:04 -0500 Subject: [PATCH] Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac). --- src/smt/smt_engine.cpp | 4 ++-- 1 file 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 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); -- 2.30.2