search

ultimate-pa / ultimate

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

Soundness-Bug in Abstract Interpretation #78

Open greitsch opened 7 years ago

greitsch commented 7 years ago

On regression/call-recursiveABAB_simple_incorrect.bpl we wrongfully report SAFE, even though the program is supposed to be UNSAFE.

This is currently the only soundness bug in AI (in our regression tests, that is).

greitsch commented 7 years ago

The current Ultimate version does not seem to have any Unsoundness on this file. However, the AIv2_INT_Total-setting produces an assertion error in the inductivity check which may be related to the previous soundness error. All other domains (and settings, incl. INT_P1, INT without Total, and default TA) run into a timeout.