From a180254c1a7b220d77175557c5d832a5063c4e65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Apr 2022 11:10:20 +0100 Subject: [PATCH] fix #5980 --- src/ast/recfun_decl_plugin.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 0e9c27655..9dd82bc1a 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -79,13 +79,15 @@ namespace recfun { } // does `e` contain any `ite` construct? + // subject to the then/else branch using a recursive call, + // but the guard does not. bool def::contains_ite(util& u, expr * e) { struct ite_find_p : public i_expr_pred { ast_manager & m; def& d; util& u; ite_find_p(ast_manager & m, def& d, util& u) : m(m), d(d), u(u) {} - bool operator()(expr * e) override { return m.is_ite(e) && d.contains_def(u, e); } + bool operator()(expr * e) override { return m.is_ite(e) && !d.contains_def(u, to_app(e)->get_arg(0)) && d.contains_def(u, e); } }; // ignore ites under quantifiers. // this is redundant as the code @@ -273,9 +275,9 @@ namespace recfun { // explore arguments for (expr * arg : *to_app(e)) { if (contains_ite(u, arg)) { + for (expr * arg : *to_app(e)) + if (contains_ite(u, arg)) stack.push_back(arg); - } - } } } }