mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

#7207

Browse source 
the utility that computes case analysis is brittle when the body of a function contains ite expressions that are not relevant to recursive unfolding.
The fold-rec occurrences that get inserted to harness large case splits work against throttling case generation: they get treated as recursive functions that have to be guarded.
This commit is contained in:
Nikolaj Bjorner 2024-06-16 15:04:42 -07:00
parent 972d35204c
commit 81ebd52f61
4 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/recfun_solver.cpp
View file

@ -271,7 +271,8 @@ namespace recfun {
SASSERT(!n || !n->is_attached_to(get_id()));
if (!n)
n = mk_enode(e, false);
SASSERT(!n->is_attached_to(get_id()));
if (n->is_attached_to(get_id()))
return true;
euf::theory_var w = mk_var(n);
ctx.attach_th_var(n, this, w);
if (u().is_defined(e) && u().has_defs())