diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 83fbe3961..0967c6cc6 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -187,10 +187,6 @@ struct check_return_helper {
     ~check_return_helper() {
         TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
         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));
-        }
     }
 };
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 436e6ab04..5b3028a98 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -27,7 +27,7 @@ void clear() {lp_assert(false); // not implemented
 }
 
 
-lar_solver::lar_solver() : m_status(lp_status::OPTIMAL),
+lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
                            m_infeasible_column_index(-1),
                            m_terms_start_index(1000000),
                            m_mpq_lar_core_solver(m_settings, *this),
@@ -1174,6 +1174,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
         std::unordered_set<impq> set_of_different_pairs; 
         std::unordered_set<mpq> set_of_different_singles;
         delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
+        TRACE("get_model", tout << "delta=" << delta << "size = " << m_mpq_lar_core_solver.m_r_x.size() << std::endl;);
         for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
             const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
             set_of_different_pairs.insert(rp);
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index cfe581ba3..4189bad4e 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -542,7 +542,6 @@ public:
         for (const auto & p : columns_to_subs) {
             auto it = t.m_coeffs.find(p.first);
             lp_assert(it != t.m_coeffs.end());
-            const lar_term& lt = get_term(p.second);
             mpq v = it->second;
             t.m_coeffs.erase(it);
             t.m_coeffs[p.second] = v;