Fix stale func_interp entry table after compression (#9906)

## Summary
Fix a use-after-free in `func_interp::compress()`.

When a function interpretation had previously grown large enough to
allocate `m_entry_table`, `compress()` could deallocate entries whose
result matched the else-case but leave the hash table intact. Later
`get_entry()` lookups could then return freed `func_entry*` values,
which showed up during model checking as a corrupted expression result
from `model_evaluator`.

## Root cause
`func_interp::compress()` compacted `m_entries` and freed removed
entries, but it did not rebuild or clear `m_entry_table`.

This left stale pointers in the lookup table whenever:
- the table had already been allocated on a larger interpretation, and
- compression removed some entries.

In the reported case, model evaluation rewrote `stack_s!1041` through
`BR_REWRITE1`, fetched a freed `func_entry` result from the stale table,
and then tripped an assertion in `expr::get_sort()` during quantifier
model checking.

## Fix
After compression removes entries, rebuild `m_entry_table` from the
surviving `m_entries`, or clear it when the surviving interpretation is
small.

## Regression coverage
Added a unit regression in `src/test/model_evaluator.cpp` that:
- creates a `func_interp` large enough to allocate `m_entry_table`,
- compresses away almost all entries,
- checks that removed keys no longer resolve, and
- checks that the surviving key still resolves to the correct result.

## Validation
- `../build/z3 ebso-115.smt2` previously hit an assertion in
`rewriter_def.h` / `ast.cpp`; after the fix it no longer asserts.
- `./test-z3 model_evaluator` passes with the new regression.

## Reproducer
I did not produce a smaller SMT2 benchmark in this change. The original
reproducer I used was `ebso-115.smt2`, and the new unit regression
directly exercises the stale-entry-table path in-process.

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>

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.

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());
+    }
     
 }