diff options
Diffstat (limited to 'test/regress/regress1/sygus/cggmp.sy')
-rw-r--r-- | test/regress/regress1/sygus/cggmp.sy | 23 |
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) |