From 8a146a92ec64c70ee07cab1b81c52f3b5d1ecc93 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 6 Mar 2026 08:54:34 -1000 Subject: [PATCH] fix: replace UNREACHABLE with VERIFY for non-COI constraint/monic violations in nra_solver 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> --- src/math/lp/nra_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index dae20dc69..bfedd12e4 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -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; } }