1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/cggmp.sy b/test/regress/regress1/sygus/cggmp.sy
new file mode 100644
index 000000000..a3247e4f4
--- /dev/null
+++ b/test/regress/regress1/sygus/cggmp.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status
+
+(set-logic LIA)
+
+(synth-inv inv-f ((i Int) (j Int)))
+
+(declare-primed-var i Int)
+(declare-primed-var j Int)
+
+(define-fun pre-f ((i Int) (j Int)) Bool
+(and (= i 1)  
+(= j 10)))
+
+(define-fun trans-f ((i Int) (j Int) (i! Int) (j! Int)) Bool
+(and (and (>= j i) (= i! (+ i 2))) (= j! (- j 1))))
+
+(define-fun post-f ((i Int) (j Int)) Bool
+(not (and (< j i) (not (= j 6)))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)