mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

fix #5980

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-19 11:10:20 +01:00
parent b7169e2a41
commit a180254c1a
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/recfun_decl_plugin.cpp
View file

@ -79,13 +79,15 @@ namespace recfun {
} }
// does `e` contain any `ite` construct? // 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) { bool def::contains_ite(util& u, expr * e) {
struct ite_find_p : public i_expr_pred { struct ite_find_p : public i_expr_pred {
ast_manager & m; ast_manager & m;
def& d; def& d;
util& u; util& u;
ite_find_p(ast_manager & m, def& d, util& u) : m(m), d(d), u(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. // ignore ites under quantifiers.
// this is redundant as the code // this is redundant as the code
@ -273,9 +275,9 @@ namespace recfun {
// explore arguments // explore arguments
for (expr * arg : *to_app(e)) { for (expr * arg : *to_app(e)) {
if (contains_ite(u, arg)) { if (contains_ite(u, arg)) {
for (expr * arg : *to_app(e))
if (contains_ite(u, arg))
stack.push_back(arg); stack.push_back(arg);
}
}
} }
} }
} }