diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 56c1d65cd..b96638944 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -135,7 +135,7 @@ if (MSVC AND Z3_BUILD_LIBZ3_MSVC_STATIC)
         set(${CompilerFlag} "${${CompilerFlag}}" CACHE STRING "msvc compiler flags" FORCE)
         message("MSVC flags: ${CompilerFlag}:${${CompilerFlag}}")
     endforeach()
-endif(MSVC)
+endif()
 add_library(libz3 ${lib_type} ${object_files})
 target_include_directories(libz3 INTERFACE
   $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/api>
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index ffcb95587..8730a2c2e 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -132,6 +132,8 @@ namespace sat {
             return false;
         }
         virtual bool is_pb() { return false; }
+
+        virtual std::string reason_unknown() { return "unknown"; }
     };
 
 };
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5222201c9..59503fb00 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1357,7 +1357,6 @@ namespace sat {
             return is_sat;
         }
         catch (const abort_solver &) {
-            m_reason_unknown = "sat.giveup";
             IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort giveup\")\n";);
             return l_undef;
         }
@@ -1778,6 +1777,7 @@ namespace sat {
             case check_result::CR_CONTINUE:
                 break;
             case check_result::CR_GIVEUP:
+                m_reason_unknown = m_ext->reason_unknown();                
                 throw abort_solver();
             }
             return l_undef;
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 883773988..87e159b87 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -686,7 +686,6 @@ namespace arith {
         if (m_nla)
             m_nla->push();
         th_euf_solver::push_core();
-
     }
 
     void solver::pop_core(unsigned num_scopes) {
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index bd01f52da..4df4f3a50 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -122,7 +122,7 @@ namespace array {
             ctx.push(push_back_vector(m_minmaxdiffs));
             break;
         case OP_ARRAY_DEFAULT:
-            add_parent_default(find(n->get_arg(0)), n);
+            add_parent_default(find(n->get_arg(0)));
             break;
         case OP_ARRAY_MAP:
         case OP_SET_UNION:
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 8b56ff3ae..aa986d87f 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -69,14 +69,21 @@ namespace array {
             values.set(n->get_expr_id(), n->get_expr());
             return;
         }
-            
+        theory_var v = get_th_var(n);
+        euf::enode* d = get_default(v);
+
+        if (a.is_const(n->get_expr())) {
+            expr* val = values.get(d->get_root_id());
+            SASSERT(val);
+            values.set(n->get_expr_id(), a.mk_const_array(n->get_sort(), val));
+            return;
+        }
+        
         unsigned arity = get_array_arity(srt);
         func_decl * f    = mk_aux_decl_for_array_sort(m, srt);
         func_interp * fi = alloc(func_interp, m, arity);
         mdl.register_decl(f, fi);
 
-        theory_var v = get_th_var(n);
-        euf::enode* d = get_default(v);
         if (d && !fi->get_else())
             fi->set_else(values.get(d->get_root_id()));
 
diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index 2481e337a..1c4b95abe 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -172,6 +172,10 @@ namespace array {
             add_parent_select(v1, select);
         if (is_lambda(e1) || is_lambda(e2))
             push_axiom(congruence_axiom(n1, n2));
+        if (d1.m_has_default && !d2.m_has_default)
+            add_parent_default(v2);
+        if (!d1.m_has_default && d2.m_has_default)
+            add_parent_default(v1);
     }
 
     void solver::add_parent_select(theory_var v_child, euf::enode* select) {
@@ -206,9 +210,10 @@ namespace array {
             propagate_select_axioms(d, lambda);
     }
 
-    void solver::add_parent_default(theory_var v, euf::enode* def) {
-        SASSERT(a.is_default(def->get_expr()));
+    void solver::add_parent_default(theory_var v) {
         auto& d = get_var_data(find(v));
+        ctx.push(value_trail(d.m_has_default));
+        d.m_has_default = true;
         for (euf::enode* lambda : d.m_lambdas)
             push_axiom(default_axiom(lambda));
         if (should_prop_upward(d))
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index fbff2afb6..5c2708842 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -50,7 +50,8 @@ namespace array {
         // void log_drat(array_justification const& c);
 
         struct var_data {
-            bool                m_prop_upward{ false };            
+            bool                m_prop_upward = false ;
+            bool                m_has_default = false;
             euf::enode_vector   m_lambdas;             // equivalent nodes that have beta reduction properties
             euf::enode_vector   m_parent_lambdas;      // parents that have beta reduction properties
             euf::enode_vector   m_parent_selects;      // parents that use array in select position
@@ -202,7 +203,7 @@ namespace array {
 
         // solving          
         void add_parent_select(theory_var v_child, euf::enode* select);
-        void add_parent_default(theory_var v_child, euf::enode* def);
+        void add_parent_default(theory_var v_child);
         void add_lambda(theory_var v, euf::enode* lambda);        
         void add_parent_lambda(theory_var v_child, euf::enode* lambda);
 
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 4b7745dd7..c22c46322 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -296,7 +296,17 @@ namespace euf {
             expr_ref sval(m);
             th_rewriter rw(m);
             rw(val, sval);
-            out << bpp(r) << " := " << sval << " " << mdl(r->get_root()->get_expr()) << "\n";
+            expr_ref mval = mdl(r->get_root()->get_expr());
+            if (mval != sval) {
+                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << mval << "\n";
+                continue;
+            }
+            if (!m.is_bool(val))
+                continue;
+            auto bval = s().value(r->bool_var());
+            bool tt = l_true == bval;
+            if (tt != m.is_true(sval))
+                out << bpp(r) << " :=\neval:  " << sval << "\nmval:  " << bval << "\n";
         }
         for (euf::enode* r : nodes)
             r->unmark1();
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 806509e4a..c30fdbf89 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -166,8 +166,9 @@ namespace euf {
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
-    void solver::init_search() {
+    void solver::init_search() {        
         TRACE("before_search", s().display(tout););
+        m_reason_unknown.clear();
         for (auto* s : m_solvers)
             s->init_search();
     }
@@ -482,7 +483,7 @@ namespace euf {
         auto apply_solver = [&](th_solver* e) {
             switch (e->check()) {
             case sat::check_result::CR_CONTINUE: cont = true; break;
-            case sat::check_result::CR_GIVEUP: give_up = true; break;
+            case sat::check_result::CR_GIVEUP: m_reason_unknown = "incomplete theory " + e->name().str(); TRACE("euf", tout << "give up " << e->name() << "\n"); give_up = true; break;
             default: break;
             }
         };
@@ -490,8 +491,10 @@ namespace euf {
             cont = true;
         for (unsigned i = 0; i < m_solvers.size(); ++i) {
             auto* e = m_solvers[i];
-            if (!m.inc())
+            if (!m.inc()) {
+                m_reason_unknown = "canceled";
                 return sat::check_result::CR_GIVEUP;
+            }
             if (e == m_qsolver)
                 continue;
             apply_solver(e);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 089c896cb..d19e0acac 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -105,6 +105,7 @@ namespace euf {
         user_solver::solver*          m_user_propagator = nullptr;
         th_solver*             m_qsolver = nullptr;
         unsigned               m_generation = 0;
+        std::string            m_reason_unknown; 
         mutable ptr_vector<expr> m_todo;
 
         ptr_vector<expr>                                m_bool_var2expr;
@@ -290,6 +291,7 @@ namespace euf {
         bool should_research(sat::literal_vector const& core) override;
         void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override;
+        std::string reason_unknown() override { return m_reason_unknown; }
 
         void propagate(literal lit, ext_justification_idx idx);
         bool propagate(enode* a, enode* b, ext_justification_idx idx);
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index f2caa2a3e..a87be2dee 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -198,6 +198,7 @@ namespace q {
         expr_ref_vector eqs(m);
         add_domain_bounds(mdl, qb);
         auto proj = solver_project(mdl, qb, eqs, false);
+        CTRACE("q", !proj, tout << "could not project " << qb.mbody << " " << eqs << "\n" << mdl);
         if (!proj)
             return false;
         add_instantiation(q, proj);
@@ -339,8 +340,10 @@ namespace q {
                 fmls.append(qb.domain_eqs);
                 eliminate_nested_vars(fmls, qb);
                 for (expr* e : fmls)
-                    if (!m_model->is_true(e))
+                    if (!m_model->is_true(e)) {
+                        TRACE("q", tout << "not true: " << mk_pp(e, m) << " := " << (*m_model)(e) << "\n");
                         return expr_ref(nullptr, m);
+                    }
                 mbp::project_plugin proj(m);
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;
@@ -348,8 +351,9 @@ namespace q {
             if (!p)
                 continue; 
             if (ctx.use_drat()) {
-                if (!p->project(*m_model, vars, fmls, m_defs))
-                    return expr_ref(m);                
+                if (!p->project(*m_model, vars, fmls, m_defs)) 
+                    return expr_ref(m);
+                    
             }
             else if (!(*p)(*m_model, vars, fmls))
                 return expr_ref(m);
@@ -430,8 +434,11 @@ namespace q {
     void mbqi::add_domain_bounds(model& mdl, q_body& qb) {
         qb.domain_eqs.reset();
         m_model->reset_eval_cache();
-        for (app* v : qb.vars)
-            m_model->register_decl(v->get_decl(), mdl(v));
+        {
+            model::scoped_model_completion _sc(mdl, true);
+            for (app* v : qb.vars)
+                m_model->register_decl(v->get_decl(), mdl(v));
+        }
         ctx.model_updated(m_model);
         if (qb.var_args.empty())
             return;
@@ -440,7 +447,8 @@ namespace q {
             expr_ref _term = subst(t, qb.vars);
             app_ref  term(to_app(_term), m);
             expr_ref value = (*m_model)(term->get_arg(idx));
-            m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs);
+            if (m.is_value(value))
+                m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs);
         }
     }
 
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 892a88f89..562fa431e 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -74,6 +74,8 @@ class sat_tactic : public tactic {
             TRACE("sat", tout << "result of checking: " << r << " "; 
                   if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";
                   if (m_goal2sat.has_interpreted_funs()) tout << "has interpreted\n";);
+            if (r == l_undef)
+                g->set_reason_unknown(m_solver->get_reason_unknown());
             if (r == l_false) {
                 expr_dependency * lcore = nullptr;
                 if (produce_core) {
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 389ee124b..81d21f959 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -164,6 +164,7 @@ public:
                     in->assert_expr(local_solver->get_assertion(i));
                 }
             }
+            in->set_reason_unknown(local_solver->reason_unknown());
             result.push_back(in.get());
             break;
         }
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index f32e4a66b..5e7e0b2fe 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -55,6 +55,7 @@ protected:
     proof_converter_ref   m_pc;
     dependency_converter_ref m_dc;
     unsigned              m_ref_count;
+    std::string           m_reason_unknown;
     expr_array            m_forms;
     expr_array            m_proofs;
     expr_dependency_array m_dependencies;
@@ -159,6 +160,8 @@ public:
     void set(model_converter* m) { m_mc = m; }
     void set(proof_converter* p) { m_pc = p; }
 
+    void set_reason_unknown(std::string const& reason_unknown) { m_reason_unknown = reason_unknown; }
+    std::string const& get_reason_unknown() { return m_reason_unknown; }
     bool is_cnf() const;
 
     goal * translate(ast_translation & translator) const;
@@ -176,6 +179,8 @@ template<typename GoalCollection>
 inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_sat(); }
 template<typename GoalCollection>
 inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); }
+template<typename GoalCollection>
+inline std::string get_reason_unknown(GoalCollection const & c) { return c.size() == 1 ? c[0]->get_reason_unknown() : std::string("unknown"); }
 
 template<typename ForEachProc>
 void for_each_expr_at(ForEachProc& proc, goal const & s) {
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index cc0ab8f5e..b1609ed85 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -184,8 +184,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
     if (r.size() > 0) {
         pr = r[0]->pr(0);
         CTRACE("tactic", pr, tout << pr << "\n";);
-    }
-    
+    }    
 
     if (is_decided_sat(r)) {
         model_converter_ref mc = r[0]->mc();            
@@ -217,7 +216,9 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
             if (mc)
                 (*mc)(labels);
         }
-        reason_unknown = "incomplete";
+        reason_unknown = get_reason_unknown(r);
+        if (reason_unknown.empty())
+            reason_unknown = "unknown";
         return l_undef;
     }
 }