From 167969d6c2148b274749eaa98967862912e59d61 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 07:52:36 -0700
Subject: [PATCH] remove debug/non-debug difference

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp     |  2 --
 src/util/lp/hnf_cutter.h   | 28 +++++++++++++---------------
 src/util/lp/int_solver.cpp | 26 ++++++++++++++++++--------
 3 files changed, 31 insertions(+), 25 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3bdd2d784..ff5b72159 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2712,7 +2712,6 @@ public:
         if (dump_lemmas()) {
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
             (void)id;
-            //SASSERT(id != 55);
         }
     }
 
@@ -2732,7 +2731,6 @@ public:
         if (dump_lemmas()) {                
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
             (void)id;
-            // SASSERT(id != 71);
         }
     }
 
diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h
index dff0b8ef8..9a06e1bc9 100644
--- a/src/util/lp/hnf_cutter.h
+++ b/src/util/lp/hnf_cutter.h
@@ -177,43 +177,41 @@ public:
 
     bool overflow() const { return m_overflow; }
     
-    lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper
-                        #ifdef Z3DEBUG
-                        ,
-                        const vector<mpq> & x0
-                        #endif
-                        ) {
+    lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
         // we suppose that x0 has at least one non integer element 
+        (void)x0;
+
         init_matrix_A();
         svector<unsigned> basis_rows;
         mpq big_number = m_abs_max.expt(3);
         mpq d = hnf_calc::determinant_of_rectangular_matrix(m_A, basis_rows, big_number);
         
-        //        std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
-        //std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
+        // std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
+        // std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
 
         if (d >= big_number) {
             return lia_move::undef;
         }
         
-        if (m_settings.get_cancel_flag())
+        if (m_settings.get_cancel_flag()) {
             return lia_move::undef;
+        }
+
         if (basis_rows.size() < m_A.row_count()) {
             m_A.shrink_to_rank(basis_rows);
             shrink_explanation(basis_rows);
         }
         
-        hnf<general_matrix> h(m_A, d);
-        //  general_matrix A_orig = m_A;
-        
+        hnf<general_matrix> h(m_A, d);        
         vector<mpq> b = create_b(basis_rows);
         lp_assert(m_A * x0 == b);
-        // vector<mpq> bcopy = b;
         find_h_minus_1_b(h.W(), b);
-        // lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
         int cut_row = find_cut_row_index(b);
-        if (cut_row == -1)
+
+        if (cut_row == -1) {
             return lia_move::undef;
+        }
+
         // the matrix is not square - we can get
         // all integers in b's projection
         
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index f49ecabfd..8bc2056b4 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -577,17 +577,27 @@ lia_move int_solver::make_hnf_cut() {
         return lia_move::undef;
     }
     settings().st().m_hnf_cutter_calls++;
-    TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls;);
+    TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
+          for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+              m_lar_solver->print_constraint(i, tout);
+          }              
+          m_lar_solver->print_constraints(tout);
+          );
 #ifdef Z3DEBUG
     vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
+#else
+    vector<mpq> x0;
 #endif
-    lia_move r =  m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper
-#ifdef Z3DEBUG
-                                          , x0
-#endif
-                                          );
-    CTRACE("hnf_cut", r == lia_move::cut, tout<< "cut:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
-    if (r == lia_move::cut) {        
+    lia_move r =  m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
+
+    if (r == lia_move::cut) {      
+        TRACE("hnf_cut",
+              m_lar_solver->print_term(*m_t, tout << "cut:"); 
+              tout << " <= " << *m_k << std::endl;
+              for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+                  m_lar_solver->print_constraint(i, tout);
+              }              
+              );
         lp_assert(current_solution_is_inf_on_cut());
         settings().st().m_hnf_cuts++;
         m_ex->clear();