From 48058e706f73304ac0c7b8a47e7eca092d9c05b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jan 2021 02:21:42 -0800 Subject: [PATCH] fix #4951 Signed-off-by: Nikolaj Bjorner --- src/ast/static_features.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index defabe07b..dd363eb33 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/static_features.h" #include "ast/ast_pp.h" +#include "ast/for_each_expr.h" static_features::static_features(ast_manager & m): m(m), @@ -301,7 +302,6 @@ void static_features::update_core(expr * e) { m_num_interpreted_constants++; } if (fid == m_afid) { - // std::cout << mk_pp(e, m) << "\n"; switch (to_app(e)->get_decl_kind()) { case OP_MUL: if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) { @@ -405,12 +405,14 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite 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); return; } mark(e); update_core(e); - if (is_quantifier(e)) { expr * body = to_quantifier(e)->get_expr(); process(body, false, false, false, stack_depth+1); @@ -444,11 +446,8 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite unsigned or_and_depth = 0; unsigned ite_depth = 0; - unsigned num_args = to_app(e)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = to_app(e)->get_arg(i); - if (m.is_not(arg)) - arg = to_app(arg)->get_arg(0); + for (expr* arg : *to_app(e)) { + m.is_not(arg, arg); process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new, stack_depth+1); depth = std::max(depth, get_depth(arg)); if (form_ctx_new)