From ee4ed1749af2f6a746dd6395b4fbedbcff405af4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Dec 2015 09:09:25 -0800 Subject: [PATCH] add cancel checks in model finder, patch by Sarah Winkler Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index e4a34d3db..08cf34e72 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1744,7 +1744,7 @@ namespace smt { // when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver. // in this case, the quantifier_info stores the instantiation sets. ptr_vector * m_uvar_inst_sets; - bool m_cancel; + volatile bool m_cancel; friend class quantifier_analyzer; @@ -1893,8 +1893,10 @@ namespace smt { (*it)->populate_inst_sets(m_flat_q, s, ctx); // second pass it = m_qinfo_vect.begin(); - for (; it != end; ++it) + for (; it != end; ++it) { + checkpoint(); (*it)->populate_inst_sets2(m_flat_q, s, ctx); + } } func_decl_set const & get_ng_decls() const { @@ -3593,6 +3595,10 @@ namespace smt { void model_finder::set_cancel(bool f) { m_cancel = f; m_analyzer->set_cancel(f); + obj_map::iterator it = m_q2info.begin(); + obj_map::iterator end = m_q2info.end(); + for (; it != end; ++it) + (*it).m_value->set_cancel(f); } };