blob: 9da07407a2b19df4432e82eeedb189877ba55dcc (
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
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2
(set-logic ALL)
(synth-fun f
() Bool
((B Bool))
(
(B Bool (true))
)
)
(synth-fun g
((r Int)) Bool
((B Bool) (I Int) (IConst Int))
(
(B Bool ((= I I) (=> B B)))
(I Int (r 0 (mod I IConst)))
(IConst Int ((Constant Int)))
)
)
(constraint (g 0))
(constraint (not (g 1)))
(constraint (g 2))
(constraint f)
(check-synth)
|
