blob: a3247e4f4bcc7b053aea6dfce4c25b2104391d4a (
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=pre --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((i Int) (j Int)))
(declare-primed-var i Int)
(declare-primed-var j Int)
(define-fun pre-f ((i Int) (j Int)) Bool
(and (= i 1)
(= j 10)))
(define-fun trans-f ((i Int) (j Int) (i! Int) (j! Int)) Bool
(and (and (>= j i) (= i! (+ i 2))) (= j! (- j 1))))
(define-fun post-f ((i Int) (j Int)) Bool
(not (and (< j i) (not (= j 6)))))
(inv-constraint inv-f pre-f trans-f post-f)
(check-synth)
|
