blob: 27378d9ca0e90dd70329a3344cadbe17aba40d76 (
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: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun args_0_refinement_0
((r Int)) Bool
((fv_B Bool))
(
(fv_B Bool (true))
)
)
(synth-fun ret_refinement_0
((x0 Int) (r Bool)) Bool
((fv_B Bool) (B Bool) (I Int))
(
(fv_B Bool (r true (=> B fv_B)))
(B Bool ((Variable Bool) (= I I)))
(I Int ((Variable Int) 1))
)
)
(constraint (ret_refinement_0 1 true))
(constraint (not (ret_refinement_0 1 false)))
(constraint (and (ret_refinement_0 0 false)))
(check-synth)
|
