From 2c977995649777655dce98ac4035babf65bcb968 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 May 2021 16:18:55 -0700 Subject: [PATCH] #5237 be stingier on stack instead of punting and saying users can set ulimit --- src/ast/static_features.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 517aaaef7..227082e6f 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -104,7 +104,7 @@ void static_features::reset() { m_num_aliens_per_family .reset(); m_num_theories = 0; m_theories .reset(); - m_max_stack_depth = 500; + m_max_stack_depth = 100; flush_cache(); } @@ -404,10 +404,11 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite m_num_sharing++; return; } + if (stack_depth > m_max_stack_depth) { for (expr* arg : subterms(expr_ref(e, m))) 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; } mark(e);