diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 4049d7204..43acce576 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1822,6 +1822,7 @@ namespace lp {
 
         if (is_base(j) && column_is_fixed(j))
             m_fixed_base_var_set.insert(j);
+        track_column_feasibility(j);
         TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << " val = " << get_column_value(j) << std::endl;);   
     }
 
@@ -2359,7 +2360,8 @@ namespace lp {
     // dep is the reason for the new bound
 
     void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
-        SASSERT(m_crossed_bounds_deps == nullptr && m_crossed_bounds_deps == nullptr);
+        if (m_crossed_bounds_column != null_lpvar) return; // already set
+        SASSERT(m_crossed_bounds_deps == nullptr);
         set_status(lp_status::INFEASIBLE);
         m_crossed_bounds_column = j;
         const auto& ul = this->m_columns_to_ul_pairs()[j];
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 0748d2507..9b0dd8381 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -152,7 +152,8 @@ public:
 
     lpvar crossed_bounds_column() const { return m_crossed_bounds_column; }
     lpvar& crossed_bounds_column() { return m_crossed_bounds_column; } 
-        
+    bool current_x_is_feasible() const { return m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible(); }     
+    
 
 private:   
     void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 8bb6ab306..0e4a5041e 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -311,8 +311,8 @@ namespace nla {
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
         
         // propagate fixed equality
-        auto exp = get_explanation(dep);
-        c().add_fixed_equality(m.var(), k, exp);
+        auto exp = get_explanation(dep);        
+        c().add_fixed_equality(c().lra.column_to_reported_index(m.var()), k, exp);
     }
 
     void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
@@ -327,7 +327,7 @@ namespace nla {
 
         if (k == 1) {
             lp::explanation exp = get_explanation(dep);
-            c().add_equality(m.var(), w, exp);
+            c().add_equality(c().lra.column_to_reported_index(m.var()), c().lra.column_to_reported_index(w), exp);
         }
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b746a88bf..7f7951b20 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2212,6 +2212,10 @@ public:
     }
     
     void propagate_bounds_with_lp_solver() {
+        if (!lp().current_x_is_feasible()) {  
+            lp().clear_columns_with_changed_bounds();
+            return;
+        }
         m_bp.init();
         lp().propagate_bounds_for_touched_rows(m_bp);