diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 08dc81cdf..16d851e87 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1950,14 +1950,20 @@ namespace lp {
                     tout << std::endl;
                 }
             });
+        bool was_fixed = column_is_fixed(j);
         mpq rs = adjust_bound_for_int(j, kind, right_side);
         if (column_has_upper_bound(j))
             update_column_type_and_bound_with_ub(j, kind, rs, dep);
         else
             update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
 
-        if (is_base(j) && column_is_fixed(j))
+        if (!was_fixed && column_is_fixed(j) && m_fixed_var_eh)
+            m_fixed_var_eh(j);
+
+        if (is_base(j) && column_is_fixed(j)) 
             m_fixed_base_var_set.insert(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") << std::endl;);
     }
 
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 2c58bbd45..c3935d24d 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -311,6 +311,7 @@ public:
 
     inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
 
+    std::function<void(lpvar)> m_fixed_var_eh;
     template <typename T>
     void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
         u_dependency* dep = ib.explain_implied();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 821b5be2a..f3ffc9854 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -254,6 +254,47 @@ class theory_lra::imp {
         return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
     }
 
+    svector<theory_var> m_fixed_vars;
+    unsigned       m_fixed_vars_head = 0;
+
+    bool propagate_fixed_vars() {
+        if (m_fixed_vars_head == m_fixed_vars.size())
+            return false;
+        ctx().push_trail(value_trail(m_fixed_vars_head));
+        bool propagated = false;
+        while (m_fixed_vars_head < m_fixed_vars.size()) {
+            theory_var v = m_fixed_vars[m_fixed_vars_head++];
+            enode* n = th.get_enode(v);
+            for (enode* p : n->get_parents()) {
+                expr* e = p->get_expr();
+                expr* x, * y;
+                if (!a.is_mul(e, x, y))
+                    continue;
+                if (a.is_numeral(x) || a.is_numeral(y))
+                    continue;
+                if (x == n->get_expr()) {
+                    std::swap(x, y);
+                }
+                if (y != n->get_expr())
+                    continue;
+
+                // comment out to enable propagation:
+                continue;
+
+                expr_ref k(a.mk_numeral(get_value(v), a.is_int(y)), m);
+                expr_ref eq(a.mk_eq(y, k), m);
+                literal eq1 = th.mk_eq(y, k, false);
+                literal eq2 = th.mk_eq(e, a.mk_mul(x, k), false);
+                ctx().mk_th_axiom(get_id(), ~eq1, eq2);
+
+                // v2 could perform propagation directly
+                // v3 could consider multiplication of more than two variables.
+                // such as e := x * y * z. If both x, y become fixed we have e = z * value(x) * value(y)
+//                verbose_stream() << mk_bounded_pp(e, m) << " - " << mk_bounded_pp(n->get_expr(), m) << "\n";
+            }
+        }
+        return propagated;
+    }
     void ensure_nla() {
         if (!m_nla) {
             m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
@@ -266,6 +307,7 @@ class theory_lra::imp {
                 return ctx().is_relevant(th.get_enode(u));
             };
             m_nla->set_relevant(is_relevant);
+
         }
     }
 
@@ -873,6 +915,18 @@ public:
         lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_lia = alloc(lp::int_solver, *m_solver.get());
+
+        std::function<void(lpvar)> new_fixed = [&](lpvar v) {
+            theory_var u = lp().local_to_external(v);
+            if (u == null_theory_var)
+                return;
+            expr* var = th.get_expr(u);
+            if (a.is_numeral(var))
+                return;
+            m_fixed_vars.push_back(u);
+            ctx().push_trail(push_back_vector(m_fixed_vars));
+        };
+        lp().m_fixed_var_eh = new_fixed;
     }
         
     void internalize_is_int(app * n) {
@@ -2083,7 +2137,7 @@ public:
     }
 
     bool propagate() {
-        return process_atoms() && propagate_core();        
+        return process_atoms() && propagate_core() && propagate_fixed_vars();
     }
 
     bool propagate_core() {