test/regress/regress3/nia-max-square.sy

   1 ; EXPECT: unsat
   2 ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --nl-ext-tplanes
   3 (set-logic NIA)
   4
   5 (synth-fun max ((x Int) (y Int)) Int
   6   ((Start Int) (StartBool Bool))
   7   ((Start Int (0 1 x y
   8                (+ Start Start)
   9                (- Start Start)
  10                (* Start Start)
  11                (ite StartBool Start Start)))
  12    (StartBool Bool ((and StartBool StartBool)
  13                     (not StartBool)
  14                     (<= Start Start)))))
  15
  16 (declare-var x Int)
  17 (declare-var y Int)
  18
  19 (constraint (>= (max x y) (* x x)))
  20 (constraint (>= (max x y) (* y y)))
  21
  22 (check-synth)