diff --git a/.gitignore b/.gitignore
index b73251f44..17465d9ae 100644
--- a/.gitignore
+++ b/.gitignore
@@ -82,6 +82,7 @@ src/api/js/build/
 src/api/js/**/*.__GENERATED__.*
 debug/*
 examples/python/z3
+examples/python/libz3.dll
 
 out/**
 *.bak
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 4530e9f93..cda05ee28 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -125,7 +125,11 @@ namespace q {
         }
         if (m.is_model_value(e))
             return expr_ref(m.mk_model_value(0, e->get_sort()), m);
-        return expr_ref(e, m);
+
+        expr_ref e1 = m_model->unfold_as_array(e);
+        if (e1 == e)
+            return e1;
+        return replace_model_value(e1);
     }
 
     expr_ref mbqi::choose_term(euf::enode* r) {
@@ -355,8 +359,8 @@ namespace q {
         for (app* v : vars) {
             expr_ref term(m);
             expr_ref val = (*m_model)(v);
-            val = m_model->unfold_as_array(val);
             term = replace_model_value(val);
+            TRACE("euf", tout << "replaced model value " << term << "\nfrom\n" << val << "\n");
             rep.insert(v, term);
             if (ctx.use_drat())
                 m_defs.push_back(mbp::def(expr_ref(v, m), term));
@@ -407,10 +411,13 @@ namespace q {
                 auto* n = nodes[i];
                 expr* e = n->get_expr();
                 expr* val = ctx.node2value(n);                
-                if (val && e->get_sort() == srt && !m.is_value(e) && !visited.is_marked(val)) {
+                if (val && e->get_sort() == srt && 
+                    !m.is_value(e) && 
+                    !visited.is_marked(val)) {
                     visited.mark(val);
+                    expr_ref value = replace_model_value(val);
                     veqs.push_back(m.mk_eq(v, e));
-                    meqs.push_back(m.mk_eq(v, val));
+                    meqs.push_back(m.mk_eq(v, value));
                     --bound;
                 }
             }
@@ -473,6 +480,7 @@ namespace q {
             expr_ref _term = subst(e, qb.vars);
             app_ref  term(to_app(_term), m);
             expr_ref value = (*m_model)(term);
+            value = replace_model_value(value);
             expr* s = m_model_fixer.invert_app(term, value);
             rep.insert(term, s);
             expr_ref eq(m.mk_eq(term, s), m);
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 37e2424ce..38f38ee0a 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -253,7 +253,7 @@ namespace q {
         euf::enode* r = nullptr;
         auto& v2r = ctx.values2root();
         TRACE("q",
-              tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
+              tout << "invert-app " << mk_pp(t, m) << " =\n" << mk_pp(value, m) << "\n";
               if (v2r.find(value, r)) 
                   tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
               /*ctx.display(tout); */
diff --git a/src/sat/smt/q_theory_checker.cpp b/src/sat/smt/q_theory_checker.cpp
index be246dd3c..9f31325b5 100644
--- a/src/sat/smt/q_theory_checker.cpp
+++ b/src/sat/smt/q_theory_checker.cpp
@@ -24,7 +24,7 @@ namespace q {
     expr_ref_vector theory_checker::clause(app* jst) {
         expr_ref_vector result(m);
         for (expr* arg : *jst) 
-            if (!is_bind(arg))
+            if (m.is_bool(arg))
                 result.push_back(mk_not(m, arg));
         return result;
     }