From 6ec40153cc097cec07c36a746d2ccc32e472a805 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Feb 2026 12:29:14 -1000 Subject: [PATCH] fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize 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> --- src/smt/theory_lra.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b5f249a00..05053f4ea 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -4013,10 +4013,10 @@ public: if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) { switch (check_nla(level)) { case FC_DONE: + case FC_CONTINUE: st = lp::lp_status::FEASIBLE; break; case FC_GIVEUP: - case FC_CONTINUE: st = lp::lp_status::UNBOUNDED; break; }