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