From 9e505edb66a0e2e073bff0283919458c51902f50 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 19 Jun 2026 10:07:46 -0700
Subject: [PATCH] add init-table for common sub-expressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/func_interp.cpp | 20 ++++++++++----------
 src/model/func_interp.h   |  2 ++
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index e42546f72..93d70af59 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -231,10 +231,8 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
         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, 1024, 
-            func_entry_hash(m_arity), func_entry_eq(m_arity));
-        for (func_entry* curr : m_entries) 
-            m_entry_table->insert(curr);   
+        init_table();
+ 
         ptr_vector<expr> null_args;
         null_args.resize(m_arity, nullptr);
         m_key = func_entry::mk(m(), m_arity, null_args.data(), nullptr);
@@ -243,6 +241,12 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
         m_entry_table->insert(new_entry);    
 }
 
+void func_interp::init_table() {
+    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);
+}
+
 void func_interp::del_entry(unsigned idx) {
     auto* e = m_entries[idx];
     if (m_entry_table) 
@@ -310,12 +314,8 @@ void func_interp::compress() {
         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);
-            }
+            if (m_entries.size() > 500) 
+                init_table();            
         }
     }
     // other compression, if else is a default branch.
diff --git a/src/model/func_interp.h b/src/model/func_interp.h
index e3935e05e..6d64f5168 100644
--- a/src/model/func_interp.h
+++ b/src/model/func_interp.h
@@ -104,6 +104,8 @@ class func_interp {
 
     void reset_interp_cache();
 
+    void init_table();
+
     expr * get_interp_core() const;
 
     expr_ref get_array_interp_core(func_decl * f) const;