From 04b0e3c2f74c318d52de5fa7fb3324d95b89bf56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 18:48:52 -0800 Subject: [PATCH] add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326 Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index d92eef5b8..d22ca88db 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3646,6 +3646,9 @@ namespace smt { approx_set::iterator it1 = plbls1.begin(); approx_set::iterator end1 = plbls1.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls1.may_contain(plbl1)); approx_set::iterator it2 = plbls2.begin(); @@ -3687,6 +3690,9 @@ namespace smt { approx_set::iterator it1 = plbls.begin(); approx_set::iterator end1 = plbls.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } unsigned plbl1 = *it1; SASSERT(plbls.may_contain(plbl1)); approx_set::iterator it2 = clbls.begin(); @@ -3706,6 +3712,9 @@ namespace smt { svector::iterator it1 = m_new_patterns.begin(); svector::iterator end1 = m_new_patterns.end(); for (; it1 != end1; ++it1) { + if (m_context.get_cancel_flag()) { + break; + } quantifier * qa = it1->first; app * mp = it1->second; SASSERT(m_ast_manager.is_pattern(mp));