From 758c3b2c3ba02d8c6fb0d26180018fb9007549e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Dec 2022 07:53:53 -0800 Subject: [PATCH] fix filtering for recursive functions --- src/ast/simplifiers/dependent_expr_state.cpp | 18 +++++++++++++----- src/ast/simplifiers/dependent_expr_state.h | 2 +- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.cpp b/src/ast/simplifiers/dependent_expr_state.cpp index 40528fe99..8e9ecf190 100644 --- a/src/ast/simplifiers/dependent_expr_state.cpp +++ b/src/ast/simplifiers/dependent_expr_state.cpp @@ -65,14 +65,22 @@ void dependent_expr_state::freeze_terms(expr* e, bool only_as_array, ast_mark& v */ void dependent_expr_state::freeze_recfun() { - if (m_recfun_frozen) - return; - m_recfun_frozen = true; auto& m = m_frozen_trail.get_manager(); recfun::util rec(m); + if (!rec.has_rec_defs()) + return; + unsigned sz = rec.get_rec_funs().size(); + if (m_num_recfun >= sz) + return; + ast_mark visited; - for (func_decl* f : rec.get_rec_funs()) - freeze_terms(rec.get_def(f).get_rhs(), false, visited); + for (func_decl* f : rec.get_rec_funs()) { + auto& d = rec.get_def(f); + if (!d.is_macro()) + freeze_terms(d.get_rhs(), false, visited); + } + m_trail.push(value_trail(m_num_recfun)); + m_num_recfun = sz; } /** diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 9f27a336c..d7aa1d6eb 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -43,7 +43,7 @@ Author: class dependent_expr_state { unsigned m_qhead = 0; bool m_suffix_frozen = false; - bool m_recfun_frozen = false; + unsigned m_num_recfun = 0; lbool m_has_quantifiers = l_undef; ast_mark m_frozen; func_decl_ref_vector m_frozen_trail;