ID0002156: **This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002156 | Frama-C | Plug-in > wp | public | 2015-09-03 | 2015-09-07 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | juki21c | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | Both Ubuntu and OS X | **OS Version** | - | | **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - | ### Description : I experienced that Frama-C/WP was very slow in generating the proof obligations only (skipping invoking any provers). For the attached files, code6.c takes about 1 min. code10.c takes about 15 min. code12.c abnormally terminates Frama-C with a stack overflow error. ### Steps To Reproduce : > frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code6.c > frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code10.c > frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code12.c ## Attachments - [code.zip](/uploads/f899faa93ff0631830e910686ea4ef7d/code.zip)