diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index bd1ac5313..1964262f3 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -31,7 +31,7 @@ namespace lp {
         lra.remove_fixed_vars_from_base();
         lp_assert(lia.is_feasible());
         for (unsigned j : lra.r_basis()) 
-            if (!lra.get_value(j).is_int() && lra.column_is_int(j)&& !lia.is_fixed(j))
+            if (!lra.get_value(j).is_int() && lra.column_is_int(j) && !lia.is_fixed(j))
                 patch_basic_column(j);
         if (!lia.has_inf_int()) {
             lia.settings().stats().m_patches_success++;
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 8061444c8..e21891ee4 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -258,23 +258,11 @@ namespace nla {
         }
     }
 
-    void monomial_bounds::unit_propagate() {  
-        for (auto const& m : c().m_emons)
+    void monomial_bounds::unit_propagate() {        
+        for (auto const& m : c().m_emons) 
             unit_propagate(m);
     }
 
-    void monomial_bounds::check_for_conflict() {
-        if (c().lra.crossed_bounds_deps() != nullptr) {
-            new_lemma lemma(c(), "fixed-values");
-            lp::explanation ex;
-            c().lra.fill_explanation_from_crossed_bounds_column(ex);
-            lemma &= ex;
-            c().lra.crossed_bounds_deps() = nullptr;
-            c().lra.crossed_bounds_column() = null_lpvar;     
-            c().lra.set_status(lp::lp_status::OPTIMAL);           
-        }
-    }
-
     void monomial_bounds::unit_propagate(monic const& m) {
         m_propagated.reserve(m.var() + 1, false);
         if (m_propagated[m.var()])
@@ -284,80 +272,37 @@ namespace nla {
             return;
         
         c().trail().push(set_bitvector_trail(m_propagated, m.var()));
-        lpvar zero_fixed = null_lpvar, non_fixed = null_lpvar;
-        // find a zero fixed variable and a non-fixed variable
-        for (lpvar v : m) {
-            if (c().var_is_fixed(v)) {
-                if (c().val(v).is_zero()) {
-                    zero_fixed = v;
+        
+        rational k = fixed_var_product(m);
+        
+        new_lemma lemma(c(), "fixed-values");
+        if (k == 0) {
+            for (auto v : m) {
+                if (c().var_is_fixed(v) && c().val(v).is_zero()) {
+                    lemma.explain_fixed(v);
                     break;
                 }
             }
-            else {
-                non_fixed = v;
-            }
+            lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
         }
-
-        if (zero_fixed != null_lpvar) {
-            // the m.var() has to have a zero value
-            u_dependency* d = this->dep.mk_join(c().lra.get_column_lower_bound_witness(zero_fixed),
-                                                c().lra.get_column_upper_bound_witness(zero_fixed));            
-            c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, mpq(0), d);
-        } else if (non_fixed != null_lpvar) {
-            u_dependency* d = nullptr;
-            rational k(1);
-            for (auto v : m)
-                if (v != non_fixed) {
-                    d = this->dep.mk_join(d, c().lra.get_column_upper_bound_witness(v));
-                    d = this->dep.mk_join(d, c().lra.get_column_lower_bound_witness(v));
-                    k *= c().val(v);
-                }
-            SASSERT(k.is_pos() || k.is_neg());
-            // we have m = k* non_fixed: m.var() getting the bounds witnesses of non_fixed
-            if (k.is_pos()) {
-                d = c().lra.get_column_upper_bound_witness(non_fixed);
-                if (d) {
-                    const auto& b = c().lra.get_column_value(non_fixed);
-                    bool strict = b.y.is_neg();
-                    c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE, k * b.x, d);
-                }
-                d = c().lra.get_column_lower_bound_witness(non_fixed);
-                if (d) {
-                    const auto& b = c().lra.get_column_value(non_fixed);
-                    bool strict = b.y.is_pos();
-                    c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE, k * b.x, d);
-                }
+        else {
+            for (auto v : m) 
+                if (c().var_is_fixed(v)) 
+                    lemma.explain_fixed(v);
+            
+            lpvar w = non_fixed_var(m);
+            if (w != null_lpvar) {
+                lp::lar_term term;
+                term.add_var(m.var());
+                term.add_monomial(-k, w);
+                lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
             } else {
-                d = c().lra.get_column_upper_bound_witness(non_fixed);
-                if (d) {
-                    const auto& b = c().lra.get_column_value(non_fixed);
-                    bool strict = b.y.is_neg();
-                    c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE, k * b.x, d);
-                }
-                d = c().lra.get_column_lower_bound_witness(non_fixed);
-                if (d) {
-                    const auto& b = c().lra.get_column_value(non_fixed);
-                    bool strict = b.y.is_pos();
-                    c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE, k * b.x, d);                    
-                }
+                lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
             }
-        } else {
-            SASSERT(non_fixed == null_lpvar && zero_fixed == null_lpvar);
-            rational k(1);
-            u_dependency* d = nullptr;
-            for (auto v : m) {
-                SASSERT(c().var_is_fixed(v));
-                d = this->dep.mk_join(d, c().lra.get_column_upper_bound_witness(v));
-                d = this->dep.mk_join(d, c().lra.get_column_lower_bound_witness(v));
-                k *= c().val(v);
-            }
-            SASSERT(k.is_pos() || k.is_neg());
-            // we have m = k: m.var() getting the bounds witnesses of all fixed variables
-            c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, d);
         }
-        check_for_conflict();
-        SASSERT (c().lra.get_status() != lp::lp_status::INFEASIBLE);
+        
     }
+    
     bool monomial_bounds::is_linear(monic const& m) {
         unsigned non_fixed = 0;
         for (lpvar v : m) {
@@ -379,6 +324,12 @@ namespace nla {
         return r;
     }
     
-   
+    lpvar monomial_bounds::non_fixed_var(monic const& m) {
+        for (lpvar v : m) 
+            if (!c().var_is_fixed(v))
+                return v;
+        return null_lpvar;
+    }
+
 }
 
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 9faf0e470..c728d1a4c 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -35,10 +35,11 @@ namespace nla {
         void unit_propagate(monic const& m);
         bool is_linear(monic const& m);
         rational fixed_var_product(monic const& m);
+        lpvar non_fixed_var(monic const& m);
+
     public:
         monomial_bounds(core* core);
         void propagate();
         void unit_propagate();
-        void check_for_conflict();
     }; 
 }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 08a768ee5..4d4fa6cbe 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1818,18 +1818,14 @@ bool core::improve_bounds() {
     }
     return bounds_improved;
 }
-    // returns false if and only if makes lp_solver inconsistent
-bool core::propagate(vector<lemma>& lemmas) {
+    
+void core::propagate(vector<lemma>& lemmas) {
    // propagate linear monomials, those that have all, or all but one, variables fixed
     lemmas.reset();
     m_lemma_vec = &lemmas;
  
     m_monomial_bounds.unit_propagate();
-    if (lra.get_status() == lp::lp_status::INFEASIBLE) {
-        TRACE("nla_solver", tout << "propagation found infeasibility\n";);
-        return false;
-    }
-    return true;
+   
 }
 
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 340b94430..9c96f2fbf 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -392,7 +392,7 @@ public:
 
     bool  no_lemmas_hold() const;
 
-    bool propagate(vector<lemma>& lemmas);
+    void propagate(vector<lemma>& lemmas);
     
     lbool  test_check(vector<lemma>& l);
     lpvar map_to_root(lpvar) const;