From 53c95e3627325dcae5a01cd3e01ec3f2c301a7e4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 27 Dec 2023 15:18:48 -1000
Subject: [PATCH] cleanup

---
 src/math/lp/gomory.cpp    | 6 +++---
 src/math/lp/lp_settings.h | 1 -
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index f5331ea0571..89f518eeef3 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -261,7 +261,7 @@ struct create_cut {
 
     lia_move cut() {
         TRACE("gomory_cut", dump(tout););
-        m_polarity = 0; // 0: means undefined, 1, -1: the polar case, 2: the mixed case
+        m_polarity = 0; // 0: means undefined, +-1, the polar case, 2: the mixed case
         // gomory cut will be  m_t >= m_k and the current solution has a property m_t < m_k
         m_k = 1;
         m_t.clear();
@@ -338,7 +338,7 @@ struct create_cut {
         TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut: "); tout << " >= " << m_k << std::endl;);
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);
               lia.lra.display(tout));
-        SASSERT(lia.current_solution_is_inf_on_cut());  // checks that indices are columns
+        SASSERT(lia.current_solution_is_inf_on_cut());
               
         lia.settings().stats().m_gomory_cuts++;
         return lia_move::cut;
@@ -522,9 +522,9 @@ struct create_cut {
         struct polar_info {lpvar j; int polarity;  u_dependency *dep;};
         vector<polar_info> polar_vars;
         unsigned_vector columns_for_cuts = gomory_select_int_infeasible_vars(num_cuts);
+        bool has_small_cut = false;
 
         // define inline helper functions
-        bool has_small_cut = false;
         auto is_small_cut = [&](lar_term const& t) {
             return all_of(t, [&](auto ci) { return ci.coeff().is_small(); });
         };
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index fef30cb6ddc..2bed1b1afad 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -215,7 +215,6 @@ struct lp_settings {
     bool             backup_costs = true;
     unsigned         column_number_threshold_for_using_lu_in_lar_solver = 4000;
     unsigned         m_int_gomory_cut_period = 4;
-    bool             m_gomory_simpliy = false;
     unsigned         m_int_find_cube_period = 4;
 private:
     unsigned         m_hnf_cut_period = 4;