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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001999 | Frama-Clang | Plug-in > wp | public | 2014-11-27 | 2014-11-27 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.