search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
194 stars 40 forks source link

MathSAT crashes because we use bvadd with three parameters #185

Open Heizmann opened 7 years ago

Heizmann commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

No, is a different issue.

Heizmann commented 7 years ago

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 commented 7 years ago

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