From 7714bff6b2225ab65346eb1dfc4ee3e7cb03ea77 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Feb 2020 19:49:12 -0800 Subject: [PATCH] simplify condition Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 70979372f..a9eeef401 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -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,