|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002286||Frama-C||Plug-in > wp||public||2017-02-27 15:59||2017-02-27 16:30|
|Assigned To||correnson|| |
|Product Version||Frama-C 14-Silicon|| |
|Target Version||Fixed in Version|| |
|Summary||0002286: lemma tacitly omitted from prover assumptions|
|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.
|Tags||No tags attached.|
|Attached Files|| bug1.c [^] (976 bytes) 2017-02-27 16:00 [Show Content]
why_495d09_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,628 bytes) 2017-02-27 16:06
why_767c25_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,439 bytes) 2017-02-27 16:07
why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,441 bytes) 2017-02-27 16:07