diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 513c39b10..e42546f72 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -307,6 +307,16 @@ void func_interp::compress() {
     if (j < m_entries.size()) {
         reset_interp_cache();
         m_entries.shrink(j);
+        if (m_entry_table) {
+            dealloc(m_entry_table);
+            m_entry_table = nullptr;
+            if (m_entries.size() > 500) {
+                m_entry_table = alloc(entry_table, 1024,
+                    func_entry_hash(m_arity), func_entry_eq(m_arity));
+                for (func_entry* curr : m_entries)
+                    m_entry_table->insert(curr);
+            }
+        }
     }
     // other compression, if else is a default branch.
     // or function encode identity.
diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index f4a64d4dc..77e13560b 100644
--- a/src/test/model_evaluator.cpp
+++ b/src/test/model_evaluator.cpp
@@ -1,5 +1,6 @@
 #include "model/model.h"
 #include "model/model_evaluator.h"
+#include "model/func_interp.h"
 #include "model/model_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/reg_decl_plugins.h"
@@ -65,5 +66,29 @@ void tst_model_evaluator() {
         eval(e, v);
         std::cout << e << " " << v << "\n";
     }
+
+    {
+        func_interp fi2(m, 1);
+        expr_ref zero(a.mk_int(0), m);
+        expr_ref one(a.mk_int(1), m);
+        fi2.set_else(zero);
+        for (unsigned i = 0; i < 600; ++i) {
+            expr_ref arg(a.mk_int(rational(i)), m);
+            expr* args[1] = { arg.get() };
+            fi2.insert_entry(args, i == 599 ? one.get() : zero.get());
+        }
+        fi2.compress();
+        SASSERT(fi2.num_entries() == 1);
+
+        expr_ref removed_arg(a.mk_int(0), m);
+        expr* removed_args[1] = { removed_arg.get() };
+        SASSERT(fi2.get_entry(removed_args) == nullptr);
+
+        expr_ref kept_arg(a.mk_int(599), m);
+        expr* kept_args[1] = { kept_arg.get() };
+        func_entry* kept = fi2.get_entry(kept_args);
+        SASSERT(kept != nullptr);
+        SASSERT(kept->get_result() == one.get());
+    }
     
 }