blob: c3f43fc07cc7bf323bbf12ca96a564db24c273eb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; COMMAND-LINE: --sygus-out=status
;EXPECT: unsat
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
(declare-primed-var b Bool)
(declare-primed-var x Int)
(declare-primed-var y Int)
(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool
(and
(and (>= x 5) (<= x 9))
(and (>= y 1) (<= y 3))
)
)
(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool
(and
(and (= b! b) (= y! x))
(ite b (= x! (+ x 10)) (= x! (+ x 12)))
)
)
(define-fun post-f ((x Int) (y Int) (b Bool)) Bool true)
(inv-constraint inv-f pre-f trans-f post-f)
(check-synth)
|
