blob: a5eb41b260a5d0b66aada18527ad5eee45b513fc (
plain)
1
2
3
4
5
6
7
8
9
10
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9)))
(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1)))
(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0))
(inv-constraint inv-f pre-f trans-f post-f)
; invariant does not depend on arguments y and b
(check-synth)
|
