blob: ff68bc06c219554e5f5b31a05c943df0b8e537f5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
(declare-primed-var x Int)
(declare-primed-var y Int)
(declare-primed-var b Bool)
(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 (<= y x))
(inv-constraint inv-f pre-f trans-f post-f)
(check-synth)
|
