1 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy
new file mode 100644
index 000000000..6e2ce3a2c
--- /dev/null
+++ b/test/regress/regress1/sygus/three.sy
@@ -0,0 +1,30 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth 
+
+(set-logic LIA)
+
+(synth-fun f ((x Int)) Int
+    ((Start Int (
+                 x
+                 3
+                 7
+                 10
+                 (* Start Start)
+                 (mod Start Start)))))
+
+(declare-var x Int)
+
+(constraint (= (f x) (f (+ x 10))))
+(constraint (= (f 1) 3))
+(constraint (= (f 2) 6))
+(constraint (= (f 3) 9))
+(constraint (= (f 4) 2))
+(constraint (= (f 5) 5))
+(constraint (= (f 6) 8))
+(constraint (= (f 7) 1))
+(constraint (= (f 8) 4))
+(constraint (= (f 9) 7))
+(constraint (= (f 0) 0))
+
+(check-synth)
+