mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
simplify condition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3ef05ced2f
commit
7714bff6b2
|
@ -33,16 +33,13 @@ namespace smt {
|
|||
unsigned thread_max_conflicts = ctx.get_fparams().m_threads_max_conflicts;
|
||||
unsigned max_conflicts = ctx.get_fparams().m_max_conflicts;
|
||||
|
||||
#if 1
|
||||
// try first sequential with a low conflict budget to make super easy problems cheap
|
||||
ctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, 40u);
|
||||
unsigned max_c = std::min(thread_max_conflicts, 40u);
|
||||
ctx.get_fparams().m_max_conflicts = max_c;
|
||||
result = ctx.check(asms.size(), asms.c_ptr());
|
||||
if (result != l_undef || (result == l_undef && ctx.m_num_conflicts < ctx.get_fparams().m_max_conflicts)) {
|
||||
if (result != l_undef || ctx.m_num_conflicts < max_c) {
|
||||
return result;
|
||||
}
|
||||
#else
|
||||
ctx.internalize_assertions();
|
||||
#endif
|
||||
|
||||
enum par_exception_kind {
|
||||
DEFAULT_EX,
|
||||
|
|
Loading…
Reference in a new issue