From ef2cdc226aba110804187c94bffd75c515243752 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Thu, 26 Jul 2018 22:46:28 -0700
Subject: [PATCH] a fix in maximize_term

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/int_solver.h   |  1 -
 src/util/lp/lar_solver.cpp |  5 ++++-
 src/util/lp/lia_move.h     | 21 +++++++++++++++++++++
 3 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index 65c818d1e..ec708918d 100644
--- a/src/util/lp/int_solver.h
+++ b/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;
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 041b49389..0cfdc33b4 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/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) {
diff --git a/src/util/lp/lia_move.h b/src/util/lp/lia_move.h
index ec4643e20..65da5826e 100644
--- a/src/util/lp/lia_move.h
+++ b/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";
+}
 }