diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 0c87f97a7..ca91cca1d 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -86,6 +86,7 @@ func_interp::~func_interp() {
     m().dec_ref(m_else);
     m().dec_ref(m_interp);
     m().dec_ref(m_array_interp);
+    dealloc(m_entry_table);
 }
 
 func_interp * func_interp::copy() const {
@@ -177,6 +178,13 @@ bool func_interp::is_constant() const {
    args_are_values to true if for all entries e e.args_are_values() is true.
 */
 func_entry * func_interp::get_entry(expr * const * args) const {
+    if (m_entry_table) {
+        func_entry key(m(), m_arity, args, m().mk_true()), * entry = nullptr;
+        if (m_entry_table->find(&key, entry))
+            return entry;
+        else
+            return nullptr;
+    }
     for (func_entry* curr : m_entries) {
         if (curr->eq_args(m(), m_arity, args))
             return curr;
@@ -214,10 +222,20 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
     if (!new_entry->args_are_values())
         m_args_are_values = false;
     m_entries.push_back(new_entry);
+    if (!m_entry_table && m_entries.size() > 500) {
+        m_entry_table = alloc(entry_table, 1000, 
+            func_entry_hash(m_arity), func_entry_eq(m_arity));
+        for (func_entry* curr : m_entries) 
+            m_entry_table->insert(curr);        
+    }
+    else if (m_entry_table) 
+        m_entry_table->insert(new_entry);    
 }
 
 void func_interp::del_entry(unsigned idx) {
     auto* e = m_entries[idx];
+    if (m_entry_table) 
+        m_entry_table->remove(e);    
     m_entries[idx] = m_entries.back();
     m_entries.pop_back();
     e->deallocate(m(), m_arity);
diff --git a/src/model/func_interp.h b/src/model/func_interp.h
index 2413d013a..3caa2eaaa 100644
--- a/src/model/func_interp.h
+++ b/src/model/func_interp.h
@@ -63,6 +63,30 @@ public:
     bool eq_args(ast_manager & m, unsigned arity, expr * const * args) const;
 };
 
+struct func_entry_eq {
+    unsigned m_arity;
+    func_entry_eq(unsigned arity) : m_arity(arity) {}
+    bool operator()(func_entry* a, func_entry* b) const {
+        for (unsigned i = 0; i < m_arity; ++i)
+            if (a->get_arg(i) != b->get_arg(i))
+                return false;        
+        return true;
+    }
+};
+
+struct func_entry_hash {
+    unsigned m_arity;
+    struct chasher {
+        unsigned operator()(func_entry* e, unsigned idx) const {
+            return e->get_arg(idx)->get_id();
+        }
+    };
+    func_entry_hash(unsigned arity) : m_arity(arity) {}
+    unsigned operator()(func_entry* e) const {
+        return get_composite_hash(e, m_arity, default_kind_hash_proc<func_entry*>(), chasher());
+    }
+};
+
 class func_interp {
     ast_manager &          m_manager;
     unsigned               m_arity;
@@ -74,6 +98,9 @@ class func_interp {
 
     expr *                 m_array_interp; // <! interp with lambda abstraction
 
+    using entry_table = ptr_hashtable<func_entry, func_entry_hash, func_entry_eq>;
+    entry_table* m_entry_table = nullptr;
+
     void reset_interp_cache();
 
     expr * get_interp_core() const;