diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index ac7e89d5b..9e7ac75ce 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1299,7 +1299,7 @@ namespace opt {
         def result;
         unsigned_vector div_rows(_div_rows), mod_rows(_mod_rows);
         SASSERT(!div_rows.empty() || !mod_rows.empty());
-        TRACE("opt", display(tout << "solve_div " << x << "\n"));
+        TRACE("opt", display(tout << "solve_div v" << x << "\n"));
 
         rational K(1);
         for (unsigned ri : div_rows)
diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index e97eb4ef7..5d9d3c19c 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -421,15 +421,23 @@ namespace mbp {
             mbo.display(tout););
             vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
 
+
             vector<row> rows;
+            u_map<row> def_vars;
             mbo.get_live_rows(rows);
-            rows2fmls(rows, index2expr, fmls);
+            for (row const& r : rows) {
+                if (r.m_type == opt::t_mod)
+                    def_vars.insert(r.m_id, r);
+                else if (r.m_type == opt::t_div)
+                    def_vars.insert(r.m_id, r);
+            }
+            rows2fmls(def_vars, rows, index2expr, fmls);
             TRACE("qe", mbo.display(tout << "mbo result\n");
             for (auto const& d : defs) tout << "def: " << d << "\n";
             tout << fmls << "\n";);
 
             if (compute_def)
-                optdefs2mbpdef(defs, index2expr, real_vars, result);
+                optdefs2mbpdef(def_vars, defs, index2expr, real_vars, result);
             if (m_apply_projection && !apply_projection(eval, result, fmls))
                 return false;
 
@@ -442,7 +450,7 @@ namespace mbp {
             return true;
         }
 
-        void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
+        void optdefs2mbpdef(u_map<row> const& def_vars, vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
             SASSERT(defs.size() == real_vars.size());
             for (unsigned i = 0; i < defs.size(); ++i) {
                 auto const& d = defs[i];
@@ -450,8 +458,12 @@ namespace mbp {
                 bool is_int = a.is_int(x);
                 expr_ref_vector ts(m);
                 expr_ref t(m);
-                for (var const& v : d.m_vars)
-                    ts.push_back(var2expr(index2expr, v));
+                for (var const& v : d.m_vars) {
+                    t = id2expr(def_vars, index2expr, v.m_id);
+                    if (v.m_coeff != 1)
+                        t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
+                    ts.push_back(t);
+                }
                 if (!d.m_coeff.is_zero())
                     ts.push_back(a.mk_numeral(d.m_coeff, is_int));
                 if (ts.empty())
@@ -492,7 +504,8 @@ namespace mbp {
                     t = a.mk_int(mod(r.m_coeff, r.m_mod));
                     return t;
                 }
-                ts.push_back(a.mk_int(r.m_coeff));
+                if (r.m_coeff != 0)
+                    ts.push_back(a.mk_int(r.m_coeff));
                 t = mk_add(ts);
                 t = a.mk_mod(t, a.mk_int(r.m_mod));
                 return t;
@@ -501,7 +514,8 @@ namespace mbp {
                     t = a.mk_int(div(r.m_coeff, r.m_mod));
                     return t;
                 }
-                ts.push_back(a.mk_int(r.m_coeff));
+                if (r.m_coeff != 0)
+                    ts.push_back(a.mk_int(r.m_coeff));
                 t = mk_add(ts);
                 t = a.mk_idiv(t, a.mk_int(r.m_mod));
                 return t;
@@ -513,15 +527,7 @@ namespace mbp {
             }
         }
 
-        void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
-
-            u_map<row> def_vars;
-            for (row const& r : rows) {
-                if (r.m_type == opt::t_mod)
-                    def_vars.insert(r.m_id, r);
-                else if (r.m_type == opt::t_div)
-                    def_vars.insert(r.m_id, r);
-            }
+        void rows2fmls(u_map<row>& def_vars, vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
 
             for (row const& r : rows) {
                 expr_ref t(m), s(m), val(m);