blob: 91ba95d392619a11afd9620ef90c3ca543670807 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
; 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 (>= 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)
|
