diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 23bab1761..fc620d757 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -150,9 +150,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         auto st = reduce_app_core(f, num, args, result, result_pr);
         CTRACE("model_evaluator", st != BR_FAILED, 
-               tout << f->get_name() << "\n";
-               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << "\n";
-               tout << result << "\n";);
+               tout << f->get_name() << "  ";
+               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
+               tout << "\n--> " << result << "\n";);
                
         return st;
     }
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 802e3d393..5c30bedd4 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -299,13 +299,12 @@ namespace q {
             auto* p = get_plugin(v);
             if (p && !fmls_extracted) {
                 TRACE("q", tout << "domain eqs\n" << qb.domain_eqs << "\n";);
-                
-                for (expr* e : qb.domain_eqs)
-                    if (!m_model->is_true(e))
-                        return expr_ref(nullptr, m);
-                
+                                
                 fmls.append(qb.domain_eqs);
                 eliminate_nested_vars(fmls, qb);
+                for (expr* e : fmls)
+                    if (!m_model->is_true(e))
+                        return expr_ref(nullptr, m);
                 mbp::project_plugin proj(m);
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;