mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5237

Browse source 
be stingier on stack instead of punting and saying users can set ulimit
This commit is contained in:
Nikolaj Bjorner 2021-05-02 16:18:55 -07:00
parent ff480d1183
commit 2c97799564
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/static_features.cpp
View file

@ -104,7 +104,7 @@ void static_features::reset() {
m_num_aliens_per_family .reset(); m_num_aliens_per_family .reset();
m_num_theories = 0; m_num_theories = 0;
m_theories .reset(); m_theories .reset();
m_max_stack_depth = 500; m_max_stack_depth = 100;
flush_cache(); flush_cache();
} }
@ -404,10 +404,11 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
m_num_sharing++; m_num_sharing++;
return; return;
} }
if (stack_depth > m_max_stack_depth) { if (stack_depth > m_max_stack_depth) {
for (expr* arg : subterms(expr_ref(e, m))) for (expr* arg : subterms(expr_ref(e, m)))
if (get_depth(arg) <= 3 || is_quantifier(arg)) if (get_depth(arg) <= 3 || is_quantifier(arg))
process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth-10); process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10);
return; return;
} }
mark(e); mark(e);