Fix backtracking issue in sygus fast enumerator (#3593)

2 files changed, 33 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 22848ff97..f8608a34d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1751,6 +1751,7 @@ set(regress_1_tests
   regress1/sygus/dup-op.sy
   regress1/sygus/error1-dt.sy
   regress1/sygus/extract.sy
+  regress1/sygus/fast-enum-backtrack.sy
   regress1/sygus/fg_polynomial3.sy
   regress1/sygus/find_sc_bvult_bvnot.sy
   regress1/sygus/hd-01-d1-prog.sy
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)
+