mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-23 18:39:38 +00:00
Code Activity

Remove UNREACHABLE() macros from nra_solver.cpp constraint validation

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-12-16 23:34:55 +00:00
parent c8d5165cac
commit 24769b5ac0
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -231,14 +231,12 @@ struct solver::imp {
if (!check_constraint(ci)) { if (!check_constraint(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n"; IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream())); lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef; return l_undef;
} }
for (auto const &m : m_nla_core.emons()) { for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) { if (!check_monic(m)) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n"; IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream())); lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef; return l_undef;
} }
} }