mirror of
https://github.com/Z3Prover/z3
synced 2026-05-03 00:45:15 +00:00
refine givup conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b8b6d96fba
commit
e76d477ab0
1 changed files with 1 additions and 2 deletions
|
|
@ -4168,10 +4168,9 @@ namespace smt {
|
||||||
break;
|
break;
|
||||||
case FC_CONTINUE:
|
case FC_CONTINUE:
|
||||||
return FC_CONTINUE;
|
return FC_CONTINUE;
|
||||||
break;
|
|
||||||
}
|
}
|
||||||
if (m_final_check_idx == old_idx) {
|
if (m_final_check_idx == old_idx) {
|
||||||
if (level >= max_level)
|
if (level >= max_level || result == FC_DONE || can_propagate())
|
||||||
break;
|
break;
|
||||||
++level;
|
++level;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue