From fdc253afddbd31e26114fdeaaadd8e4b8cf77297 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Dec 2021 08:19:18 -0800 Subject: [PATCH] update arithmetic contract for unbounded (#5696) Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_solver.cpp | 4 +++- src/smt/theory_lra.cpp | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index f38db0d88..da68691c7 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -986,7 +986,7 @@ namespace arith { IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); SASSERT(lp().ax_is_correct()); - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) { + if (!lp().is_feasible() || lp().has_changed_columns()) { switch (make_feasible()) { case l_false: get_infeasibility_explanation_and_set_conflict(); @@ -1097,6 +1097,8 @@ namespace arith { return l_false; case lp::lp_status::FEASIBLE: case lp::lp_status::OPTIMAL: + case lp::lp_status::UNBOUNDED: + SASSERT(!lp().has_changed_columns()); return l_true; case lp::lp_status::TIME_EXHAUSTED: default: diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9f116cf28..42e98e471 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3460,7 +3460,7 @@ public: st = lp::lp_status::UNBOUNDED; } else { - if (!lp().is_feasible() || lp().has_changed_columns()) + if (!lp().is_feasible() || lp().has_changed_columns()) make_feasible(); vi = get_lpvar(v);