mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

expr_abstract: save 1 hashtable lookup per app argument

Browse source 
when we already know that the app is missing one arg to rewrite
This commit is contained in:
Nuno Lopes 2024-12-18 09:50:50 +00:00
parent 2f5c0a6985
commit c33bc2c8be
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/expr_abstract.cpp
View file

@ -58,7 +58,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
bool changed = false; bool changed = false;
m_args.reset(); m_args.reset();
for (unsigned i = 0, e = a->get_num_args(); i < e; ++i) { for (unsigned i = 0, e = a->get_num_args(); i < e; ++i) {
if (!m_map.find(a->get_arg(i), b)) { if (!all_visited || !m_map.find(a->get_arg(i), b)) {
m_stack.push_back(a->get_arg(i)); m_stack.push_back(a->get_arg(i));
all_visited = false; all_visited = false;
} }