1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/fast-enum-backtrack.sy b/test/regress/regress1/sygus/fast-enum-backtrack.sy
new file mode 100644
index 000000000..73a3dc2e2
--- /dev/null
+++ b/test/regress/regress1/sygus/fast-enum-backtrack.sy
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-active-gen=enum
+
+(set-logic ALL)
+
+(declare-datatype Formula (
+  (P (Id Int))
+  (Op1 (op1 Int) (f Formula))
+  (Op2 (op2 Int) (f1 Formula) (f2 Formula))
+  )
+)
+
+(synth-fun phi () Formula
+  ((<F> Formula) (<O2> Int))
+  ((<F> Formula (
+     (P <O2>)
+     (Op1 <O2> <F>)
+     (Op2 <O2> <F> <F>)
+     )
+   )
+   (<O2> Int (0 1))
+   )
+)
+(define-fun holds ((f Formula)) Bool
+  (and ((_ is Op2) f) (= (op2 f) 1))
+)
+(define-fun holds2 ((f Formula)) Bool
+  (and ((_ is Op2) f) (= (op1 (f1 f)) 1))
+)
+(constraint (holds phi))
+(check-synth)
+