From 1a30705bd925023a086cb6b09e8d6d534a1d6534 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 18 Aug 2025 01:18:26 +0000
Subject: [PATCH] Identify root cause and implement targeted fix for recursive
 function hanging

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/theory_recfun.cpp     | 9 ++++-----
 test_definite_hang.smt2       | 2 ++
 test_issue_with_checksat.smt2 | 3 +++
 test_just_define.smt2         | 1 +
 test_simple_hang.smt2         | 2 ++
 5 files changed, 12 insertions(+), 5 deletions(-)
 create mode 100644 test_definite_hang.smt2
 create mode 100644 test_issue_with_checksat.smt2
 create mode 100644 test_just_define.smt2
 create mode 100644 test_simple_hang.smt2

diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 4247dcb2a..e4b37a45b 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -60,8 +60,8 @@ namespace smt {
             ctx.mk_enode(atom, false, true, true);
         if (!ctx.b_internalized(atom)) 
             ctx.set_var_theory(ctx.mk_bool_var(atom), get_id());
-        if (!ctx.relevancy() && u().is_defined(atom)) 
-            push_case_expand(atom);
+        // Removed eager case expansion - recursive functions should only be expanded
+        // when they become relevant during solving, not during assertion processing
         return true;
     }
 
@@ -77,9 +77,8 @@ namespace smt {
         if (!ctx.e_internalized(term)) {            
             ctx.mk_enode(term, false, false, true);
         }
-        if (!ctx.relevancy() && u().is_defined(term)) {
-            push_case_expand(term);
-        }
+        // Removed eager case expansion - recursive functions should only be expanded
+        // when they become relevant during solving, not during assertion processing
         return true; 
     }
 
diff --git a/test_definite_hang.smt2 b/test_definite_hang.smt2
new file mode 100644
index 000000000..8ffc6262c
--- /dev/null
+++ b/test_definite_hang.smt2
@@ -0,0 +1,2 @@
+(define-funs-rec ((loop ((x Int)) Int)) ((loop x)))
+(assert (= (loop 1) 0))
\ No newline at end of file
diff --git a/test_issue_with_checksat.smt2 b/test_issue_with_checksat.smt2
new file mode 100644
index 000000000..fc82f01ef
--- /dev/null
+++ b/test_issue_with_checksat.smt2
@@ -0,0 +1,3 @@
+(define-funs-rec ((g ((a Int) (b Int)) Bool)) ((or (= a b) (ite (> a b) (g (- a 1) b) (g a (- b 1))))))
+(assert (g 2 2))
+(check-sat)
\ No newline at end of file
diff --git a/test_just_define.smt2 b/test_just_define.smt2
new file mode 100644
index 000000000..5be6038c3
--- /dev/null
+++ b/test_just_define.smt2
@@ -0,0 +1 @@
+(define-funs-rec ((g ((a Int) (b Int)) Bool)) ((or (= a b) (ite (> a b) (g (- a 1) b) (g a (- b 1))))))
\ No newline at end of file
diff --git a/test_simple_hang.smt2 b/test_simple_hang.smt2
new file mode 100644
index 000000000..d7802b3d3
--- /dev/null
+++ b/test_simple_hang.smt2
@@ -0,0 +1,2 @@
+(define-funs-rec ((simple ((x Int)) Int)) ((ite (= x 0) 0 (simple (- x 1)))))
+(assert (= (simple 1) 0))
\ No newline at end of file