mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-17 18:48:52 -08:00
parent d6d301c5eb
commit 04b0e3c2f7
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/mam.cpp
View file

@ -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<qp_pair>::iterator it1 = m_new_patterns.begin();
svector<qp_pair>::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));