diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp
index d2c580c872..8baf0cdd69 100644
--- a/src/ast/euf/ho_matcher.cpp
+++ b/src/ast/euf/ho_matcher.cpp
@@ -609,8 +609,6 @@ namespace euf {
             return false;
         if (block_inference(wi))
             return false;
-        if (wi.index() > 1)
-            return false;
 
         // Introduce three fresh meta-variables C, Tr, El and bind
         //   v -> \xs . ite(C xs, Tr xs, El xs)
@@ -619,7 +617,6 @@ namespace euf {
         // The condition/branch split is performed later when the ite subgoal
         // is consumed (see the is_ite(p, ...) case in consume_work).
 
-        wi.inc_index();
         m_trail.push(undo_resize(m_subst));
 
         flex_frame fr(m);
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 7b685db9e8..3b245981d5 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -205,7 +205,7 @@ namespace nla {
             if (!c().is_monic_var(v))
                 continue;
             monic& m = c().emon(v);
-            if (propagate_changed_bound(m))
+            if (propagate_linear_bound(m))
                 propagated = true;
             if (tighten_lp(m))
                 propagated = true;
@@ -215,6 +215,20 @@ namespace nla {
         return propagated;
     }
 
+    bool monomial_bounds::propagate_linear_bounds() {
+        bool propagated = false;
+        for (auto& mm : c().emons()) {
+            //if (!c().is_monic_var(v))
+            //    continue;
+            monic &m = c().emon(mm.var());
+            if (propagate_linear_bound(m))
+                propagated = true;
+            if (c().lra.get_status() == lp::lp_status::INFEASIBLE)
+                break;
+        }
+        return propagated;
+    }
+
     bool monomial_bounds::add_lemma() {
         if (c().lra.get_status() != lp::lp_status::INFEASIBLE)
             return false;
@@ -225,7 +239,7 @@ namespace nla {
         return true;
     }
 
-    bool monomial_bounds::propagate_changed_bound(monic & m) {
+    bool monomial_bounds::propagate_linear_bound(monic & m) {
         if (m.is_propagated())
             return false;
         lpvar w, fixed_to_zero;
@@ -285,8 +299,10 @@ namespace nla {
     }
 
     bool monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
-        if (c().val(m.var()) == k * c().val(w))
-            return false;
+        if (c().val(m.var()) == k * c().val(w)) {
+            verbose_stream() << "non-fixed\n";
+            //return false;
+        }
         vector<std::pair<lp::mpq, unsigned>> coeffs;        
         coeffs.push_back({-k, w});
         coeffs.push_back({rational::one(), m.var()});
@@ -671,7 +687,7 @@ namespace nla {
        
     bool monomial_bounds::tighten_lp_bounds() {
         bool new_bound = false;
-        for (auto &m : c().emons()) 
+        for (auto &m : c().emons())
             if (tighten_lp(m))
                 new_bound = true;
         return new_bound;
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 3a27bad11a..c88285ff53 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -48,7 +48,7 @@ namespace nla {
         // linear-monomial equality propagation:
         // when all but one variable of a monomial are fixed, the monomial is
         // linear and its value/equality can be propagated into the LP solver.
-        bool propagate_changed_bound(monic & m);
+        bool propagate_linear_bound(monic & m);
         bool is_linear(monic const& m, lpvar& w, lpvar & fixed_to_zero);
         rational fixed_var_product(monic const& m, lpvar w);
 
@@ -88,6 +88,7 @@ namespace nla {
         monomial_bounds(core* core);
         void generate_lemmas();
         bool tighten_lp_bounds();
+        bool propagate_linear_bounds();
         bool propagate_changed_bounds();
         bool propagate_fixed_rows();