blob: 29e8527dce5688bba60c7b3014886bea4086cc94 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const
(set-logic LIA)
(synth-inv inv-f ((y Int) (z Int) (c Int)))
(declare-primed-var y Int)
(declare-primed-var z Int)
(declare-primed-var c Int)
(define-fun pre-f ((y Int) (z Int) (c Int)) Bool
(and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y)))))
(define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool
(and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y)))
(define-fun post-f ((y Int) (z Int) (c Int)) Bool
(not (and (< c 36) (or (< z 0) (>= z 4608)))))
(inv-constraint inv-f pre-f trans-f post-f)
; needs --sygus-repair-const, since easy solution involves the constant 4608
(check-synth)
|
