mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 13:19:04 +00:00
Code Activity

initialize table with power of 2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-11 11:47:17 -07:00
parent 294f0578b0
commit 8440623f6d
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/func_interp.cpp
View file

@ -223,7 +223,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
m_args_are_values = false; m_args_are_values = false;
m_entries.push_back(new_entry); m_entries.push_back(new_entry);
if (!m_entry_table && m_entries.size() > 500) { if (!m_entry_table && m_entries.size() > 500) {
m_entry_table = alloc(entry_table, 1000, m_entry_table = alloc(entry_table, 1024,
func_entry_hash(m_arity), func_entry_eq(m_arity)); func_entry_hash(m_arity), func_entry_eq(m_arity));
for (func_entry* curr : m_entries) for (func_entry* curr : m_entries)
m_entry_table->insert(curr); m_entry_table->insert(curr);