; 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)