diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 76b628dd3..22443ee1f 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -369,16 +369,14 @@ expr_ref func_interp::get_array_interp_core(func_decl * f) const {
     if (m_else == nullptr) 
         return r;
     ptr_vector<sort> domain;
-    for (sort* s : *f) {
-        domain.push_back(s);
-    }
+    for (sort* s : *f) 
+        domain.push_back(s);    
 
     bool ground = is_ground(m_else);
     for (func_entry * curr : m_entries) {
         ground &= is_ground(curr->get_result());
-        for (unsigned i = 0; i < m_arity; i++) {
-            ground &= is_ground(curr->get_arg(i));
-        }
+        for (unsigned i = 0; i < m_arity; i++) 
+            ground &= is_ground(curr->get_arg(i));        
     }
     if (!ground) {
         r = get_interp();
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 06ad4028d..f2861292f 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -224,7 +224,7 @@ struct model::top_sort : public ::top_sort<func_decl> {
     }
 };
 
-void model::compress() {
+void model::compress(bool force_inline) {
     if (m_cleaned) return;
 
     // stratify m_finterp and m_decls in a topological sort
@@ -238,7 +238,7 @@ void model::compress() {
         collect_deps(ts);
         ts.topological_sort();
         for (func_decl * f : ts.top_sorted()) {
-            cleanup_interp(ts, f);
+            cleanup_interp(ts, f, force_inline);
         }
 
         func_decl_set removed;
@@ -332,11 +332,11 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
    \brief Inline interpretations of skolem functions
 */
 
-void model::cleanup_interp(top_sort& ts, func_decl* f) {
+void model::cleanup_interp(top_sort& ts, func_decl* f, bool force_inline) {
     unsigned pid = ts.partition_id(f);
     expr * e1 = get_const_interp(f);
     if (e1) {
-        expr_ref e2 = cleanup_expr(ts, e1, pid);
+        expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
         if (e2 != e1) 
             register_decl(f, e2);
         return;
@@ -344,11 +344,11 @@ void model::cleanup_interp(top_sort& ts, func_decl* f) {
     func_interp* fi = get_func_interp(f);
     if (fi) {
         e1 = fi->get_else();
-        expr_ref e2 = cleanup_expr(ts, e1, pid);
+        expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
         if (e1 != e2) 
             fi->set_else(e2);
         for (auto& fe : *fi) {
-            e2 = cleanup_expr(ts, fe->get_result(), pid);
+            e2 = cleanup_expr(ts, fe->get_result(), pid, force_inline);
             if (e2 != fe->get_result()) {
                 fi->insert_entry(fe->get_args(), e2);
             }
@@ -382,21 +382,26 @@ void model::collect_occs(top_sort& ts, expr* e) {
     for_each_ast(collector, e, true);
 }
 
-bool model::can_inline_def(top_sort& ts, func_decl* f) {
+bool model::can_inline_def(top_sort& ts, func_decl* f, bool force_inline) {
     if (ts.occur_count(f) <= 1) return true;
     func_interp* fi = get_func_interp(f);
-    if (!fi) return false;
-    if (fi->get_else() == nullptr) return false;
-    if (m_inline) return true;
+    if (!fi) 
+        return false;
+    if (fi->get_else() == nullptr) 
+        return false;
+    if (m_inline) 
+        return true;
     expr* e = fi->get_else();
     obj_hashtable<expr> subs;
     ptr_buffer<expr> todo;
     todo.push_back(e);
     while (!todo.empty()) {
-        if (fi->num_entries() + subs.size() > 8) return false;
+        if (!force_inline && fi->num_entries() + subs.size() > 8) 
+            return false;
         expr* e = todo.back();
         todo.pop_back();
-        if (subs.contains(e)) continue;
+        if (subs.contains(e)) 
+            continue;
         subs.insert(e);
         if (is_app(e)) {
             for (expr* arg : *to_app(e)) {
@@ -411,7 +416,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) {
 }
 
 
-expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) {
+expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline) {
     if (!e) return expr_ref(nullptr, m);
 
     TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";);
@@ -455,7 +460,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             if (autil.is_as_array(a)) {
                 func_decl* f = autil.get_as_array_func_decl(a);
                 // only expand auxiliary definitions that occur once.
-                if (can_inline_def(ts, f)) {
+                if (can_inline_def(ts, f, force_inline)) {
                     fi = get_func_interp(f);
                     if (fi) {
                         new_t = fi->get_array_interp(f);
@@ -467,7 +472,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             if (new_t) {
                 // noop
             }
-            else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && 
+            else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) && 
                      fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
                 var_subst vs(m, false);
                 new_t = vs(fi->get_interp(), args.size(), args.data());
@@ -526,15 +531,15 @@ expr_ref model::unfold_as_array(expr* e) {
 }
 
 
-expr_ref model::get_inlined_const_interp(func_decl* f) {
+expr_ref model::get_inlined_const_interp(func_decl* f, bool force_inline) {
     expr* v = get_const_interp(f);
     if (!v) return expr_ref(nullptr, m);
     top_sort st(m);
     expr_ref result1(v, m);
-    expr_ref result2 = cleanup_expr(st, v, UINT_MAX);
+    expr_ref result2 = cleanup_expr(st, v, UINT_MAX, force_inline);
     while (result1 != result2) {
         result1 = result2;
-        result2 = cleanup_expr(st, result1, UINT_MAX);
+        result2 = cleanup_expr(st, result1, UINT_MAX, force_inline);
     }
     return result2;
 }
diff --git a/src/model/model.h b/src/model/model.h
index 8183c5a0e..822e4cff9 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -50,10 +50,10 @@ protected:
     void collect_deps(top_sort& ts);    
     void collect_occs(top_sort& ts, func_decl* f);
     void collect_occs(top_sort& ts, expr* e);
-    void cleanup_interp(top_sort& ts, func_decl * f);
-    expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition);
+    void cleanup_interp(top_sort& ts, func_decl * f, bool force_inline);
+    expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline);
     void remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s);
-    bool can_inline_def(top_sort& ts, func_decl* f);
+    bool can_inline_def(top_sort& ts, func_decl* f, bool force_inline);
     value_factory* get_factory(sort* s);
 
 public:
@@ -78,7 +78,7 @@ public:
     sort * get_uninterpreted_sort(unsigned idx) const override;
     bool has_uninterpreted_sort(sort * s) const;
 
-    expr_ref get_inlined_const_interp(func_decl* f);
+    expr_ref get_inlined_const_interp(func_decl* f, bool force_inline);
     expr_ref unfold_as_array(expr* e);
 
     //
@@ -90,7 +90,7 @@ public:
     //
     model * translate(ast_translation & translator) const;
 
-    void compress();
+    void compress(bool force_inline = false);
 
     void set_model_completion(bool f) { m_mev.set_model_completion(f); }
     void updt_params(params_ref const & p);