Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002286Frama-CPlug-in > wppublic2017-02-27 15:592017-02-27 16:30
Assigned Tocorrenson 
PlatformSilicon-20161101OSxubuntuOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002286: lemma tacitly omitted from prover assumptions
DescriptionRunning "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.
TagsNo tags attached.
Attached Filesc file icon bug1.c [^] (976 bytes) 2017-02-27 16:00 [Show Content]
? file icon why_495d09_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,628 bytes) 2017-02-27 16:06
? file icon why_767c25_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,439 bytes) 2017-02-27 16:07
? file icon why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2 [^] (14,441 bytes) 2017-02-27 16:07

- Relationships

-  Notes
Jochen (reporter)
2017-02-27 16:06

I also attach the "z3" input files: "why_495d09_Axiomatic2-T-Q_addIncAdd.smt2" for "incAdd } addAdd " "why_767c25_Axiomatic2-T-Q_addIncAdd.smt2" for " } incAdd addAdd" "why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2" for " } addAdd incAdd"

- Issue History
Date Modified Username Field Change
2017-02-27 15:59 Jochen New Issue
2017-02-27 15:59 Jochen Status new => assigned
2017-02-27 15:59 Jochen Assigned To => correnson
2017-02-27 16:00 Jochen File Added: bug1.c
2017-02-27 16:06 Jochen Note Added: 0006363
2017-02-27 16:06 Jochen File Added: why_495d09_Axiomatic2-T-Q_addIncAdd.smt2
2017-02-27 16:07 Jochen File Added: why_767c25_Axiomatic2-T-Q_addIncAdd.smt2
2017-02-27 16:07 Jochen File Added: why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker