From 88f1c68a94bd998854cb0bf3a1ce3f516cb774f8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Jan 2020 15:31:26 -0600
Subject: Fix backtracking issue in sygus fast enumerator (#3593)

---
 test/regress/CMakeLists.txt                        |  1 +
 test/regress/regress1/sygus/fast-enum-backtrack.sy | 32 ++++++++++++++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 test/regress/regress1/sygus/fast-enum-backtrack.sy

(limited to 'test/regress')

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)
+
-- 
cgit v1.2.3