1 2 3 4 5 6 7 8 9 10 11 12 13 14
; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status (set-logic LIA) (synth-fun f () Bool) (synth-fun g () Bool) (synth-fun h () Bool) (synth-fun w () Int) (constraint (not (= w 0))) (constraint f) (constraint (not g)) (constraint h) (check-synth)