1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/issue3580.sy b/test/regress/regress1/sygus/issue3580.sy
new file mode 100644
index 000000000..9da07407a
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3580.sy
@@ -0,0 +1,24 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2
+(set-logic ALL)
+(synth-fun f 
+	() Bool 
+	((B Bool)) 
+	(
+		(B Bool (true))
+	)
+)
+(synth-fun g 
+	((r Int)) Bool 
+	((B Bool) (I Int) (IConst Int)) 
+	(
+		(B Bool ((= I I) (=> B B)))
+		(I Int (r 0 (mod I IConst)))
+		(IConst Int ((Constant Int)))
+	)
+) 
+(constraint (g 0))
+(constraint (not (g 1)))
+(constraint (g 2))
+(constraint f)
+(check-synth)