obligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo nevertheless
ID0001999: This issue was created automatically from Mantis Issue 1999. Further discussion may take place here.
|ID0001999||Frama-Clang||Plug-in > wp||public||2014-11-27||2014-11-27|
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp 167.c" on the attached program yields the output:
... [wp] [Alt-Ergo] Goal typed_foo_assert : Unknown ...
The corresponding file "foo_assert_Alt-Ergo.mlw" contains the goal "goal foo_assert: false", in line 369.
Apparently, Qed succeeds to recognize that the assertion in line 3 of file "167.c" is provably wrong. However, the obligation is passed to the external prover Alt-Ergo nevertheless.
Similar to goals recognized as true by Qed, goals recognized as false needn't be passed to subsequent provers.