mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 19:53:34 +00:00
fix #3236 - fix also max conflict overwrite for incremental mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c49d0c5033
commit
59acd1093d
|
@ -35,7 +35,7 @@ namespace smt {
|
|||
|
||||
// try first sequential with a low conflict budget to make super easy problems cheap
|
||||
unsigned max_c = std::min(thread_max_conflicts, 40u);
|
||||
ctx.get_fparams().m_max_conflicts = max_c;
|
||||
flet<unsigned> _mc(ctx.get_fparams().m_max_conflicts, max_c);
|
||||
result = ctx.check(asms.size(), asms.c_ptr());
|
||||
if (result != l_undef || ctx.m_num_conflicts < max_c) {
|
||||
return result;
|
||||
|
|
Loading…
Reference in a new issue