diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg
index c3d50ab86..9930265bd 100644
--- a/src/math/lp/lp_params_helper.pyg
+++ b/src/math/lp/lp_params_helper.pyg
@@ -9,5 +9,6 @@ def_module_params(module_name='lp',
                           ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
                           ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
                           ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),                          
+                          ('enable_relevancy', BOOL, False, 'enable relevancy propagation to filter emons (experiment)')
                          ))
                          
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index 42d6d8ef6..62432320e 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -44,4 +44,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
     m_dio_calls_period = lp_p.dio_calls_period();
     m_dio_run_gcd = lp_p.dio_run_gcd();
     m_max_conflicts = p.max_conflicts();
+    m_enable_relevancy = lp.enable_relevancy();
 }
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index d86b7d70e..afa73c70e 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -259,6 +259,7 @@ private:
     unsigned         m_dio_calls_period = 4;
     bool             m_dio_run_gcd = true;
 public:
+    bool m_enable_relevancy = false;
     unsigned dio_calls_period() const { return m_dio_calls_period; }
     unsigned & dio_calls_period() { return m_dio_calls_period; }
     bool print_external_var_name() const { return m_print_external_var_name; }
diff --git a/src/math/lp/nla_mul_saturate.cpp b/src/math/lp/nla_mul_saturate.cpp
index fe1a3a043..6a9c5c047 100644
--- a/src/math/lp/nla_mul_saturate.cpp
+++ b/src/math/lp/nla_mul_saturate.cpp
@@ -31,10 +31,10 @@ namespace nla {
             for (auto& con : lra.constraints().active()) {                
                 for (auto v : m.vars()) {
                     for (auto [coeff, u] : con.coeffs()) {
-                        if (u == v) {
-                            // add new constraint
+                        if (u == v) 
                             // multiply by remaining vars
-                        }
+                            multiply_constraint(con, m, v);
+                            // add new constraint
                     }
                 }
             }
@@ -55,8 +55,53 @@ namespace nla {
         return r;
     }
 
-    lp::lar_base_constraint* mul_saturate::multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x) {
+    // multiply by remaining vars
+    void mul_saturate::multiply_constraint(lp::lar_base_constraint const& con, monic const& m, lpvar x) {
+        auto const& lhs = con.coeffs();
+        auto const& rhs = con.rhs();
+        auto k = con.kind();
+        auto sign = false;
+        svector<lpvar> vars;
+        bool first = true;
+        for (auto v : m.vars()) {
+            if (v != x || !first)
+                vars.push_back(v);
+            else
+                first = false;
+        }
+        vector<std::pair<rational, lpvar>> new_lhs;
+        rational new_rhs(rhs);
+        for (auto [coeff, v] : lhs) {
+            vars.push_back(v);
 
-        return nullptr;
+            auto new_m = c().emons().find_canonical(vars);
+            if (!new_m) {
+                bool is_int = lra.var_is_int(x);  // assume all vars in monic have the same type, can be changed for MIP
+                lpvar new_monic_var = 0; // lra.add_var(is_int);
+                c().emons().add(new_monic_var, vars);
+                new_m = c().emons().find_canonical(vars);
+                SASSERT(new_m);
+            }
+            new_lhs.push_back({coeff, new_m->var()});
+            vars.pop_back();
+        }
+        if (rhs != 0) {
+            new_lhs.push_back({-rhs, m.var()});
+            new_rhs = 0;
+        }
+        // compute sign of vars
+        for (auto v : vars) 
+            if (c().val(v).is_neg())
+                sign = !sign;
+        if (sign) {
+            switch (k) {
+            case lp::lconstraint_kind::LE: k = lp::lconstraint_kind::GE; break;
+            case lp::lconstraint_kind::LT: k = lp::lconstraint_kind::GT; break;
+            case lp::lconstraint_kind::GE: k = lp::lconstraint_kind::LE; break;
+            case lp::lconstraint_kind::GT: k = lp::lconstraint_kind::LT; break;
+            default: break;
+            }
+        }
+        // instead of adding a constraint here, add row to tableau based on the new_lhs, new_rhs, k.
     }
 }
diff --git a/src/math/lp/nla_mul_saturate.h b/src/math/lp/nla_mul_saturate.h
index fac751bb6..f13bf8a7d 100644
--- a/src/math/lp/nla_mul_saturate.h
+++ b/src/math/lp/nla_mul_saturate.h
@@ -10,7 +10,7 @@ namespace nla {
     class lar_solver;
     class mul_saturate : common {
         lp::lar_solver& lra;
-        lp::lar_base_constraint* multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x);
+        void multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x);
     public:
         mul_saturate(core* core);