mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

check cancel flag after bcp. BCP returns in incomplete state after it check's the cancel flag. Propagate returns 'true' in this case so that the main loop exits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-02 14:33:42 -07:00
parent e57e5328ce
commit d03a4bc306
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -1615,6 +1615,8 @@ namespace smt {
unsigned qhead = m_qhead; unsigned qhead = m_qhead;
if (!bcp()) if (!bcp())
return false; return false;
if (m_cancel_flag)
return true;
SASSERT(!inconsistent()); SASSERT(!inconsistent());
propagate_relevancy(qhead); propagate_relevancy(qhead);
if (inconsistent()) if (inconsistent())