diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 826f87e8c..c2d7d84a3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -166,6 +166,8 @@ foreach (header ${libz3_public_headers})
   set_property(TARGET libz3 APPEND PROPERTY
     PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}")
 endforeach()
+set_property(TARGET libz3 APPEND PROPERTY
+    PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/version.h")
 
 install(TARGETS libz3
   EXPORT Z3_EXPORTED_TARGETS
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index fc42acbb9..5a4537a4a 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -372,6 +372,21 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) {
+        Z3_TRY;
+        LOG_Z3_solver_get_non_units(c, s);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector fmls = to_solver_ref(s)->get_non_units(mk_c(c)->m());
+        for (expr* f : fmls) {
+            v->m_ast_vector.push_back(f);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a65d6e4d8..a283571d0 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2038,6 +2038,7 @@ namespace z3 {
         stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
         expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
+        expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s);
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 25b437bc4..d7d8aeddc 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1816,7 +1816,7 @@ struct
 
   let get_model x =
     let q = Z3native.solver_get_model (gc x) x in
-    if Z3native.is_null_model q then None else Some q
+    try if Z3native.is_null_model q then None else Some q with | _ -> None
 
   let get_proof x =
     let q = Z3native.solver_get_proof (gc x) x in
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 73339d478..b9e15d329 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6646,6 +6646,11 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
 
+    def non_units(self):
+        """Return an AST vector containing all atomic formulas in solver state that are not units.
+        """
+        return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
+
     def statistics(self):
         """Return statistics for the last `check()`.
 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 2657e558d..03bce5d5e 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6121,6 +6121,14 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
 
+
+    /**
+       \brief Return the set of non units in the solver state.
+
+       def_API('Z3_solver_get_non_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
+    */
+    Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fd2dc0da2..ca59a2c27 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) {
 }
 
 class bound { 
-    smt::bool_var     m_bv;
+    smt::bool_var    m_bv;
     smt::theory_var  m_var;
     bool             m_is_int;
     rational         m_value;
@@ -165,13 +165,13 @@ class theory_lra::imp {
         expr_ref_vector     m_terms;                     
         vector<rational>    m_coeffs;
         svector<theory_var> m_vars;
-        rational            m_coeff;
+        rational            m_offset;
         ptr_vector<expr>    m_terms_to_internalize;
         internalize_state(ast_manager& m): m_terms(m) {}
         void reset() {
             m_terms.reset();
             m_coeffs.reset();
-            m_coeff.reset();
+            m_offset.reset();
             m_vars.reset();
             m_terms_to_internalize.reset();
         }
@@ -197,7 +197,7 @@ class theory_lra::imp {
         expr_ref_vector&     terms() { return m_st.m_terms; }                     
         vector<rational>&    coeffs() { return m_st.m_coeffs; }
         svector<theory_var>& vars() { return m_st.m_vars; }
-        rational&            coeff() { return m_st.m_coeff; }
+        rational&            offset() { return m_st.m_offset; }
         ptr_vector<expr>&    terms_to_internalize() { return m_st.m_terms_to_internalize; }            
         void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
         void set_back(unsigned i) { 
@@ -216,6 +216,8 @@ class theory_lra::imp {
     svector<theory_var>      m_term_index2theory_var;   // reverse map from lp_solver variables to theory variables  
     var_coeffs               m_left_side;              // constraint left side
     mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
+    lp::var_index m_one_var;
+    lp::var_index m_zero_var;
 
     enum constraint_source {
         inequality_source,
@@ -331,6 +333,32 @@ class theory_lra::imp {
         }
     }
 
+    void add_const(int c, lp::var_index& var) {
+        if (var != UINT_MAX) {
+            return;
+        }
+        app_ref cnst(a.mk_int(c), m);
+        TRACE("arith", tout << "add " << cnst << "\n";);
+        enode* e = mk_enode(cnst);
+        theory_var v = mk_var(cnst);
+        var = m_solver->add_var(v, true);
+        m_theory_var2var_index.setx(v, var, UINT_MAX);
+        m_var_index2theory_var.setx(var, v, UINT_MAX);
+        m_var_trail.push_back(v);
+        add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c)));
+        add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c)));
+    }
+
+    lp::var_index get_one() {
+        add_const(1, m_one_var);
+        return m_one_var;
+    }
+
+    lp::var_index get_zero() {
+        add_const(0, m_zero_var);
+        return m_zero_var;
+    }
+
 
     void found_not_handled(expr* n) {
         m_not_handled = n;
@@ -375,7 +403,7 @@ class theory_lra::imp {
         expr_ref_vector & terms = st.terms();
         svector<theory_var>& vars = st.vars();
         vector<rational>& coeffs = st.coeffs();
-        rational& coeff = st.coeff();
+        rational& offset = st.offset();
         rational r;
         expr* n1, *n2;
         unsigned index = 0;
@@ -415,7 +443,7 @@ class theory_lra::imp {
                 ++index;
             }
             else if (a.is_numeral(n, r)) {
-                coeff += coeffs[index]*r;
+                offset += coeffs[index]*r;
                 ++index;
             }
             else if (a.is_uminus(n, n1)) {
@@ -427,7 +455,6 @@ class theory_lra::imp {
                 app* t = to_app(n);
                 internalize_args(t);
                 mk_enode(t);
-				
                 theory_var v = mk_var(n);
                 coeffs[vars.size()] = coeffs[index];
                 vars.push_back(v);
@@ -738,7 +765,15 @@ class theory_lra::imp {
     }
        
     bool is_unit_var(scoped_internalize_state& st) {
-        return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
+        return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
+    }
+
+    bool is_one(scoped_internalize_state& st) {
+        return st.offset().is_one() && st.vars().empty();
+    }
+
+    bool is_zero(scoped_internalize_state& st) {
+        return st.offset().is_zero() && st.vars().empty();
     }
 
     theory_var internalize_def(app* term, scoped_internalize_state& st) {
@@ -771,13 +806,24 @@ class theory_lra::imp {
         if (is_unit_var(st)) {
             return st.vars()[0];
         }
+        else if (is_one(st)) {
+            return get_one();
+        }
+        else if (is_zero(st)) {
+            return get_zero();
+        }
         else {
             init_left_side(st);
             theory_var v = mk_var(term);
             lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
-            TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";);
+            TRACE("arith", tout << mk_pp(term, m) << " v" << v << "\n";);
             if (vi == UINT_MAX) {
-                vi = m_solver->add_term(m_left_side, st.coeff());
+                rational const& offset = st.offset();
+                if (!offset.is_zero()) {
+                    m_left_side.push_back(std::make_pair(offset, get_one()));
+                }
+                SASSERT(!m_left_side.empty());
+                vi = m_solver->add_term(m_left_side);
                 m_theory_var2var_index.setx(v, vi, UINT_MAX);
                 if (m_solver->is_term(vi)) {
                     m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX);
@@ -806,6 +852,8 @@ public:
         m_has_int(false),
         m_arith_eq_adapter(th, ap, a),            
         m_internalize_head(0),
+        m_one_var(UINT_MAX),
+        m_zero_var(UINT_MAX),
         m_not_handled(nullptr),
         m_asserted_qhead(0), 
         m_assume_eq_head(0),
@@ -879,7 +927,7 @@ public:
     }
         
     void internalize_eq_eh(app * atom, bool_var) {
-        expr* lhs = 0, *rhs = 0;
+        expr* lhs = nullptr, *rhs = nullptr;
         VERIFY(m.is_eq(atom, lhs, rhs));
         enode * n1 = get_enode(lhs);
         enode * n2 = get_enode(rhs);
@@ -1197,7 +1245,6 @@ public:
             m_todo_terms.pop_back();
             if (m_solver->is_term(vi)) {
                 const lp::lar_term& term = m_solver->get_term(vi);
-                result += term.m_v * coeff;
                 for (const auto & i:  term) {
                     m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
                 }                    
@@ -1234,7 +1281,6 @@ public:
             m_todo_terms.pop_back();
             if (m_solver->is_term(wi)) {
                 const lp::lar_term& term = m_solver->get_term(wi);
-                result += term.m_v * coeff;
                 for (const auto & i : term) {
                     if (m_variable_values.count(i.var()) > 0) {
                         result += m_variable_values[i.var()] * coeff * i.coeff();
@@ -1481,8 +1527,8 @@ public:
         bool all_bounded = true;
         for (unsigned v = 0; v < nv; ++v) {
             lp::var_index vi = m_theory_var2var_index[v];
-			if (vi == UINT_MAX)
-				continue;
+            if (vi == UINT_MAX)
+                continue;
             if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
                 lp::lar_term term;
                 term.add_monomial(rational::one(), vi);
@@ -1516,23 +1562,10 @@ public:
             theory_var v  = mk_var(n);
             theory_var v1 = mk_var(p);
             theory_var v2 = mk_var(q);
-            rational r = get_value(v);
             rational r1 = get_value(v1);
-            rational r2 = get_value(v2);
-            rational r3;
-            if (r2.is_zero()) {
-                continue;
-            }
-            if (r1.is_int() && r2.is_int() && r == div(r1, r2)) {
-                continue;
-            }
-            if (r2.is_neg() || r1.is_neg()) {
-                // TBD
-                continue;
-            }
+            rational r2;
 
-            if (!r1.is_int() || !r2.is_int()) {
-                // std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n";
+            if (!r1.is_int() || r1.is_neg()) {
                 // TBD
                 // r1 = 223/4, r2 = 2, r = 219/8 
                 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
@@ -1542,16 +1575,18 @@ public:
                 continue;
             }
 
-            if (a.is_numeral(q, r3)) {
+            if (a.is_numeral(q, r2) && r2.is_pos()) {
+                if (get_value(v) == div(r1, r2)) continue;
             
-                SASSERT(r3 == r2 && r2.is_int());
-                SASSERT(r1.is_int() && r3.is_int());
                 rational div_r = div(r1, r2);
                 // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2)
                 // p >= q * div(r1, q) => div(r1, q) <= div(p, q)
                 rational mul(1);
                 rational hi = r2 * div_r + r2 - 1;
                 rational lo = r2 * div_r;
+
+                // used to normalize inequalities so they 
+                // don't appear as 8*x >= 15, but x >= 2
                 expr *n1 = nullptr, *n2 = nullptr;
                 if (a.is_mul(p, n1, n2) && is_numeral(n1, mul) && mul.is_pos()) {
                     p = n2;
@@ -1568,7 +1603,7 @@ public:
                 all_divs_valid = false;
 
                 TRACE("arith",
-                      tout << r1 << " div " << r2 << " = " << r3 << "\n";
+                      tout << r1 << " div " << r2 << "\n";
                       literal_vector lits;
                       lits.push_back(~p_le_r1);
                       lits.push_back(n_le_div);
@@ -1578,8 +1613,10 @@ public:
                       ctx().display_literals_verbose(tout, lits) << "\n";);                      
                 continue;
             }
+#if 0
 
-
+            // TBD similar for non-linear division.
+            // better to deal with in nla_solver:
 
             all_divs_valid = false;
 
@@ -1610,6 +1647,7 @@ public:
                   lits[0] = pq_rhs;
                   lits[1] = n_ge_div;
                   ctx().display_literals_verbose(tout, lits) << "\n";);
+#endif
         }
         
         return all_divs_valid;
@@ -1708,17 +1746,13 @@ public:
             TRACE("arith", tout << "idiv bounds check\n";);
             return l_false;
         }
-        lp::lar_term term;
-        lp::mpq k;
-        lp::explanation ex; // TBD, this should be streamlined accross different explanations
-        bool upper;
         m_explanation.reset();
-        switch(m_lia->check(term, k, ex, upper)) {
+        switch (m_lia->check()) {
         case lp::lia_move::sat:
             return l_true;
         case lp::lia_move::branch: {
             TRACE("arith", tout << "branch\n";);
-            app_ref b = mk_bound(term, k, !upper);
+            app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
             // branch on term >= k + 1
             // branch on term <= k
@@ -1731,13 +1765,13 @@ public:
             TRACE("arith", tout << "cut\n";);
             ++m_stats.m_gomory_cuts;
             // m_explanation implies term <= k
-            app_ref b = mk_bound(term, k, !upper);
+            app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n");
-            TRACE("arith", dump_cut_lemma(tout, term, k, ex, upper););
+            TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper()););
             m_eqs.reset();
             m_core.reset();
             m_params.reset();
-            for (auto const& ev : ex.m_explanation) {
+            for (auto const& ev : m_lia->get_explanation().m_explanation) {
                 if (!ev.first.is_zero()) { 
                     set_evidence(ev.second);
                 }
@@ -1752,7 +1786,7 @@ public:
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
-            m_explanation = ex.m_explanation;
+            m_explanation = m_lia->get_explanation().m_explanation;
             set_conflict1();
             return l_false;
         case lp::lia_move::undef:
@@ -2921,7 +2955,7 @@ public:
                 lp::lar_term const& term = m_solver->get_term(vi);
                 TRACE("arith", m_solver->print_term(term, tout) << "\n";);
                 scoped_anum r1(m_nra->am());
-                rational c1 = term.m_v * wcoeff;
+                rational c1(0);
                 m_nra->am().set(r1, c1.to_mpq());
                 m_nra->am().add(r, r1, r);                
                 for (auto const & arg : term) {
@@ -3196,7 +3230,6 @@ public:
             coeffs.find(w, c0);
             coeffs.insert(w, c0 + ti.coeff() * coeff);
         }
-        offset += coeff * term.m_v;
     }
 
     app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 4044c4a85..e4fe09adf 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -256,3 +256,34 @@ expr_ref_vector solver::get_units(ast_manager& m) {
 
     return result;
 }
+
+expr_ref_vector solver::get_non_units(ast_manager& m) {
+    expr_ref_vector result(m), fmls(m);
+    get_assertions(fmls);
+    family_id bfid = m.get_basic_family_id();
+    expr_mark marked;
+    unsigned sz0 = fmls.size();
+    for (unsigned i = 0; i < fmls.size(); ++i) {
+        expr* f = fmls.get(i);
+        if (marked.is_marked(f)) continue;
+        marked.mark(f);
+        if (!is_app(f)) {
+            if (i >= sz0) result.push_back(f);
+            continue;
+        }
+        app* _f = to_app(f);
+        if (_f->get_family_id() == bfid) {
+            // basic objects are true/false/and/or/not/=/distinct and proof objects (that are not Boolean)
+            if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) {
+                fmls.append(_f->get_num_args(), _f->get_args());
+            }
+            else if (m.is_eq(f) || m.is_distinct(f)) {
+                if (i >= sz0) result.push_back(f);
+            }
+        }
+        else {
+            if (i >= sz0) result.push_back(f);
+        }
+    }
+    return result;
+}
diff --git a/src/solver/solver.h b/src/solver/solver.h
index c371be284..5329161cd 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -236,6 +236,8 @@ public:
     */
     expr_ref_vector get_units(ast_manager& m);
 
+    expr_ref_vector get_non_units(ast_manager& m);
+
     class scoped_push {
         solver& s;
         bool    m_nopop;
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index 501ad9e1a..972466dc3 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -185,7 +185,6 @@ struct gomory_test {
     }
 
     void print_term(lar_term & t, std::ostream & out) {
-        lp_assert(is_zero(t.m_v));
         vector<std::pair<mpq, unsigned>>  row;
         for (auto p : t.m_coeffs)
             row.push_back(std::make_pair(p.second, p.first));
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 6e418fe68..ff9de0e58 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -2667,13 +2667,20 @@ void test_term() {
     lar_solver solver;
     unsigned _x = 0;
     unsigned _y = 1;
+    unsigned _one = 2;
     var_index x = solver.add_var(_x, false);
     var_index y = solver.add_var(_y, false);
+    var_index one = solver.add_var(_one, false);
+
+    vector<std::pair<mpq, var_index>> term_one;
+    term_one.push_back(std::make_pair((int)1, one));
+    solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0));
 
     vector<std::pair<mpq, var_index>> term_ls;
     term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
     term_ls.push_back(std::pair<mpq, var_index>((int)1, y));
-    var_index z = solver.add_term(term_ls, mpq(3));
+    term_ls.push_back(std::make_pair((int)3, one));
+    var_index z = solver.add_term(term_ls);
 
     vector<std::pair<mpq, var_index>> ls;
     ls.push_back(std::pair<mpq, var_index>((int)1, x));
@@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() {
     vector<std::pair<mpq, var_index>> coeffs;
     coeffs.push_back(std::pair<mpq, var_index>(1, a));
     coeffs.push_back(std::pair<mpq, var_index>(-1, c));
-    ls.add_term(coeffs, zero_of_type<mpq>());
+    ls.add_term(coeffs);
     coeffs.pop_back();
     coeffs.push_back(std::pair<mpq, var_index>(-1, b));
-    ls.add_term(coeffs, zero_of_type<mpq>());
+    ls.add_term(coeffs);
     coeffs.clear();
     coeffs.push_back(std::pair<mpq, var_index>(1, a));
     coeffs.push_back(std::pair<mpq, var_index>(-1, b));
@@ -3485,12 +3492,12 @@ void test_maximize_term() {
     vector<std::pair<mpq, var_index>> term_ls;
     term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
     term_ls.push_back(std::pair<mpq, var_index>((int)-1, y));
-    unsigned term_x_min_y = solver.add_term(term_ls, mpq(0));
+    unsigned term_x_min_y = solver.add_term(term_ls);
     term_ls.clear();
     term_ls.push_back(std::pair<mpq, var_index>((int)2, x));
     term_ls.push_back(std::pair<mpq, var_index>((int)2, y));
     
-    unsigned term_2x_pl_2y = solver.add_term(term_ls, mpq(0));
+    unsigned term_2x_pl_2y = solver.add_term(term_ls);
     solver.add_var_bound(term_x_min_y,  LE, zero_of_type<mpq>());
     solver.add_var_bound(term_2x_pl_2y, LE, mpq((int)5));
     solver.find_feasible_solution();
@@ -3502,8 +3509,7 @@ void test_maximize_term() {
         std::cout<< "v[" << p.first << "] = " << p.second << std::endl;
     }
     std::cout << "calling int_solver\n";
-    lar_term t; mpq k; explanation ex; bool upper;
-    lia_move lm = i_solver.check(t, k, ex, upper);
+    lia_move lm = i_solver.check();
     VERIFY(lm == lia_move::sat);
     impq term_max;
     lp_status st = solver.maximize_term(term_2x_pl_2y, term_max);
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 85b6f955c..a84cc1f00 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -7,6 +7,7 @@ endif()
 set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
 configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h)
 
+
 z3_add_component(util
   SOURCES
     approx_nat.cpp
diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/bound_propagator.cpp
index c4fa2aefa..a5c7c976a 100644
--- a/src/util/lp/bound_propagator.cpp
+++ b/src/util/lp/bound_propagator.cpp
@@ -17,10 +17,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const {
 }
 void bound_propagator::try_add_bound(mpq  v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
     j = m_lar_solver.adjust_column_index_to_term_index(j);    
-    if (m_lar_solver.is_term(j)) {
-        // lp treats terms as not having a free coefficient, restoring it below for the outside consumption
-        v += m_lar_solver.get_term(j).m_v;
-    }
 
     lconstraint_kind kind = is_low? GE : LE;
     if (strict)
diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp
index 53e12c7ec..96b3ab395 100644
--- a/src/util/lp/gomory.cpp
+++ b/src/util/lp/gomory.cpp
@@ -41,10 +41,11 @@ class gomory::imp {
     constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); }
     constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); }
     bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); }
+
     void int_case_in_gomory_cut(const mpq & a, unsigned j,
-                                            mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
+                                mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) {
         lp_assert(is_int(j) && !a.is_int());
-        mpq fj =  fractional_part(a);
+        mpq fj = fractional_part(a);
         TRACE("gomory_cut_detail", 
               tout << a << " j=" << j << " k = " << m_k;
               tout << ", fj: " << fj << ", ";
@@ -53,22 +54,23 @@ class gomory::imp {
               );
         lp_assert(fj.is_pos() && (a - fj).is_int());
         mpq new_a;
-        mpq one_minus_fj = 1 - fj;
         if (at_lower(j)) {
-            new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0;
+            new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0);
+            lp_assert(new_a.is_pos());
             m_k.addmul(new_a, lower_bound(j).x);
-            m_ex.push_justification(column_lower_bound_constraint(j), new_a);
+            m_ex.push_justification(column_lower_bound_constraint(j), new_a);            
         }
         else {
             lp_assert(at_upper(j));
             // the upper terms are inverted: therefore we have the minus
-            new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0);
+            new_a = - (fj <= f0 ? fj / f0  : ((1 - fj) / one_minus_f0));
+            lp_assert(new_a.is_neg());
             m_k.addmul(new_a, upper_bound(j).x);
             m_ex.push_justification(column_upper_bound_constraint(j), new_a);
         }
         m_t.add_monomial(new_a, j);
         lcm_den = lcm(lcm_den, denominator(new_a));
-        TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
+        TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";);
     }
 
     void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) {
@@ -111,6 +113,7 @@ class gomory::imp {
 
     void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) {
         lp_assert(!m_t.is_empty());
+        // k = 1 + sum of m_t at bounds
         auto pol = m_t.coeffs_as_vector();
         m_t.clear();
         if (pol.size() == 1) {
@@ -131,9 +134,9 @@ class gomory::imp {
                 m_t.add_monomial(mpq(1), v);
             }
         } else {
-            TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
             lcm_den = lcm(lcm_den, denominator(m_k));
             lp_assert(lcm_den.is_pos());
+            TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << lcm_den << std::endl;);
             if (!lcm_den.is_one()) {
                 // normalize coefficients of integer parameters to be integers.
                 for (auto & pi: pol) {
@@ -143,8 +146,10 @@ class gomory::imp {
                 m_k *= lcm_den;
             }
             // negate everything to return -pol <= -m_k
-            for (const auto & pi: pol)
+            for (const auto & pi: pol) {
+                TRACE("gomory_cut", tout << pi.first << "* " << "v" << pi.second << "\n";);
                 m_t.add_monomial(-pi.first, pi.second);
+            }
             m_k.neg();
         }
         TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;);
@@ -155,21 +160,16 @@ class gomory::imp {
         return std::string("x") + std::to_string(j);
     }
 
-    void dump_coeff_val(std::ostream & out, const mpq & a) const {
+    std::ostream& dump_coeff_val(std::ostream & out, const mpq & a) const {
         if (a.is_int()) {
-            if ( a >= zero_of_type<mpq>())
-                out << a;
-            else {
-                out << "( - " <<  - a << ") ";
-            }
-        } else {
-            if ( a >= zero_of_type<mpq>())
-                out << "(div " << numerator(a) << " " << denominator(a) << ")";
-            else {
-                out << "(- ( div " <<   numerator(-a) << " " << denominator(-a) << "))";
-            }
-            
+            out << a;
+        } 
+        else if ( a >= zero_of_type<mpq>())
+            out << "(/ " << numerator(a) << " " << denominator(a) << ")";
+        else {
+            out << "(- ( / " <<   numerator(-a) << " " << denominator(-a) << "))";
         }
+        return out;
     }
     
     template <typename T>
@@ -179,80 +179,82 @@ class gomory::imp {
         out << " " << var_name(c.var()) << ")";
     }
     
-    void dump_row_coefficients(std::ostream & out) const {
+    std::ostream& dump_row_coefficients(std::ostream & out) const {
+        mpq lc(1);
         for (const auto& p : m_row) {
-            if (!column_is_fixed(p.var()))
-                dump_coeff(out, p);
+            lc = lcm(lc, denominator(p.coeff())); 
+        }        
+        for (const auto& p : m_row) {
+            dump_coeff_val(out << " (* ", p.coeff()*lc) << " " << var_name(p.var()) << ")";
         }
+        return out;
     }
     
     void dump_the_row(std::ostream& out) const {
         out << "; the row, excluding fixed vars\n";
-        out << "(assert ( = ( + ";
-        dump_row_coefficients(out);
-        out << ") 0))\n";
+        out << "(assert ( = ( +";
+        dump_row_coefficients(out) << ") 0))\n";
+    }
+
+    void dump_declaration(std::ostream& out, unsigned v) const {
+        out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n";
     }
     
     void dump_declarations(std::ostream& out) const {
         // for a column j the var name is vj
         for (const auto & p : m_row) {
-            if (column_is_fixed(p.var())) continue;
-            out << "(declare-fun " << var_name(p.var()) << " () "
-                << (is_int(p.var())? "Int" : "Real") << ")\n";
+            dump_declaration(out, p.var());
+        }
+        for (const auto& p : m_t) {
+            unsigned v = p.var();
+            if (m_int_solver.m_lar_solver->is_term(v)) {
+                dump_declaration(out, v);
+            }
         }
     }
 
     void dump_lower_bound_expl(std::ostream & out, unsigned j) const {
-        out << "(assert ( >= " << var_name(j) << " " << lower_bound(j).x << "))\n";
+        out << "(assert (>= " << var_name(j) << " " << lower_bound(j).x << "))\n";
     }
     void dump_upper_bound_expl(std::ostream & out, unsigned j) const {
-        out << "(assert ( <= " << var_name(j) << " " << upper_bound(j).x << "))\n";
+        out << "(assert (<= " << var_name(j) << " " << upper_bound(j).x << "))\n";
     }
     
     void dump_explanations(std::ostream& out) const {
         for (const auto & p : m_row) {            
             unsigned j = p.var();
-            if (column_is_fixed(j)) continue;
-            if (j == m_inf_col) {
+            if (j == m_inf_col || (!is_real(j) && p.coeff().is_int())) {
                 continue;
             }
-
-            if (column_is_fixed(j)) {
-                dump_lower_bound_expl(out, j);
-                dump_upper_bound_expl(out, j);
-                continue;
-            }
-
-            if (at_lower(j)) {
+            else if (at_lower(j)) {
                 dump_lower_bound_expl(out, j);
             } else {
+                lp_assert(at_upper(j));
                 dump_upper_bound_expl(out, j);
             }
         }
     }
 
-    void dump_terms_coefficients(std::ostream & out) const {
+    std::ostream& dump_term_coefficients(std::ostream & out) const {
         for (const auto& p : m_t) {
             dump_coeff(out, p);
         }
+        return out;
     }
     
-    void dump_term_sum(std::ostream & out) const {
-        out << "( + ";
-        dump_terms_coefficients(out);
-        out << ")";
+    std::ostream& dump_term_sum(std::ostream & out) const {
+        return dump_term_coefficients(out << "(+ ") << ")";
     }
     
-    void dump_term_le_k(std::ostream & out) const {
-        out << "( <= ";
-        dump_term_sum(out);
-        out << m_k << ")";
+    std::ostream& dump_term_le_k(std::ostream & out) const {
+        return dump_term_sum(out << "(<= ") << " " << m_k << ")";
     }
+
     void dump_the_cut_assert(std::ostream & out) const {
-        out <<"(assert (not ";
-        dump_term_le_k(out);
-        out << "))\n";
+        dump_term_le_k(out << "(assert (not ") << "))\n";
     }
+
+
     void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const {
         dump_declarations(out);
         dump_the_row(out);
@@ -272,6 +274,7 @@ public:
         
         // gomory will be   t <= k and the current solution has a property t > k
         m_k = 1;
+        m_t.clear();
         mpq lcm_den(1);
         bool some_int_columns = false;
         mpq f0  = fractional_part(get_value(m_inf_col));
@@ -282,11 +285,6 @@ public:
         mpq one_min_f0 = 1 - f0;
         for (const auto & p : m_row) {
             unsigned j = p.var();
-            if (column_is_fixed(j)) {
-                m_ex.push_justification(column_lower_bound_constraint(j));
-                m_ex.push_justification(column_upper_bound_constraint(j));
-                continue;
-            }
             if (j == m_inf_col) {
                 lp_assert(p.coeff() == one_of_type<mpq>());
                 TRACE("gomory_cut_detail", tout << "seeing basic var";);
@@ -307,11 +305,12 @@ public:
         if (some_int_columns)
             adjust_term_and_k_for_some_ints_case_gomory(lcm_den);
         lp_assert(m_int_solver.current_solution_is_inf_on_cut());
-        m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
-        TRACE("gomory_cut", tout<<"gomory cut:"; print_linear_combination_of_column_indices_only(m_t, tout); tout << " <= " << m_k << std::endl;);
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
+        m_int_solver.m_lar_solver->subs_term_columns(m_t);
+        TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
         return lia_move::cut;
     }
+
     imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :
         m_t(t),
         m_k(k),
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index cc01a0038..83fbe3961 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -125,19 +125,19 @@ constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
 
 bool int_solver::current_solution_is_inf_on_cut() const {
     const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
-    impq v = m_t->apply(x);
-    mpq sign = *m_upper ? one_of_type<mpq>()  : -one_of_type<mpq>();
-    CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign,
-           tout << "m_upper = " << *m_upper << std::endl;
-           tout << "v = " << v << ", k = " << (*m_k) << std::endl;
+    impq v = m_t.apply(x);
+    mpq sign = m_upper ? one_of_type<mpq>()  : -one_of_type<mpq>();
+    CTRACE("current_solution_is_inf_on_cut", v * sign <= m_k * sign,
+           tout << "m_upper = " << m_upper << std::endl;
+           tout << "v = " << v << ", k = " << m_k << std::endl;
           );
-    return v * sign > (*m_k) * sign;
+    return v * sign > m_k * sign;
 }
 
 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);
+    gomory gc(m_t, m_k, m_ex, inf_col, row, *this);
     return gc.create_cut();
 }
 
@@ -147,7 +147,7 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
     if (!is_gomory_cut_target(row)) 
         return create_branch_on_column(j);
 
-    *m_upper = true;
+    m_upper = true;
     return mk_gomory_cut(j, row);
 }
 
@@ -189,7 +189,7 @@ struct check_return_helper {
         m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
         if (m_r == lia_move::cut || m_r == lia_move::branch) {
             int_solver * s = m_lar_solver->get_int_solver();
-            m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
+            // m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
         }
     }
 };
@@ -373,21 +373,21 @@ lia_move int_solver::make_hnf_cut() {
 #else
     vector<mpq> x0;
 #endif
-    lia_move r =  m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
+    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;
+              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();        
+        m_ex.clear();        
         for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
-             m_ex->push_justification(i);
+             m_ex.push_justification(i);
         }
     } 
     return r;
@@ -403,10 +403,13 @@ lia_move int_solver::hnf_cut() {
     return lia_move::undef;
 }
 
-lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) {
+lia_move int_solver::check() {
     if (!has_inf_int()) return lia_move::sat;
 
-    m_t = &t;  m_k = &k;  m_ex = &ex; m_upper = &upper;
+    m_t.clear();
+    m_k.reset();
+    m_ex.clear();
+    m_upper = false;
     lia_move r = run_gcd_test();
     if (r != lia_move::undef) return r;
 
@@ -646,8 +649,8 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
 void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
     constraint_index lc, uc;
     m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc);
-    m_ex->m_explanation.push_back(std::make_pair(mpq(1), lc));
-    m_ex->m_explanation.push_back(std::make_pair(mpq(1), uc));
+    m_ex.m_explanation.push_back(std::make_pair(mpq(1), lc));
+    m_ex.m_explanation.push_back(std::make_pair(mpq(1), uc));
 }
 void int_solver::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
     for (const auto & c : row) {
@@ -1042,20 +1045,20 @@ const impq& int_solver::lower_bound(unsigned j) const {
 
 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(m_t.is_empty());
     lp_assert(j != -1);
-    m_t->add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
+    m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
     if (is_free(j)) {
-        *m_upper = true;
-        *m_k = mpq(0);
+        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_upper = left_branch_is_more_narrow_than_right(j);
+        m_k = m_upper? floor(get_value(j)) : ceil(get_value(j));        
     }
 
     TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
           display_column(tout, j);
-          tout << "k = " << *m_k << std::endl;
+          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 013f53ce0..17ce20481 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -39,19 +39,23 @@ public:
     // fields
     lar_solver          *m_lar_solver;
     unsigned            m_number_of_calls;
-    lar_term            *m_t; // the term to return in the cut
-    mpq                 *m_k; // the right side of the cut
-    explanation         *m_ex; // the conflict explanation
-    bool                *m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
+    lar_term            m_t; // the term to return in the cut
+    mpq                 m_k; // the right side of the cut
+    explanation         m_ex; // the conflict explanation
+    bool                m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
     hnf_cutter          m_hnf_cutter;
     // methods
     int_solver(lar_solver* lp);
 
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
-    lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper);
+    lia_move check();
+    lar_term const& get_term() const { return m_t; }
+    mpq const& get_offset() const { return m_k; }
+    explanation const& get_explanation() const { return m_ex; }
+    bool is_upper() const { return m_upper; }
+
     bool move_non_basic_column_to_bounds(unsigned j);
-    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;
diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h
index ac15028bb..6305089b4 100644
--- a/src/util/lp/lar_constraints.h
+++ b/src/util/lp/lar_constraints.h
@@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint {
     }
     unsigned size() const override { return m_term->size();}
     lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { }
-    mpq get_free_coeff_of_left_side() const override { return m_term->m_v;}
+    // mpq get_free_coeff_of_left_side() const override { return m_term->m_v;}
 
 };
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 56a61177c..30494aa1c 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -137,7 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
             kind = static_cast<lconstraint_kind>(-kind);
         }
         rs_of_evidence /= ratio;
-        rs_of_evidence += t->m_v * ratio;
+        // rs_of_evidence += t->m_v * ratio;
     }
 
     return kind == be.kind() && rs_of_evidence == be.m_bound;
@@ -602,7 +602,7 @@ void lar_solver::register_monoid_in_map(std::unordered_map<var_index, mpq> & coe
 
 
 void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mpq, var_index>>& left_side_with_terms,
-                                                       vector<std::pair<mpq, var_index>> &left_side, mpq & free_coeff) const {
+                                                       vector<std::pair<mpq, var_index>> &left_side) const {
     std::unordered_map<var_index, mpq> coeffs;
     for (auto & t : left_side_with_terms) {
         unsigned j = t.second;
@@ -613,7 +613,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
             for (auto & p : term.coeffs()){
                 register_monoid_in_map(coeffs, t.first * p.second , p.first);
             }
-            free_coeff += t.first * term.m_v;
         }
     }
 
@@ -955,9 +954,9 @@ bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unord
     mpq left_side_val = get_left_side_val(constr, var_map);
     switch (constr.m_kind) {
     case LE: return left_side_val <= constr.m_right_side;
-    case LT: return left_side_val < constr.m_right_side;
+    case LT: return left_side_val <  constr.m_right_side;
     case GE: return left_side_val >= constr.m_right_side;
-    case GT: return left_side_val > constr.m_right_side;
+    case GT: return left_side_val >  constr.m_right_side;
     case EQ: return left_side_val == constr.m_right_side;
     default:
         lp_unreachable();
@@ -976,8 +975,10 @@ bool lar_solver::the_relations_are_of_same_type(const vector<std::pair<mpq, unsi
             flip_kind(m_constraints[con_ind]->m_kind);
         if (kind == GT || kind == LT)
             strict = true;
-        if (kind == GE || kind == GT) n_of_G++;
-        else if (kind == LE || kind == LT) n_of_L++;
+        if (kind == GE || kind == GT) 
+            n_of_G++;
+        else if (kind == LE || kind == LT) 
+            n_of_L++;
     }
     the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ);
     if (strict)
@@ -1117,7 +1118,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value
 bool lar_solver::has_value(var_index var, mpq& value) const {
     if (is_term(var)) {
         lar_term const& t = get_term(var);
-        value = t.m_v;
+        value = 0;
         for (auto const& cv : t) {
             impq const& r = get_column_value(cv.var());
             if (!numeric_traits<mpq>::is_zero(r.y)) return false;
@@ -1229,8 +1230,7 @@ std::ostream& lar_solver::print_constraints(std::ostream& out) const  {
 
 std::ostream& lar_solver::print_terms(std::ostream& out) const  {
     for (auto it : m_terms) {
-        print_term(*it, out);
-        out << "\n";
+        print_term(*it, out) << "\n";
     }
     return out;
 }
@@ -1244,9 +1244,6 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain
 }
 
 std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const {
-    if (!numeric_traits<mpq>::is_zero(term.m_v)) {
-        out << term.m_v << " + ";
-    }
     bool first = true;
     for (const auto p : term) {
         mpq val = p.coeff();
@@ -1270,9 +1267,6 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c
 }
 
 std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const {
-    if (!numeric_traits<mpq>::is_zero(term.m_v)) {
-        out << term.m_v << " + ";
-    }
     print_linear_combination_of_column_indices_only(term, out);
     return out;
 }
@@ -1497,7 +1491,7 @@ bool lar_solver::term_is_int(const lar_term * t) const {
     for (auto const & p :  t->m_coeffs)
         if (! (column_is_int(p.first)  && p.second.is_int()))
             return false;
-    return t->m_v.is_int();
+    return true;
 }
 
 bool lar_solver::var_is_int(var_index v) const {
@@ -1598,17 +1592,13 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
 }
 
 
-var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
-                                         const mpq &m_v) {
-    push_and_register_term(new lar_term(coeffs, m_v));
+var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs) {
+    push_and_register_term(new lar_term(coeffs));
     return m_terms_start_index + m_terms.size() - 1;
 }
 
 #if Z3DEBUG_CHECK_UNIQUE_TERMS
-bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs, const mpq& v) {
-    if (coeffs.empty()) {
-        return is_zero(v);
-    }
+bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs) {
 
     for (const auto & p : coeffs) {
         if (column_is_real(p.second))
@@ -1643,12 +1633,11 @@ void lar_solver::push_and_register_term(lar_term* t) {
 }
 
 // terms
-var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
-                               const mpq &m_v) {
+var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
     if (strategy_is_undecided())
-        return add_term_undecided(coeffs, m_v);
+        return add_term_undecided(coeffs);
 
-    push_and_register_term(new lar_term(coeffs, m_v));
+    push_and_register_term(new lar_term(coeffs));
     unsigned adjusted_term_index = m_terms.size() - 1;
     var_index ret = m_terms_start_index + adjusted_term_index;
     if (use_tableau() && !coeffs.empty()) {
@@ -1656,13 +1645,12 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs,
         if (m_settings.bound_propagation())
             m_rows_with_changed_bounds.insert(A_r().row_count() - 1);
     }
-    CTRACE("add_term_lar_solver", !m_v.is_zero(), print_term(*m_terms.back(), tout););
     lp_assert(m_var_register.size() == A_r().column_count());
     return ret;
 }
 
 void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
-    TRACE("dump_terms", print_term(*term, tout); tout << std::endl;);
+    TRACE("dump_terms", print_term(*term, tout) << std::endl;);
     register_new_ext_var_index(term_ext_index, term_is_int(term));
     // j will be a new variable
     unsigned j = A_r().column_count();
@@ -1744,9 +1732,8 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
     //    lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
     unsigned term_j;
     if (m_var_register.external_is_used(j, term_j)) {
-        mpq rs = right_side - m_terms[adjusted_term_index]->m_v;
         m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
-        update_column_type_and_bound(term_j, kind, rs, ci);
+        update_column_type_and_bound(term_j, kind, right_side, ci);
     }
     else {
         add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
@@ -1755,11 +1742,10 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
 
 constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
     vector<std::pair<mpq, var_index>> left_side;
-    mpq rs = -right_side_parm;
-    substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs);
-    unsigned term_index = add_term(left_side, zero_of_type<mpq>());
+    substitute_terms_in_linear_expression(left_side_with_terms, left_side);
+    unsigned term_index = add_term(left_side);
     constraint_index ci = m_constraints.size();
-    add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci);
+    add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci);
     return ci;
 }
 
@@ -1768,7 +1754,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter
 
     add_row_from_term_no_constraint(term, term_j);
     unsigned j = A_r().column_count() - 1;
-    update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size());
+    update_column_type_and_bound(j, kind, right_side, m_constraints.size());
     m_constraints.push_back(new lar_term_constraint(term, kind, right_side));
     lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
 }
@@ -2266,15 +2252,6 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) {
     } 
 }
 
-void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) {
-    for (const auto& p : t) {
-        if (!is_term(p.var())) continue;
-        const lar_term & p_term = get_term(p.var());
-        if (p_term.m_v.is_zero()) continue;
-        rs -= p.coeff() * p_term.m_v;
-    }
-}
-
 
 } // namespace lp
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3c0ed4fbf..f3aa4f23b 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -164,13 +164,11 @@ public:
 
 
     // terms
-    var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
-                       const mpq &m_v);
+    var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
 
-    var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
-                                 const mpq &m_v);
+    var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);
 
-    bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs, const mpq& v);
+    bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs);
     void push_and_register_term(lar_term* t);
 
     void add_row_for_term(const lar_term * term, unsigned term_ext_index);
@@ -239,8 +237,7 @@ public:
 
     void analyze_new_bounds_on_row_tableau(
         unsigned row_index,
-        bound_propagator & bp
-                                           );
+        bound_propagator & bp);
 
     
     void substitute_basis_var_in_terms_for_row(unsigned i);
@@ -332,7 +329,7 @@ public:
 
 
     void substitute_terms_in_linear_expression( const vector<std::pair<mpq, var_index>>& left_side_with_terms,
-                                                vector<std::pair<mpq, var_index>> &left_side, mpq & free_coeff) const;
+                                                vector<std::pair<mpq, var_index>> &left_side) const;
 
 
     void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j);
@@ -535,7 +532,7 @@ public:
         return m_columns_to_ul_pairs()[j].lower_bound_witness();
     }
 
-    void subs_term_columns(lar_term& t, mpq & rs) {
+    void subs_term_columns(lar_term& t) {
         vector<std::pair<unsigned,unsigned>> columns_to_subs;
         for (const auto & m : t.m_coeffs) {
             unsigned tj = adjust_column_index_to_term_index(m.first);
@@ -549,8 +546,6 @@ public:
             mpq v = it->second;
             t.m_coeffs.erase(it);
             t.m_coeffs[p.second] = v;
-            if (lt.m_v.is_zero()) continue;
-            rs -= v * lt.m_v;
         }
     }
 
@@ -587,6 +582,5 @@ public:
     lar_term get_term_to_maximize(unsigned ext_j) const;
     void set_cut_strategy(unsigned cut_frequency);
     bool sum_first_coords(const lar_term& t, mpq & val) const;
-    void adjust_cut_for_terms(const lar_term& t, mpq & rs);
 };
 }
diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h
index 519847848..e9259b8c0 100644
--- a/src/util/lp/lar_term.h
+++ b/src/util/lp/lar_term.h
@@ -21,9 +21,9 @@
 #include "util/lp/indexed_vector.h"
 namespace lp {
 struct lar_term {
-    // the term evaluates to sum of m_coeffs + m_v
+    // the term evaluates to sum of m_coeffs 
     std::unordered_map<unsigned, mpq> m_coeffs;
-    mpq m_v;
+    // mpq m_v;
     lar_term() {}
     void add_monomial(const mpq& c, unsigned j) {
         auto it = m_coeffs.find(j);
@@ -37,7 +37,7 @@ struct lar_term {
     }
 
     bool is_empty() const {
-        return m_coeffs.size() == 0 && is_zero(m_v);
+        return m_coeffs.size() == 0; // && is_zero(m_v);
     }
     
     unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
@@ -46,8 +46,7 @@ struct lar_term {
         return m_coeffs;
     }
     
-    lar_term(const vector<std::pair<mpq, unsigned>>& coeffs,
-             const mpq & v) : m_v(v) {
+    lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
         for (const auto & p : coeffs) {
             add_monomial(p.first, p.second);
         }
@@ -87,7 +86,7 @@ struct lar_term {
 
     template <typename T>
     T apply(const vector<T>& x) const {
-        T ret = T(m_v);
+        T ret(0);
         for (const auto & t : m_coeffs) {
             ret += t.second * x[t.first];
         }
@@ -96,7 +95,6 @@ struct lar_term {
    
     void clear() {
         m_coeffs.clear();
-        m_v = zero_of_type<mpq>();
     }
 
     struct ival {
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 41b6fe31d..9a6549917 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -577,7 +577,7 @@ public:
     }
 
     void print_column_info(unsigned j, std::ostream & out) const {
-        out << "j = " << j << ", name = "<< column_name(j);
+        out << "j = " << j << ",\tname = "<< column_name(j) << "\t";
         switch (m_column_types[j]) {
         case column_type::fixed:
         case column_type::boxed:
@@ -596,11 +596,11 @@ public:
             lp_assert(false);
         }
         //        out << "basis heading = " << m_basis_heading[j] << std::endl;
-        out << " x =                " << m_x[j];
+        out << "\tx = " << m_x[j];
         if (m_basis_heading[j] >= 0)
             out << " base\n";
         else
-            out << " nbas\n";
+           out << " \n";
     }
 
     bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }