; EXPECT: unsat
; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)

(synth-fun f ((x Int) (y Int)) Int
  (
    (Start Int
      (0 1 x y
        (+ Start Start)
        (- Start Start)
        (ite CBool Start Start)
        )
      )
    (CBool Bool
      (true false
        (and CBool CBool)
        (or CBool CBool)
        (not CBool)
        (<= Start Start)
        ; Having equality makes the problem easy to CEGIS
        ; (= Start Start)
        )
      )
    )
  )

(declare-var x Int)
(declare-var y Int)

(constraint (= (f 0 1) 0))
(constraint (= (f 1 y) y))
(constraint (= (f 2 1) 0))

(check-synth)