; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
; EXPECT: unsat
(set-logic LIA)

(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)

(synth-fun g ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)

(declare-var x1 Int)
(declare-var x2 Int)
(declare-var x3 Int)
(declare-var x4 Int)
(declare-var x5 Int)
(declare-var x6 Int)
(declare-var x7 Int)
(declare-var x8 Int)
(declare-var x9 Int)
(declare-var x10 Int)

; should be able to determine that arguments 1...6, 8...10 are irrelevant for f
; and arguments 1...3, 5...10 are irrelevant for g

(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7)))

(constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4)))

(check-synth)