blob: 55f4723ec674daa0bdf23cfa855919555de96b9c (
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-out=status
(set-logic NIA)
(synth-fun patternGen ((i Int)) Int
((ITE Int) (CONST Int) (I Int) (B Bool))
( (ITE Int (
(ite (<= i CONST) I I)
))
(CONST Int (0))
(I Int (i 1
(+ I I) (- I I) (* I I)
))
(B Bool (
(<= I I)
))
)
)
(declare-var i Int)
(constraint (= (patternGen 0) 1))
(constraint (= (patternGen 1) 1))
(constraint (= (patternGen 2) 1))
(check-synth)
|
