MathSAT crashes because we use bvadd with three parameters

[Heizmann]

Separate ticket for one issue of #150 .
The SMT solver MathSAT crashes because we use bvadd with three parameters, which is not legal according to the SMT-LIB standard.
The number of paramters is deeply integrated in our SMT library. We want to use bvadd with three parameters because

1. more conveniant and Z3 and CVC4 support it
2. interpolants genereated by Z3 contain bvadd with more than two parameters

(The function bvadd with more than two parameters does not occur that often in practice, since we construct affine terms that summarize literals also for bitvectors.)

[danieldietsch]

Is this the issue we talked about (solutions: add required bvadd definitions during C translation OR allow backtranslation to introduce additional boogie functions) or something else?

[Heizmann]

No, is a different issue.

[Heizmann]

Thanks to Alberto Griggio, MathSAT support bvadd with multiple parameters. So for MathSAT the problem is gone.
The problem will however arise again if we use another solver or if we want to submit standard compliant SMT-LIB benchmarks.

[danieldietsch]

@Heizmann: Then lets keep this ticket around as reminder.