diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 4f5c1f9cf..46666b892 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -119,7 +119,6 @@ namespace arith {
             literal lit = eq_internalize(n, e);
             add_unit(lit);
         }
-
     }
 
     lpvar solver::add_const(int c, lpvar& var, bool is_int) {
@@ -299,6 +298,11 @@ namespace arith {
         st.to_ensure_var().reset();
     }
 
+    void solver::eq_internalized(enode* n) {
+        internalize_term(n->get_arg(0)->get_expr());
+        internalize_term(n->get_arg(1)->get_expr());
+    }
+
     bool solver::internalize_atom(expr* atom) {
         TRACE("arith", tout << mk_pp(atom, m) << "\n";);
         SASSERT(!ctx.get_enode(atom));
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index f0b084c9a..a3dca72dd 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -432,6 +432,7 @@ namespace arith {
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
+        void eq_internalized(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override {}
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index f7a204014..9f0dbda26 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -203,14 +203,25 @@ namespace q {
     expr_ref mbqi::solver_project(model& mdl, q_body& qb) {
         for (app* v : qb.vars)
             m_model->register_decl(v->get_decl(), mdl(v));
-        TRACE("q",
-            tout << "Project\n";
-        tout << *m_model << "\n";
-        tout << qb.vbody << "\n";
-        tout << "model of projection\n" << mdl << "\n";);
         expr_ref_vector fmls(qb.vbody);
         app_ref_vector vars(qb.vars);
         fmls.append(qb.domain_eqs);
+        TRACE("q",
+            tout << "Project\n";
+        tout << *m_model << "\n";
+        tout << fmls << "\n";
+        tout << "model of projection\n" << mdl << "\n";
+        tout << "var args: " << qb.var_args.size() << "\n";
+        for (expr* f : fmls)
+            if (m_model->is_false(f))
+                tout << mk_pp(f, m) << " := false\n";
+        );
+        // 
+        // TBD: need to compute projection based on eliminate_nested_vars,
+        // but apply it based on original formulas, or add constraints that
+        // nested variable occurrences are equal to their subsitutions.
+        // The result may not be a proper projection.
+        // 
         eliminate_nested_vars(fmls, qb);
         mbp::project_plugin proj(m);
         proj.extract_literals(*m_model, vars, fmls);
@@ -220,17 +231,6 @@ namespace q {
             if (p)
                 (*p)(*m_model, vars, fmls);
         }
-#if 0
-        // should be redundant
-        expr_safe_replace esubst(m);
-        for (app* v : qb.vars) {
-            expr_ref val = assign_value(*m_model, v);
-            if (!val)
-                return expr_ref(m);
-            esubst.insert(v, val);
-        }
-        esubst(fmls);
-#endif
         return mk_and(fmls);
     }