From 752f08c9d6ca9eeefc6837db5b0a57583edd1326 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Nov 2020 00:02:19 -0800 Subject: [PATCH] check_feasible is called after column is added for fixed variable Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 45340ba0d..57d929c21 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -914,7 +914,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().get_status() != lp::lp_status::OPTIMAL) { switch (make_feasible()) { case l_false: get_infeasibility_explanation_and_set_conflict();