mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix regression introduced when testing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9a681b1a37
commit
8d0e66b3e3
|
@ -1522,11 +1522,6 @@ lbool core::check() {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
if (no_effect() && params().arith_nl_nra()) {
|
||||
ret = m_nra.check();
|
||||
lp_settings().stats().m_nra_calls++;
|
||||
}
|
||||
|
||||
|
||||
if (no_effect() && should_run_bounded_nlsat())
|
||||
ret = bounded_nlsat();
|
||||
|
|
Loading…
Reference in a new issue