; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes (set-logic NIA) (synth-fun max ((x Int) (y Int)) Int) (declare-var x Int) (declare-var y Int) (constraint (>= (max x y) (* x x))) (constraint (>= (max x y) (* y y))) (check-synth)