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