From 06faf03eaae495cef945a413d64928b92e73bfa4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 2 Oct 2024 16:07:49 -0700
Subject: [PATCH] use cuts from proofs, remove gcc warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/dioph_eq.cpp   | 10 ++++------
 src/math/lp/int_solver.cpp |  4 +---
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 93dffc76f..db5b725c1 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -256,7 +256,7 @@ namespace lp {
                 if (lra.settings().stats().m_dio_conflicts % lra.settings().dio_cut_from_proof_period() == 0) {
                     // prepare int_solver for reporting
                     lar_term& t = lia.get_term();
-                    for (auto& p: ep.m_e) {
+                    for (const auto& p: ep.m_e) {
                         t.add_monomial(p.coeff()/g, p.j());
                     }
                     lia.offset() = floor(-new_c);
@@ -407,7 +407,7 @@ namespace lp {
             bool is_strict;
             u_dependency *b_dep = nullptr;
             if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
-                if (t.c() > rs || is_strict && t.c() == rs) {
+                if (t.c() > rs || (is_strict && t.c() == rs)) {
                     for (const auto& p: lra.flatten(dep)) {
                         m_infeas_explanation.push_back(p);
                     }
@@ -418,7 +418,7 @@ namespace lp {
                 }
             }
             if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
-                if (t.c() < rs || is_strict && t.c() == rs) {
+                if (t.c() < rs || (is_strict && t.c() == rs)) {
                     for (const auto& p: lra.flatten(dep)) {
                         m_infeas_explanation.push_back(p);
                     }
@@ -521,9 +521,8 @@ namespace lp {
                 term_o& e = m_eprime[e_index].m_e;
                 if (!e.contains(k)) continue;
 
-                const mpq& k_coeff = e.get_coeff(k);
                 TRACE("dioph_eq", print_eprime_entry(e_index, tout << "before:") << std::endl;
-                      tout << "k_coeff:" << k_coeff << std::endl;);
+                      tout << "k_coeff:" << e.get_coeff(k) << std::endl;);
 
 /*
                 if (!l_term.is_empty()) {
@@ -684,7 +683,6 @@ namespace lp {
             SASSERT(ex.empty());
             TRACE("dioph_eq", tout << "conflict:"; print_eprime_entry(m_conflict_index, tout) << std::endl;);
             auto & ep = m_eprime[m_conflict_index];
-            u_dependency* dep = nullptr;
             /*
               for (const auto & pl : ep.m_l) {
               unsigned row_index = pl.j();
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 3fe939170..216ad1026 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -231,12 +231,10 @@ namespace lp {
             ++m_number_of_calls;
             if (r == lia_move::undef) r = patch_basic_columns();
             if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)();
-            if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
             if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
             if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
-
             if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2);
-
+            if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();
             if (r == lia_move::undef) r = int_branch(lia)();
             if (settings().get_cancel_flag()) r = lia_move::undef;        
             return r;