blob: f8a3136f20d962f699fc90bc846ec6b1a497ca79 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (z Int)))
(define-fun pre-f ((x Int) (z Int)) Bool
(and (> x (- 0 100)) (< x 200)
(> z 100) (< z 200)))
(define-fun trans-f ((x Int) (z Int) (x! Int) (z! Int)) Bool
(and (< x 100) (> z 100)
(or (and (= x! (+ x 1)) (= z! z))
(and (= x! (- x 1)) (= z! (- z 1))))))
(define-fun post-f ((x Int) (z Int)) Bool
(or (and (< x 100) (> z 100))
(or (>= x 100) (<= z 100))))
(inv-constraint inv-f pre-f trans-f post-f)
(check-synth)
|