test/regress/regress1/sygus/issue3802-default-consts.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
(synth-fun f 
	() Bool
	((B Bool))
	(
		(B Bool ((Constant Bool)))
	)
)
(synth-fun g 
	((x0 Int) (r Int)) Bool 
	((B Bool) (I Int)) 
	(
		(B Bool ((= I I))) 
		(I Int (x0 r))
	)
)
(constraint (=> f (g 2 2)))
(constraint (not (=> f (g 0 1))))
(check-synth)