Only call bounded_nlsat before the lemma return when the to-refine
set contains real (non-integer) monomials. Integer NLA problems are
better served by the lemma pipeline; calling nlsat drains the rlimit
budget without benefit. For real NLA (QF_NRA, QF_UFNRA, QF_NIRA with
reals), nlsat via CAD is the right approach when bounds propagation
is not converging.
Remove the arith.nl.nra_before_lemma_return parameter since the
has_real_monomial() gate is precise enough.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The unconditional early call drained rlimit budget on QF_NIA problems
where nlsat returns l_undef. Only try early nlsat every arith.nl.delay
(default 10) NLA calls, combined with the existing exponential backoff.
This preserves the benefit for stuck QF_NRA problems while reducing
overhead on problems where the lemma pipeline is effective.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When monomial_bounds.propagate() generates interval-refinement lemmas,
bounded_nlsat() was blocked by the no_effect() gate and never reached.
This caused timeouts on QF_NRA/QF_NIRA/QF_UFNRA problems that nlsat
can solve directly via cylindrical algebraic decomposition.
The new parameter (default true) moves the bounded_nlsat() call before
the early lemma return, allowing nlsat a chance to solve the problem.
Set to false to restore the old behavior.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The IF_VERBOSE(0,...) block at line 498 in q_mbi.cpp used operator[]
on values2root map which asserts the key exists. When the model
evaluation of the inverted term produces a value not present in the
EUF values2root map, this crashes.
Use find() instead to handle the missing key gracefully, since this
is diagnostic output and the missing key is expected when the model
inversion produces inconsistent results.
Fixes assertion violation from #7027 (obj_hashtable.h line 168/174)
with forall/array/eq2ineq combination.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Three bugs in the def ref-counting infrastructure:
1. dec_ref() incremented (++) instead of decrementing (--) the ref count,
so objects were never freed.
2. def_ref lacked copy and move constructors, so the compiler-generated
default copy just copied the raw pointer without inc_ref. This caused
use-after-free when def_ref values were copied into vectors.
3. Compound def types (add_def, mul_def, div_def) lacked destructors to
dec_ref their children. Added virtual destructor to base def class
and child-releasing destructors to compound types.
Fixes the memory leak from #7027 (model_based_opt.cpp:81).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add internalize_overflow() to handle OP_BUMUL_OVFL, OP_BSMUL_OVFL,
OP_BUADD_OVFL, OP_BSADD_OVFL, OP_BUSUB_OVFL, OP_BSSUB_OVFL,
OP_BSDIV_OVFL, and OP_BNEG_OVFL in the sat.euf=true solver path.
Previously these overflow predicates hit UNREACHABLE() in
internalize_circuit(). Now they are reduced to equivalent expressions
using existing BV operations and internalized via add_def().
Fixes the assertion violation from #7027 for bvuaddo and related
overflow predicates with tactic.default_tactic=smt sat.euf=true.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When check_nla returns FC_CONTINUE it means NLA found constraint
violations and added lemmas. The current LP value is a valid lower
bound, so the status should be FEASIBLE, not UNBOUNDED.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add checkpoint() call in gcd_prs() main loop so polynomial GCD
computation respects rlimit/timeout. Add cancellation callback to
HNF calculation so it can be interrupted when the solver is cancelled.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.
Two changes:
1. is_non_negative: detect products where unpaired factors are
consecutive integer expressions (differ by exactly 1), handling
both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
to multiplication expressions to avoid disrupting other theories
Also adds regression tests for the new simplification.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
