From 475af3e5c5b7f95254f1c85668c8b96d75088b19 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Jul 2026 08:45:15 -0700 Subject: [PATCH] opt: drop LP-relaxation infinitesimal on NLA maximize path The nonlinear optimization path (max_with_nl) returned the linear-relaxation optimum lp_val including its infinitesimal. That infinitesimal is an artifact of the strict bounds introduced by the linearization, not a genuine strict optimum of the nonlinear problem. Threading it into opt_solver::mk_ge made theory_lra assert a delta-rational lower bound (r, -1) that coincides with the column's existing strict upper bound (r, -1), fixing the objective column at a delta value the LP core never snapped, tripping the non_basic_columns_are_set_correctly assertion in a debug build (unit tests max_reg / max_rev). Project the infinitesimal away in both NLA branches (FC_DONE and FC_CONTINUE); the rational part remains a sound bound for check_bound to validate. The genuinely-strict, NLA-free path (e.g. pure LP suprema and shared-symbol/EUF objectives) is unaffected, so faithful validation of strict optima is preserved. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/theory_lra.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 34243c7717..b878d7e231 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -4068,11 +4068,22 @@ public: tout << " x[" << j << "] = " << lp().get_column_value(j) << "\n"; } }); + // Discard the infinitesimal of the value returned from the NLA path. + // When NLA is involved the objective is nonlinear, so lp_val is the + // optimum of the LINEAR relaxation: its infinitesimal comes from the + // strict bounds introduced by the linearization, not from a genuine + // strict optimum of the nonlinear problem. If it were kept, + // opt_solver::mk_ge would assert a delta-rational bound (r, -1) that the + // real problem cannot honor, fixing the objective column at a delta + // value the LP core cannot snap on the next solve (assertion + // non_basic_columns_are_set_correctly). The rational part remains a + // sound bound for the optimizer to validate via check_bound. + inf_eps lp_val_no_eps(lp_val.get_infinity(), inf_rational(lp_val.get_rational())); switch (nla_st) { case FC_DONE: // NLA satisfied: keep the optimal assignment, return LP value blocker = mk_gt(v); - result = lp_val; + result = lp_val_no_eps; st = lp::lp_status::FEASIBLE; return true; case FC_CONTINUE: @@ -4081,7 +4092,7 @@ public: // as a bound for the optimizer to validate via check_bound(). lp().restore_x(); blocker = mk_gt(v, lp_ival); - result = lp_val; + result = lp_val_no_eps; st = lp::lp_status::FEASIBLE; return true; case FC_GIVEUP: