; EXPECT: (define-fun comm ((x Int) (y Int)) Int (+ x y))
; EXPECT: (define-fun comm ((x Int) (y Int)) Int (- x x))
; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
; EXIT: 1

; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification

(set-logic LIA)

(synth-fun comm ((x Int) (y Int)) Int
    ((Start Int (x
                 y
                 (+ Start Start)
                 (- Start Start)
                 ))
          ))

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

(constraint (= (comm x y) (comm y x)))

(check-synth)