[SMT-COMP] Incremental QF_BV, addition with >2 operands

[Trevor Hansen]

In the incremental QF_BV benchmarks, The
/20170501-Heizmann-UltimateAutomizer/jain_5_true-unreach-call_true-no-overflow.i.smt2
benchmark has additions with >2 operands.

For example:

(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(declare-fun c_main_~x~4 () (_ BitVec 32))
(declare-fun c_main_~y~4 () (_ BitVec 32))
(assert
(distinct
(bvadd
  c_main_~y~4
  c_main_~x~4
  (_ bv4294967266 32)
)
(_ bv0 32)
)
)
(check-sat)

This example is parsed and solved by z3, mathsat, boolector, yices2, and
cvc4. So addition with >2 operands has wide support.

The solvers I'm involved with don't parse it. Although it's easy for me to
change that.

Am I confused, are >2 operands allowed?
Even if they are currently not allowed, is the use so widespread they
should be allowed?

Thanks,
Trev.