plus [] is accepted, but z3 does not understand it

[jwaldmann]

When I have plus [] in my formula,

• smtlib's output is wrong (does not conform to SMTLIB grammar): it will output + (at least that's what I see with the debug back-end). I was expecting (+) (with parens)
• and even with the parens it'd be wrong: Z3 rejects it, while I was expecting that this denotes 0.

anyway, I suggest smtlib2

• either rejects plus []
• or rewrites to 0 (if this can be done in a type-safe way)

[jwaldmann]

and when CVC4 sees one-argument plus (+ 1) it says

(error "Parse Error: <stdin>:3.26: Expecting at least 2 arguments for operator 'PLUS', found 1")