4 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a7d931246..5eaaf3e67 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -968,6 +968,7 @@ set(regress_0_tests
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/issue3356-syg-inf-usort.smt2
   regress0/sygus/issue3624.sy
+  regress0/sygus/issue3645-grammar-sets.smt2
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy
@@ -1870,6 +1871,7 @@ set(regress_1_tests
   regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
+  regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
   regress1/sygus/strings-any-term1.sy
@@ -2017,6 +2019,7 @@ set(regress_2_tests
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
+  regress2/sygus/sets-fun-test.sy
   regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/sygus/vcb.sy
diff --git a/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2
new file mode 100644
index 000000000..22a5e07d4
--- /dev/null
+++ b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () (Set (_ BitVec 2)))
+(declare-fun b () (Set (_ BitVec 2)))
+(assert (= a b))
+(check-sat)
diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy
new file mode 100644
index 000000000..284325712
--- /dev/null
+++ b/test/regress/regress1/sygus/sets-pred-test.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun P ((x (Set Int))) Bool)
+
+(constraint (not (P (as emptyset (Set Int)))))
+(constraint (not (P (insert 1 2 (as emptyset (Set Int))))))
+(constraint (P (insert 0 (as emptyset (Set Int)))))
+(constraint (P (insert 0 4 5 (as emptyset (Set Int)))))
+(constraint (not (P (singleton 45))))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy
new file mode 100644
index 000000000..987d6a792
--- /dev/null
+++ b/test/regress/regress2/sygus/sets-fun-test.sy
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun f ((x Int)) (Set Int))
+
+(constraint (member 45 (f 45)))
+(constraint (member 8 (f 8)))
+(constraint (member 0 (f 3)))
+
+(check-synth)