mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 06:37:49 +00:00
Code Activity

fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-02-27 12:29:14 -10:00
parent ffe29b1433
commit 6ec40153cc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -4013,10 +4013,10 @@ public:
if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) { if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
switch (check_nla(level)) { switch (check_nla(level)) {
case FC_DONE: case FC_DONE:
case FC_CONTINUE:
st = lp::lp_status::FEASIBLE; st = lp::lp_status::FEASIBLE;
break; break;
case FC_GIVEUP: case FC_GIVEUP:
case FC_CONTINUE:
st = lp::lp_status::UNBOUNDED; st = lp::lp_status::UNBOUNDED;
break; break;
} }