Fix bugs related to sygus higher-order + recursive functions (#3448)

2 files changed, 27 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c98dd1be2..aa5329e2f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1718,6 +1718,7 @@ set(regress_1_tests
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
+  regress1/sygus/list_recursor.sy
   regress1/sygus/logiccell_help.sy
   regress1/sygus/max.sy
   regress1/sygus/max2-bv.sy
diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy
new file mode 100644
index 000000000..53c55397e
--- /dev/null
+++ b/test/regress/regress1/sygus/list_recursor.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho
+
+(set-logic ALL)
+
+(declare-datatype List ((cons (head Int) (tail List)) (nil)))
+
+(define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int
+  (ite ((_ is nil) l) x 
+                      (y (head l) (tail l) (List_rec x y (tail l)))))
+
+(synth-fun f () Int
+  ((I Int))
+  ((I Int  (0 1 (+ I I)))))
+   
+(synth-fun g ((x Int) (y List) (z Int)) Int
+  ((I Int) (L List))
+  ((I Int  (x z (+ I I) (head L) 0 1))
+   (L List (y (tail y)))))
+   
+
+(constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2))
+(constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2))
+(constraint (= (List_rec f g (cons 5 (cons 3 (cons 3 (cons 0 nil))))) 4))
+(constraint (= (List_rec f g nil) 0))
+(check-synth)