diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 07a7b0131..cadccb09f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -159,7 +159,6 @@ class theory_lra::imp {
     ast_manager&         m;
     theory_arith_params& m_arith_params;
     arith_util           a;
-    bool                 m_has_int;
     arith_eq_adapter     m_arith_eq_adapter;
     vector<rational>     m_columns;
       
@@ -720,7 +719,6 @@ class theory_lra::imp {
         }
         if (result == UINT_MAX) {
             result = m_solver->add_var(v, is_int(v));
-            m_has_int |= is_int(v);
             m_theory_var2var_index.setx(v, result, UINT_MAX);
             m_var_index2theory_var.setx(result, v, UINT_MAX);
             m_var_trail.push_back(v);
@@ -913,7 +911,6 @@ public:
         th(th), m(m), 
         m_arith_params(ap), 
         a(m), 
-        m_has_int(false),
         m_arith_eq_adapter(th, ap, a),            
         m_internalize_head(0),
         m_one_var(UINT_MAX),
@@ -1510,7 +1507,6 @@ public:
     }
 
     void init_variable_values() {
-        reset_variable_values();
         if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
             TRACE("arith", tout << "update variable values\n";);
             m_solver->get_model(m_variable_values);
@@ -1991,6 +1987,7 @@ public:
         return !added_bound;
     }
 
+
     lbool check_lia() {
         if (m.canceled()) {
             TRACE("arith", tout << "canceled\n";);
@@ -2000,6 +1997,7 @@ public:
         if (!check_idiv_bounds()) {
             return l_false;
         }
+
         lp::lar_term term;
         lp::mpq k;
         lp::explanation ex; // TBD, this should be streamlined accross different explanations
@@ -2075,12 +2073,12 @@ public:
         return lia_check;
     }
 
-    lbool check_aftermath_nra(lbool r, lp::explanation& ex) {
+    lbool check_aftermath_nra(lbool r) {
         m_a1 = alloc(scoped_anum, m_nra->am());
         m_a2 = alloc(scoped_anum, m_nra->am());
         switch (r) {
         case l_false:
-            set_conflict1(ex);
+            set_conflict1();
             break;
         case l_true:
             m_use_nra_model = true;
@@ -2096,40 +2094,39 @@ public:
         return r;
     }
 
-    void process_lemma(lp::explanation& ex, const niil::lemma& lemma) {
-        literal_vector core;
-        for (auto const& ineq : lemma) {
-            bool is_lower = true, pos = true, is_eq = false;
-                
-            switch (ineq.m_cmp) {
-            case lp::LE: is_lower = false; pos = false;  break;
-            case lp::LT: is_lower = true;  pos = true; break;
-            case lp::GE: is_lower = true;  pos = false;  break;
-            case lp::GT: is_lower = false; pos = true; break;
-            case lp::EQ: is_eq = true; pos = true; break;
-            case lp::NE: is_eq = true; pos = false; break;
-            default: UNREACHABLE();
-            }
-            TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
-            app_ref atom(m);
-            if (is_eq) {
-                atom = mk_eq(ineq.m_term);
-            }
-            else {
-                // create term >= 0 (or term <= 0)
-                atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
-            }
-            literal lit(ctx().get_bool_var(atom), pos);
-            core.push_back(~lit);
-        }
-        set_conflict_or_lemma(ex, core, false);
-    }
+    niil::lemma m_lemma;
  
-    lbool check_aftermath_niil(lbool r, lp::explanation& ex, const niil::lemma & lemma) {
+    lbool check_aftermath_niil(lbool r) {
         switch (r) {
-        case l_false:
-            process_lemma(ex, lemma);
+        case l_false: {            
+            literal_vector core;
+            for (auto const& ineq : m_lemma) {
+                bool is_lower = true, pos = true, is_eq = false;
+                
+                switch (ineq.m_cmp) {
+                case lp::LE: is_lower = false; pos = false;  break;
+                case lp::LT: is_lower = true;  pos = true; break;
+                case lp::GE: is_lower = true;  pos = false;  break;
+                case lp::GT: is_lower = false; pos = true; break;
+                case lp::EQ: is_eq = true; pos = true; break;
+                case lp::NE: is_eq = true; pos = false; break;
+                default: UNREACHABLE();
+                }
+                TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
+                app_ref atom(m);
+                if (is_eq) {
+                    atom = mk_eq(ineq.m_term);
+                }
+                else {
+                    // create term >= 0 (or term <= 0)
+                    atom = mk_bound(ineq.m_term, rational::zero(), is_lower);
+                }
+                literal lit(ctx().get_bool_var(atom), pos);
+                core.push_back(~lit);
+            }
+            set_conflict_or_lemma(core, false);
             break;
+        }
         case l_true:
             if (assume_eqs()) {
                 return l_false;
@@ -2150,10 +2147,9 @@ public:
         if (!m_nra && !m_niil) return l_true;
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
-        niil::lemma lemma;
         m_explanation.reset();
-        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, lemma);
-        return m_nra? check_aftermath_nra(r, m_explanation) : check_aftermath_niil(r, m_explanation, lemma);
+        lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, m_lemma);
+        return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
     }
 
     /**
@@ -3192,27 +3188,27 @@ public:
     void set_conflict() {
         m_explanation.clear();
         m_solver->get_infeasibility_explanation(m_explanation);
-        set_conflict1(m_explanation);
+        set_conflict1();
     }
 
-    void set_conflict1(lp::explanation& ex) {
+    void set_conflict1() {
         literal_vector core;
-        set_conflict_or_lemma(ex, core, true);
+        set_conflict_or_lemma(core, true);
     }
 
-    void set_conflict_or_lemma(lp::explanation& ex, literal_vector const& core, bool is_conflict) {
+    void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
         m_eqs.reset();
         m_core.reset();
         m_params.reset();
         for (literal lit : core) {
             m_core.push_back(lit);
         }
-        // m_solver->shrink_explanation_to_minimum(ex); // todo, enable when perf is fixed
+        // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
-        TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, ex); );
+        TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
         TRACE("arith", display(tout););
-        for (auto const& ev : ex) {
+        for (auto const& ev : m_explanation) {
             if (!ev.first.is_zero()) { 
                 set_evidence(ev.second);
             }
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 432fcd016..f7a792519 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -104,10 +104,11 @@ bool int_solver::is_gomory_cut_target(const row_strip<mpq>& row) {
         j = p.var();
         if (!is_base(j) && (!at_bound(j) || !is_zero(get_value(j).y))) {
             TRACE("gomory_cut", tout << "row is not gomory cut target:\n";
-                  display_column(tout, j););
+                  display_column(tout, j);
+                  tout << "infinitesimal: " << !is_zero(get_value(j).y) << "\n";);
             return false;
         }
-	}
+    }
     return true;
 }
 
@@ -133,11 +134,22 @@ bool int_solver::current_solution_is_inf_on_cut() const {
 }
 
 lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row) {
+
     lp_assert(column_is_int_inf(inf_col));
     gomory gc(m_t, m_k, m_ex, inf_col, row, *this);
     return gc.create_cut();
 }
 
+int int_solver::find_free_var_in_gomory_row(const row_strip<mpq>& row) {
+    unsigned j;
+    for (const auto & p : row) {
+        j = p.var();
+        if (!is_base(j) && is_free(j))
+            return static_cast<int>(j);
+    }
+    return -1;
+}
+
 lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
     const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
 
@@ -147,7 +159,6 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
         return create_branch_on_column(j);
 
     m_upper = true;
-
     return mk_gomory_cut(j, row);
 }
 
@@ -375,17 +386,10 @@ lia_move int_solver::make_hnf_cut() {
 #endif
     lia_move r =  m_hnf_cutter.create_cut(m_t, m_k, m_ex, m_upper, x0);
 
-    m_lemma->clear();
-    m_lemma->push_back(ineq());
-    ineq & f_in = first_in();
-    mpq k;
-    bool upper;
-    lia_move r =  m_hnf_cutter.create_cut(f_in.m_term, k, *m_ex, upper, x0);
-    if (r == lia_move::cut) {
-        f_in.m_term.m_v = -k;
-        f_in.m_cmp = upper? lconstraint_kind::LE : GE;
+    if (r == lia_move::cut) {      
         TRACE("hnf_cut",
-              print_ineq(f_in, tout << "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);
               }              
@@ -866,7 +870,7 @@ bool int_solver::at_bound(unsigned j) const {
     case column_type::upper_bound:
         return  mpq_solver.m_upper_bounds[j] == get_value(j);
     default:
-        return true; // a free var is always at a bound
+        return false;
     }
 }
 
@@ -1004,18 +1008,19 @@ lia_move int_solver::create_branch_on_column(int j) {
     TRACE("check_main_int", tout << "branching" << std::endl;);
     lp_assert(m_t.is_empty());
     lp_assert(j != -1);
-    first_in().add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
+    m_t->add_coeff_var(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
     if (is_free(j)) {
         m_upper = true;
         m_k = mpq(0);
     } else {
         m_upper = left_branch_is_more_narrow_than_right(j);
-        m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
+        m_k = *m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }
 
     TRACE("int_solver", tout << "branching v" << j << " = " << get_value(j) << "\n";
           display_column(tout, j);
           tout << "k = " << m_k << std::endl;
+
           );
     return lia_move::branch;
 
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index b51ae95d5..83a16aed8 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -33,39 +33,8 @@ class lar_solver;
 template <typename T, typename X>
 struct lp_constraint;
 
-struct ineq {
-    lp::lconstraint_kind m_cmp;
-    lp::lar_term         m_term;
-    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term) : m_cmp(cmp), m_term(term) {}
-    ineq() {} // empty constructor
-    void add_coeff_var(const mpq& c, unsigned j) {
-        m_term.add_coeff_var(c, j);
-    }
-    bool holds(const vector<impq> & x) const {
-        auto v = m_term.apply(x);
-        switch(m_cmp) {
-        case lconstraint_kind::LE: return v <= zero_of_type<impq>();
-        case lconstraint_kind::LT: return v <  zero_of_type<impq>();
-        case lconstraint_kind::GE: return v >= zero_of_type<impq>();
-        case lconstraint_kind::GT: return v >  zero_of_type<impq>();
-        case lconstraint_kind::EQ: return v == zero_of_type<impq>();
-        default:
-            lp_assert(false);
-            return false;
-        }
-    }
-    bool is_empty() const { return m_term.is_empty(); }
-};
-
-typedef vector<ineq> lemma;
 
 class int_solver {
-    struct validate_model {
-        int_solver& s;
-        lia_move& r;
-        validate_model(int_solver& s, lia_move& r): s(s), r(r) {}
-        ~validate_model();
-    };
 public:
     // fields
     lar_solver          *m_lar_solver;
@@ -85,6 +54,7 @@ public:
     mpq const& get_offset() const { return m_k; }
     explanation const& get_explanation() const { return m_ex; }
     bool is_upper() const { return m_upper; }
+    lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);    
     bool is_base(unsigned j) const;
     bool is_real(unsigned j) const;
     const impq & lower_bound(unsigned j) const;
@@ -146,7 +116,6 @@ private:
     unsigned row_of_basic_column(unsigned j) const;
 
 public:
-    std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
     void display_column(std::ostream & out, unsigned j) const;
     constraint_index column_upper_bound_constraint(unsigned j) const;
     constraint_index column_lower_bound_constraint(unsigned j) const;
@@ -171,7 +140,6 @@ public:
     int find_inf_int_nbasis_column() const;
     lia_move run_gcd_test();
     lia_move gomory_cut();
-    void add_free_vars_ineqs_to_lemma();
     lia_move hnf_cut();
     lia_move make_hnf_cut();
     bool init_terms_for_hnf_cut();
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index e4f2261b0..63d57d4be 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -26,7 +26,7 @@ typedef lp::constraint_index     lpci;
 typedef std::unordered_set<lpci> expl_set;
 typedef nra::mon_eq              mon_eq;
 typedef lp::var_index            lpvar;
-typedef lp::ineq                 ineq;
+
 struct hash_svector {
     size_t operator()(const unsigned_vector & v) const {
         return svector_hash<unsigned_hash>()(v);
@@ -979,117 +979,124 @@ struct solver::imp {
         int      m_sign;  // 
     };
     
-    // struct factors_of_monomial {
-    //     unsigned         m_i_mon;
-    //     const imp&       m_imp;
-    //     const mon_eq&    m_mon;
-    //     unsigned_vector  m_minimized_vars;
-    //     int              m_sign;
-    //     factors_of_monomial(unsigned i_mon, const imp& s) : m_i_mon(i_mon), m_imp(s),
-    //                                                         m_mon(m_imp.m_monomials[i_mon]) {
-    //         m_minimized_vars = reduce_monomial_to_minimal(i_mon, m_sign);
-    //     }
+    struct factors_of_monomial {
+        unsigned         m_i_mon;
+        const imp&       m_imp;
+        const mon_eq&    m_mon;
+        unsigned_vector  m_minimized_vars;
+        int              m_sign;
+        factors_of_monomial(unsigned i_mon, const imp& s) : m_i_mon(i_mon), m_imp(s),
+                                                            m_mon(m_imp.m_monomials[i_mon]) {
+            // m_minimized_vars = reduce_monomial_to_minimal(i_mon, m_sign);
+        }
 
         
         
-    //     struct const_iterator {
-    //         // fields
-    //         unsigned_vector        m_mask;
-    //         factors_of_monomial&   m_fm;
-    //         //typedefs
+        struct const_iterator {
+            // fields
+            unsigned_vector        m_mask;
+            //            factors_of_monomial&   m_fm;
+            //typedefs
             
             
-    //         typedef const_iterator self_type;
-    //         typedef signed_two_factorization value_type;
-    //         typedef const signed_two_factorization reference;
-    //         //        typedef const column_cell* pointer;
-    //         typedef int difference_type;
-    //         typedef std::forward_iterator_tag iterator_category;
-
-    //         bool get_factors(unsigned& k, unsigned& j) {
-    //             unsigned_vector a;
-    //             unsigned_vector b;
-    //             for (unsigned j = 0; j < m_mask.size(); j++) {
-    //                 if (m_mask[j] == 1) {
-    //                     a.push_back(m_fm.m_minimized_vars[j]);
-    //                 } else {
-    //                     b.push_back(m_fm.m_minimized_vars[j]);
-    //                 }
-    //             }
-    //             SASSERT(!a.empty() && !b.empty());
-    //             std::sort(a.begin(), a.end());
-    //             std::sort(b.begin(), b.end());
-    //             int a_sign, b_sign;
-    //             if (a.size() == 1) {
-    //                 k = a[0];
-    //                 a_sign = 1;
-    //             } else if (!m_imp.find_monomial_of_vars(a, k, a_sign)) {
-    //                 return false;
-    //             } else {
-    //                 return false;
-    //             }
-    //             if (b.size() == 1) {
-    //                 j = b[0];
-    //                 b_sign = 1;
-    //             } else  if (!m_imp.find_monomial_of_vars(b, j, b_sign)) {
-    //                     return false;
-    //             } else {
-    //                 return false;
-    //             }
+            typedef const_iterator self_type;
+            typedef signed_two_factorization value_type;
+            typedef const signed_two_factorization reference;
+            //        typedef const column_cell* pointer;
+            typedef int difference_type;
+            typedef std::forward_iterator_tag iterator_category;
 
+            bool get_factors(unsigned& k, unsigned& j) {
+                /*
+                unsigned_vector a;
+                unsigned_vector b;
+                for (unsigned j = 0; j < m_mask.size(); j++) {
+                    if (m_mask[j] == 1) {
+                        a.push_back(m_fm.m_minimized_vars[j]);
+                    } else {
+                        b.push_back(m_fm.m_minimized_vars[j]);
+                    }
+                }
+                SASSERT(!a.empty() && !b.empty());
+                std::sort(a.begin(), a.end());
+                std::sort(b.begin(), b.end());
+                int a_sign, b_sign;
+                if (a.size() == 1) {
+                    k = a[0];
+                    a_sign = 1;
+                } else if (!m_imp.find_monomial_of_vars(a, k, a_sign)) {
+                    return false;
+                } else {
+                    return false;
+                }
+                if (b.size() == 1) {
+                    j = b[0];
+                    b_sign = 1;
+                } else  if (!m_imp.find_monomial_of_vars(b, j, b_sign)) {
+                        return false;
+                } else {
+                    return false;
+                }
+                */
+                SASSERT(false); // not implemented
+                return false;
                 
-    //         }
+            }
             
-    //         reference operator*() const {
-    //             unsigned k, j; // the factors
-    //             if (!get_factors(k, j))
-    //                 return std::pair<lpvar, lpvar>(static_cast<unsigned>(-1), 0);
-                
-    //             return std::pair<lpvar, lpvar>(k, j);
-    //         }
-    //         void advance_mask() {
-    //             for (unsigned k = 0; k < m_masl.size(); k++) {
-    //                 if (mask[k] == 0){
-    //                     mask[k] = 1;
-    //                     break;
-    //                 } else {
-    //                     mask[k] = 0;
-    //                 }
-    //             }
-    //         }
-    //         self_type operator++() {  self_type i = *this; operator++(1); return i;  }
-    //         self_type operator++(int) { advance_mask(); return *this; }
+            reference operator*() const {
+                SASSERT(false); // not implemented
+                // unsigned k, j; // the factors
+                //if (!get_factors(k, j))
+                //  return std::pair<lpvar, lpvar>(static_cast<unsigned>(-1), 0);
+                return signed_two_factorization();
+                //                return std::pair<lpvar, lpvar>(k, j);
+            }
+            void advance_mask() {
+                SASSERT(false);// not implemented
+                /*
+                for (unsigned k = 0; k < m_masl.size(); k++) {
+                    if (mask[k] == 0){
+                        mask[k] = 1;
+                        break;
+                    } else {
+                        mask[k] = 0;
+                    }
+                    }*/
+            }
+            self_type operator++() {  self_type i = *this; operator++(1); return i;  }
+            self_type operator++(int) { advance_mask(); return *this; }
 
-    //         const_iterator(const unsigned_vector& mask) :
-    //             m_mask(mask) {
-    //             //   SASSERT(false);
-    //         }
-    //         bool operator==(const self_type &other) const {
-    //             return m_mask == other.m_mask;
-    //         }
-    //         bool operator!=(const self_type &other) const { return !(*this == other); }
-    //     };
+            const_iterator(const unsigned_vector& mask) :
+                m_mask(mask) {
+                //   SASSERT(false);
+            }
+            bool operator==(const self_type &other) const {
+                return m_mask == other.m_mask;
+            }
+            bool operator!=(const self_type &other) const { return !(*this == other); }
+        };
 
-    //     const_iterator begin() const {
-    //         unsigned_vector mask(m_mon.m_vs.size(), static_cast<lpvar>(0));
-    //         mask[0] = 1; 
-    //         return const_iterator(mask);
-    //     }
+        const_iterator begin() const {
+            unsigned_vector mask(m_mon.m_vs.size(), static_cast<lpvar>(0));
+            mask[0] = 1; 
+            return const_iterator(mask);
+        }
         
-    //     const_iterator end() const {
-    //         unsigned_vector mask(m_mon.m_vs.size(), 1);
-    //         return const_iterator(mask);
-    //     }
-    // };
+        const_iterator end() const {
+            unsigned_vector mask(m_mon.m_vs.size(), 1);
+            return const_iterator(mask);
+        }
+    };
     bool lemma_for_proportional_factors(unsigned i_mon, lpvar a, lpvar b) {
         return false;
     }
     // we derive a lemma from |xy| > |y| => |x| >= 1 || |y| = 0
     bool basic_lemma_for_mon_proportionality_from_product_to_factors(unsigned i_mon) {
-        SASSERT(false); // not implemented
-        // for (std::pair<lpvar, lpvar> factors : factors_of_monomial(i_mon, *this))
-        //     if (lemma_for_proportional_factors(i_mon, factors.first, factors.second))
-        //         return true;
+        for (auto factors : factors_of_monomial(i_mon, *this)) {
+            // if (lemma_for_proportional_factors(i_mon, factors.first, factors.second))
+        }
+            //  return true;
+        SASSERT(false);
         return false;
     }
 
diff --git a/src/util/lp/niil_solver.h b/src/util/lp/niil_solver.h
index c24b23e14..71c9eec37 100644
--- a/src/util/lp/niil_solver.h
+++ b/src/util/lp/niil_solver.h
@@ -24,9 +24,15 @@ Revision History:
 #include "util/params.h"
 #include "nlsat/nlsat_solver.h"
 #include "util/lp/lar_solver.h"
-#include "util/lp/int_solver.h"
 namespace niil {
-typedef lp::lemma lemma;
+struct ineq {
+    lp::lconstraint_kind m_cmp;
+    lp::lar_term         m_term;
+    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term) : m_cmp(cmp), m_term(term) {} 
+};
+
+typedef vector<ineq> lemma;
+
 // nonlinear integer incremental linear solver
 class solver {
     struct imp;