diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index f5cc61ba9e..8fb383d475 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -240,16 +240,26 @@ struct solver::imp { lra.init_model(); for (lp::constraint_index ci : lra.constraints().indices()) if (!check_constraint(ci)) { - IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); + // nlsat only solves over the cone-of-influence (COI) subset + // of constraints, so constraints outside the COI may be + // legitimately violated by the nlsat model. Only a violation + // of a COI constraint indicates a genuine nlsat bug; a + // non-COI violation is benign, so fall back to l_undef + // quietly without emitting diagnostics. + if (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)) { - IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; - lra.constraints().display(verbose_stream())); - UNREACHABLE(); + if (m_coi.mons().contains(m.var())) { + IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; + lra.constraints().display(verbose_stream())); + UNREACHABLE(); + } return l_undef; } }