mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-06 21:34:53 +00:00
Code Activity

fix: replace UNREACHABLE with VERIFY for non-COI constraint/monic violations in nra_solver

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-03-06 08:54:34 -10:00
parent 84a7566c3a
commit 8a146a92ec
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nra_solver.cpp
View file

@ -241,16 +241,16 @@ struct solver::imp {
lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
VERIFY(!m_coi.constraints().contains(ci));
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) {
VERIFY(!m_coi.mons().contains(m.var()));
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
}