The optimizer's simplification pass did not expand products of sums
into sum-of-monomials form. This caused mathematically equivalent
expressions like (5-x)^2 vs (x-5)^2 to simplify into different
internal forms, where the former produced nested multiplies
(+ 5.0 (* -1.0 x)) that led to harder purification constraints
and solver timeouts.
Enabling som=true in the first simplification tactic normalizes
polynomial objectives into canonical monomial form, making the
optimizer robust to operand ordering.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Same as test_bnh_optimize but constructs f1 and f2 with reversed
parameter order in mk_add, mk_mul, mk_sub calls. Exposes optimizer
sensitivity to expression structure.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
**Root cause**: `vector::resize(SZ s, Args args...)` in `src/util/vector.h` took `args` by value and used `std::forward<Args>(args)` in a loop. The first iteration moved from `args`, leaving all subsequent elements with a moved-from state (`rational{0/0}` instead of
`rational{0/1}`). This corrupted the coefficient vector in the pretty printer, causing a division-by-zero assertion when multiplying.
**Fix**: Changed `resize` to take `Args const& args` and copy-construct each element instead of forwarding/moving.
- Add ENSURE(result == Z3_L_TRUE) for each BNH optimization call and
ENSURE(num_sat == 7) at the end so CI catches regressions.
- Remove test_bnh_optimize() from tst_api() to avoid duplicate
execution under /a; keep standalone tst_bnh_opt() entry point.
- Fix Test 2 comment: it tests same-size backup, not backup-longer.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Relax restore_x() to handle backup/current size mismatches: when
backup is shorter (new columns added), call
move_non_basic_columns_to_bounds() to find a feasible solution.
- Fix 100x performance regression in nonlinear optimization: save LP
optimum before check_nla and return it as bound regardless of NLA
result, so opt_solver::check_bound() can validate via full re-solve
with accumulated NLA lemmas.
- Refactor theory_lra::maximize() into three helpers: max_with_lp(),
max_with_nl(), and max_result().
- Add mk_gt(theory_var, impq const&) overload for building blockers
from saved LP optimum values.
- Add BNH multi-objective optimization test (7/7 sat in <1s vs 1/7
in 30s before fix).
- Add restore_x test for backup size mismatch handling.
Fixes#8890
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The NRA solver's check() uses cone-of-influence (COI) to select a subset
of constraints for nlsat. When nlsat returns l_true, the model is validated
against all constraints, but non-COI constraints can legitimately be
violated since nlsat only solved over the COI subset.
- Non-COI violations gracefully return l_undef (fallback to other strategies)
- COI violations still trigger an assertion (indicating a real nlsat bug)
Fixes#8883
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>
