mirror of
https://github.com/Z3Prover/z3
synced 2025-04-18 14:49:01 +00:00
fix #7607
This commit is contained in:
parent
9d8291a75b
commit
a39efbb008
|
@ -1556,6 +1556,8 @@ lbool core::check() {
|
|||
}
|
||||
|
||||
if (no_effect() && params().arith_nl_nra()) {
|
||||
scoped_limits sl(m_reslim);
|
||||
sl.push_child(&m_nra_lim);
|
||||
ret = m_nra.check();
|
||||
lp_settings().stats().m_nra_calls++;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue