From 1f425824ff78a3595cbef01f9a9cdf9c6a9c8e16 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 23 May 2017 15:46:53 -0700
Subject: [PATCH] adding stub check_int_feasibility()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lar_solver.cpp | 4 ++++
 src/util/lp/lar_solver.h   | 3 ++-
 src/util/lp/lp_settings.h  | 7 +++++++
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 18b901104..b6315fe5c 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1380,6 +1380,10 @@ void lar_solver::shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_
     quick_xplain::run(explanation, *this);
     lean_assert(this->explanation_is_correct(explanation));
 }
+
+final_check_status check_int_feasibility() {
+	return final_check_status::GIVEUP;
+}
 } // namespace lean
 
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index bd0fe8fac..6fba62fe8 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -401,6 +401,7 @@ public:
         unsigned ext_var = m_columns_to_ext_vars_or_term_indices[j];
         return m_ext_vars_to_columns.find(ext_var)->second.is_integer();
     }
-    inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }
+    inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }	
+	final_check_status check_int_feasibility();
 };
 }
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index 6b6aba2ad..c081a84ff 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -16,6 +16,13 @@ namespace lean {
 typedef unsigned var_index;
 typedef unsigned constraint_index;
 typedef unsigned row_index;
+
+enum class final_check_status {
+	DONE,
+	CONTINUE,
+	GIVEUP
+};
+
 enum class column_type  {
     free_column = 0,
         low_bound = 1,