diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 27abac072..c0119f7f1 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -496,7 +496,7 @@ public:
         auto _check_feasible = [&](void) {
             lra.find_feasible_solution();
             if (!lra.is_feasible() && !lia.settings().get_cancel_flag()) {
-                lra.get_infeasibility_explanation(*(lia.explanation()));
+                lra.get_infeasibility_explanation(*(lia.expl()));
                 return false;
             }
             return true;
@@ -507,7 +507,7 @@ public:
             SASSERT(is_gomory_cut_target(j));
             unsigned row_index = lia.row_of_basic_column(j);
             const row_strip<mpq>& row = lra.get_row(row_index);
-            create_cut cc(lia.get_term(), lia.offset(), lia.explanation(), j, row, lia);
+            create_cut cc(lia.get_term(), lia.offset(), lia.expl(), j, row, lia);
             auto r = cc.cut();
             if (r != lia_move::cut) {
                 if (r == lia_move::conflict)
diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
index d4ba12809..192be557d 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -260,7 +260,7 @@ branch y_i >= ceil(y0_i) is impossible.
 #ifdef Z3DEBUG
         vector<mpq> x0 = transform_to_local_columns(lra.r_x());
 #endif
-        lia_move r =  create_cut(lia.get_term(), lia.offset(), lia.explanation(), lia.is_upper()
+        lia_move r =  create_cut(lia.get_term(), lia.offset(), lia.expl(), lia.is_upper()
 #ifdef Z3DEBUG
                                  , x0
 #endif
@@ -276,10 +276,10 @@ branch y_i >= ceil(y0_i) is impossible.
                   );
             lp_assert(lia.current_solution_is_inf_on_cut());
             lia.settings().stats().m_hnf_cuts++;
-            lia.explanation()->clear();        
+            lia.expl()->clear();        
             for (u_dependency* dep : constraints_for_explanation()) 
                 for (auto ci : lia.lra.flatten(dep))
-                    lia.explanation()->push_back(ci);            
+                    lia.expl()->push_back(ci);            
         } 
         return r;
     }
diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp
index 9573b122c..086424c79 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -252,7 +252,7 @@ namespace lp {
     void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
         auto* deps = lra.get_bound_constraint_witnesses_for_column(j);
         for (auto d : lra.flatten(deps))
-            lia.explanation()->push_back(d);
+            lia.expl()->push_back(d);
     }
 
     bool int_gcd_test::accumulate_parity(const row_strip<mpq> & row, unsigned least_idx) {
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 3f402ec07..7854fde58 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -873,7 +873,7 @@ namespace lp {
     
     bool int_solver::is_upper() const { return m_imp->m_upper; }
     bool& int_solver::is_upper() { return m_imp->m_upper; }
-    explanation* int_solver::explanation() { return m_imp->m_ex; }
+    explanation* int_solver::expl() { return m_imp->m_ex; }
     bool int_solver::column_is_int_inf(unsigned j) const {
         return m_imp->column_is_int_inf(j);
     }
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index 452889d7f..64d452196 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -45,6 +45,20 @@ class int_solver {
     lar_core_solver&    lrac;
     imp*                m_imp; 
     vector<equality>       m_equalities;
+    bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
+    bool is_boxed(unsigned j) const;
+    bool is_free(unsigned j) const;
+    bool value_is_int(unsigned j) const;
+    bool is_feasible() const;
+    bool column_is_int_inf(unsigned j) const;
+    std::ostream& display_inf_rows(std::ostream&) const;
+   
+    lp_settings& settings();
+    const lp_settings& settings() const;
+    bool at_bound(unsigned j) const;
+    bool has_lower(unsigned j) const;
+    bool has_upper(unsigned j) const;
+    unsigned row_of_basic_column(unsigned j) const;
 public:
     int_solver(lar_solver& lp);
     ~int_solver();
@@ -66,26 +80,6 @@ public:
     bool at_upper(unsigned j) const;
     void simplify(std::function<bool(unsigned)>& is_root);
     vector<equality> const& equalities() const { return m_equalities; }
-
-private:
-    // lia_move patch_nbasic_columns();
-    bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
-    bool is_boxed(unsigned j) const;
-    bool is_free(unsigned j) const;
-    bool value_is_int(unsigned j) const;
-    bool is_feasible() const;
-    bool column_is_int_inf(unsigned j) const;
-    std::ostream& display_inf_rows(std::ostream&) const;
-   
-    lp_settings& settings();
-    const lp_settings& settings() const;
-    bool at_bound(unsigned j) const;
-    bool has_lower(unsigned j) const;
-    bool has_upper(unsigned j) const;
-    unsigned row_of_basic_column(unsigned j) const;
-   
-        
-public:
     bool is_fixed(unsigned j) const;
     std::ostream& display_column(std::ostream & out, unsigned j) const;
     u_dependency* column_upper_bound_constraint(unsigned j) const;
@@ -95,11 +89,9 @@ public:
     bool shift_var(unsigned j, unsigned range);
     std::ostream&  display_row_info(std::ostream & out, unsigned row_index) const;
     std::ostream & display_row(std::ostream & out, vector<row_cell<rational>> const & row) const;
-
-public:
     bool is_term(unsigned j) const;
     unsigned column_count() const;
     int select_int_infeasible_var();
-    explanation * explanation();
+    explanation * expl();
 };
 }