diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 99bae39bc..2249eba8d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3161,7 +3161,7 @@ public:
             return l_false;
         case lp::lp_status::FEASIBLE:
         case lp::lp_status::OPTIMAL:
-            SASSERT(lp().all_constraints_hold());
+            //            SASSERT(lp().all_constraints_hold());
             return l_true;
         case lp::lp_status::TIME_EXHAUSTED:
                 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 15e2b7615..7c7320a73 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -880,12 +880,12 @@ void lar_solver::fix_Ax_b_on_rounded_row(unsigned i) {
     if (A_r().m_rows.size() <= i)
         return;
     unsigned bj = m_mpq_lar_core_solver.m_r_basis[i];
-    auto& v = m_mpq_lar_core_solver.m_r_x[bj];
-    v = zero_of_type<numeric_pair<mpq>>();
+    auto v = zero_of_type<impq>();
     for (const auto & c : A_r().m_rows[i]) {
         if (c.var() != bj) 
             v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()];
     }
+    m_mpq_lar_core_solver.m_r_solver.update_x_with_feasibility_tracking(bj, v);
 }
 void lar_solver::collect_rounded_rows_to_fix() {
     lp_assert(m_cube_rounded_rows.size() == 0);
@@ -1622,6 +1622,7 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() {
             m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j);
         lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
     }
+    SASSERT(m_mpq_lar_core_solver.m_r_solver.inf_set_is_correct());
 }
 
 bool lar_solver::model_is_int_feasible() const {
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 081b7124a..b9cbc64d9 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -394,7 +394,7 @@ public:
     bool make_column_feasible(unsigned j, numeric_pair<mpq> & delta) {
         bool ret = false;
         lp_assert(m_basis_heading[j] < 0);
-        auto & x = m_x[j];
+        const auto & x = m_x[j];
         switch (m_column_types[j]) {
         case column_type::fixed:
             lp_assert(m_lower_bounds[j] == m_upper_bounds[j]);
@@ -429,7 +429,7 @@ public:
             break;
         }
         if (ret)
-            add_delta_to_x_and_call_tracker(j, delta);
+            add_delta_to_x_and_do_not_track_feasibility(j, delta);
 
         return ret;
         
@@ -694,10 +694,10 @@ public:
         m_x[j] = v;
     }
 
-    void add_delta_to_x_and_call_tracker(unsigned j, const X & delta) {
+    void add_delta_to_x_and_do_not_track_feasibility(unsigned j, const X & delta) {
         m_x[j] += delta;
     }
-    
+   
     void track_column_feasibility(unsigned j) {
         if (column_is_feasible(j))
             remove_column_from_inf_set(j);
diff --git a/src/util/lp/lp_primal_core_solver_tableau_def.h b/src/util/lp/lp_primal_core_solver_tableau_def.h
index f2b6309f2..2d6eb95d6 100644
--- a/src/util/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/util/lp/lp_primal_core_solver_tableau_def.h
@@ -358,7 +358,7 @@ update_basis_and_x_tableau(int entering, int leaving, X const & tt) {
 }
 template <typename T, typename X> void lp_primal_core_solver<T, X>::
 update_x_tableau(unsigned entering, const X& delta) {
-    this->add_delta_to_x_and_call_tracker(entering, delta);
+    this->add_delta_to_x_and_do_not_track_feasibility(entering, delta);
     if (!this->m_using_infeas_costs) {
         for (const auto & c : this->m_A.m_columns[entering]) {
             unsigned i = c.var();
@@ -371,7 +371,7 @@ update_x_tableau(unsigned entering, const X& delta) {
         for (const auto & c : this->m_A.m_columns[entering]) {
             unsigned i = c.var();
             unsigned j = this->m_basis[i];
-            this->add_delta_to_x_and_call_tracker(j, -delta * this->m_A.get_val(c));
+            this->add_delta_to_x_and_do_not_track_feasibility(j, -delta * this->m_A.get_val(c));
             update_inf_cost_for_column_tableau(j);
             if (is_zero(this->m_costs[j]))
                 this->remove_column_from_inf_set(j);