diff options
Diffstat (limited to 'test/regress/regress0/sygus/cggmp.sy')
| -rw-r--r-- | test/regress/regress0/sygus/cggmp.sy | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/test/regress/regress0/sygus/cggmp.sy b/test/regress/regress0/sygus/cggmp.sy deleted file mode 100644 index a3247e4f4..000000000 --- a/test/regress/regress0/sygus/cggmp.sy +++ /dev/null @@ -1,23 +0,0 @@ -; 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) |