blob: ed4689fe9e2d0a918613c4fc6c29dbf3e30076b7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 --sygus-grammar-cons=any-const
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int)) )
(define-fun pre-f ((x Int) (y Int)) Bool
(and
(= x 0)
(= y 100)
)
)
(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool
(and
(< x 100)
(= x! (+ x 1))
(= y! (+ y 1))
)
)
(define-fun post-f ((x Int) (y Int)) Bool
(=> (>= x 100) (>= y 200))
)
(inv-constraint inv-f pre-f trans-f post-f)
(check-synth)
|
