a fix in maximize_term

Signed-off-by: Lev <levnach@hotmail.com>

src/util/lp/int_solver.h

@@ -50,7 +50,6 @@ public:
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
     lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper);
-    lia_move check_(lar_term& t, mpq& k, explanation& ex, bool & upper);
     bool move_non_basic_column_to_bounds(unsigned j);
     lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);    
     bool is_base(unsigned j) const;

src/util/lp/lar_solver.cpp

@@ -542,8 +542,11 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
                 return lp_status::FEASIBLE; // it should not happen
         }
         m_int_solver->patch_nbasic_column(j, false);
-        if (!column_value_is_integer(j))
+        if (!column_value_is_integer(j)) {
+            term_max = prev_value;
+            m_mpq_lar_core_solver.m_r_x = backup;
             return lp_status::FEASIBLE;
+        }
         change = true;
     }
     if (change) {

src/util/lp/lia_move.h

@@ -28,4 +28,25 @@ enum class lia_move {
     undef,
     unsat
 };
+inline std::string lia_move_to_string(lia_move m) {
+    switch (m) {
+    case lia_move::sat:
+        return "sat";
+    case lia_move::branch:
+        return "branch";
+    case lia_move::cut:
+        return "cut";
+    case lia_move::conflict:
+        return "conflict";
+    case lia_move::continue_with_check:
+        return "continue_with_check";
+    case lia_move::undef:
+        return "undef";
+    case lia_move::unsat:
+        return "unsat";
+    default:
+        lp_assert(false);
+    };
+    return "strange";
+}
 }