diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 4ae66707d..ab21c4c88 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
 void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
     op_names.push_back(builtin_name("store",OP_STORE));
     op_names.push_back(builtin_name("select",OP_SELECT));
-    if (true || logic == symbol::null) {
+    if (logic == symbol::null || logic == symbol("HORN")) {
         // none of the SMT2 logics support these extensions
         op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
         op_names.push_back(builtin_name("map",OP_ARRAY_MAP));
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 219a4b45a..85371d8ef 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -454,8 +454,7 @@ public:
                     (*p)(model, vars, fmls);
                 }
             }
-            while (!vars.empty() && !fmls.empty()) {
-                std::cout << "mbp: " << var << "\n";
+            while (!vars.empty() && !fmls.empty()) {                
                 var = vars.back();
                 vars.pop_back();
                 project_plugin* p = get_plugin(var);
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 02c6d26cd..1bfd53597 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -158,6 +158,8 @@ namespace qe {
             return;
         }
         model_evaluator eval(*mdl);
+        eval.set_model_completion(true);
+        TRACE("qe", model_v2_pp(tout, *mdl););
 
         expr_ref val(m);
         for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
@@ -169,7 +171,7 @@ namespace qe {
             if (m.is_false(val)) {
                 m_asms.push_back(m.mk_not(p));
             }
-            else {
+            else {                
                 SASSERT(m.is_true(val));
                 m_asms.push_back(p);
             }
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index a5013cd5a..81635f906 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -475,18 +475,6 @@ lbool mus::get_mus(expr_ref_vector& mus) {
     return m_imp->get_mus(mus);
 }
 
-lbool mus::get_mus(ptr_vector<expr>& mus) {
-    return m_imp->get_mus(mus);
-}
-
-lbool mus::get_mus(expr_ref_vector& mus) {
-    ptr_vector<expr> result;
-    lbool r = m_imp->get_mus(result);
-    mus.append(result.size(), result.c_ptr());
-    return r;
-}
-
-
 void mus::reset() {
     m_imp->reset();
 }