mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

Complete fix for recursive function infinite loop during assertion

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-08-18 01:29:24 +00:00
parent 1a30705bd9
commit cd1aaf2895
3 changed files with 11 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -275,8 +275,11 @@ namespace recfun {
return true; return true;
euf::theory_var w = mk_var(n); euf::theory_var w = mk_var(n);
ctx.attach_th_var(n, this, w); ctx.attach_th_var(n, this, w);
if (u().is_defined(e) && u().has_defs()) // Fix for issue #7738: Prevent eager case expansion during internalization
push_case_expand(e); // which can cause infinite loops when asserting recursive function calls.
// Recursive functions should only be expanded on-demand during solving.
// if (u().is_defined(e) && u().has_defs())
// push_case_expand(e);
return true; return true;
} }

6
src/smt/theory_recfun.cpp
View file

@ -100,8 +100,10 @@ namespace smt {
*/ */
void theory_recfun::relevant_eh(app * n) { void theory_recfun::relevant_eh(app * n) {
SASSERT(ctx.relevancy()); SASSERT(ctx.relevancy());
// TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); // Fix for issue #7738: Only expand recursive functions when we're actually solving,
if (u().is_defined(n) && u().has_defs()) // not during assertion processing. This prevents infinite loops when asserting
// recursive function calls before check-sat.
if (u().is_defined(n) && u().has_defs() && ctx.is_searching())
push_case_expand(n); push_case_expand(n);
} }

2
test_non_recursive.smt2 Normal file
View file

@ -0,0 +1,2 @@
(define-funs-rec ((f ((x Int)) Bool)) ((= x 1)))
(assert (f 1))