From 830ede6623a229df7455de8430e9160f689781f4 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 18 Aug 2025 01:00:03 +0000
Subject: [PATCH] Initial exploration of recursive function hanging issue

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 test_infinite.smt2      | 2 ++
 test_issue.smt2         | 2 ++
 test_recfun_simple.smt2 | 2 ++
 3 files changed, 6 insertions(+)
 create mode 100644 test_infinite.smt2
 create mode 100644 test_issue.smt2
 create mode 100644 test_recfun_simple.smt2

diff --git a/test_infinite.smt2 b/test_infinite.smt2
new file mode 100644
index 000000000..ab8f332d4
--- /dev/null
+++ b/test_infinite.smt2
@@ -0,0 +1,2 @@
+(define-funs-rec ((g ((a Int) (b Int)) Bool)) ((g a b)))
+(assert (g 2 2))
\ No newline at end of file
diff --git a/test_issue.smt2 b/test_issue.smt2
new file mode 100644
index 000000000..af10605f8
--- /dev/null
+++ b/test_issue.smt2
@@ -0,0 +1,2 @@
+(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))
diff --git a/test_recfun_simple.smt2 b/test_recfun_simple.smt2
new file mode 100644
index 000000000..8814a3f4f
--- /dev/null
+++ b/test_recfun_simple.smt2
@@ -0,0 +1,2 @@
+(define-funs-rec ((f ((x Int)) Int)) ((ite (= x 0) 0 (+ 1 (f (- x 1))))))
+(assert (= (f 2) 2))
\ No newline at end of file