lemma tacitly omitted from prover assumptions
ID0002286: This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002286 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2017-02-27 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Silicon-20161101 | OS | xubuntu | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp -wp-rte -wp-prop=addIncAdd -wp-prover z3 bug1.c" on the attached file verifies the given goal "addIncAdd" in 40ms. However, when the closing brace is moved from line 35 up to line 30, no proof is found in 10s.
A "diff -r" on the wp-out directories shows that the translation of lemma "incAdd" is put into file "A_addAxioms.why" in the former, but into "Axiomatic2.why" in the latter case.
Intercepting the input if "z3" shows that only in the former case the translation is included in the input of "z3"; in the latter case it is missing.
I couldn't find the reason for just omitting "incAdd": exchanging lemmas "incAdd" and "addAdd" in the C source and comparing the "z3" inputs again shows that still "incAdd" is omitted; so the reason could be in it's name of form, but not in it place in source.