diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 396f93973..7975a4d61 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -127,7 +127,6 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const *
         return nullptr;
     }
     if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) {
-        SASSERT(false);
         m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument");
         return nullptr;
     }
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 1ae0c9593..e0342ad72 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -180,11 +180,6 @@ public:
         parameter param(s);
         return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v);
     }
-    app * mk_const_array(unsigned n, sort * const* s, expr * v) {
-        vector<parameter> ps;
-        for (unsigned i = 0; i < n; ++i) ps.push_back(parameter(s[i]));
-        return m_manager.mk_app(m_fid, OP_CONST_ARRAY, n, ps.c_ptr(), 1, &v);
-    }
     app * mk_empty_set(sort * s) {
         return mk_const_array(s, m_manager.mk_false());
     }
diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp
index e6980583a..8819eb584 100644
--- a/src/cmd_context/eval_cmd.cpp
+++ b/src/cmd_context/eval_cmd.cpp
@@ -71,7 +71,7 @@ public:
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
         unsigned rlimit  = m_params.get_uint("rlimit", 0);
-        md->compress();
+        // md->compress();
         model_evaluator ev(*(md.get()), m_params);
         ev.set_solver(alloc(th_solver, ctx));
         cancel_eh<reslimit> eh(ctx.m().limit());