blob: b04022766c518547a9a7cbd4ae3bb4bbfedeb0f6 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (z Int)))
(declare-primed-var x Int)
(declare-primed-var 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)
|
