ID0000186: **This issue was created automatically from Mantis Issue 186. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000186 | Frama-C | Plug-in > slicing | public | 2009-07-14 | 2014-02-12 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | fixed | | **Priority** | high | **Severity** | crash | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | Frama-C Boron-20100401 | **Fixed in Version** | Frama-C Boron-20100401 | ### Description : Stack overflow for the following code: /*@ requires y == 1; @ ensures @ \result == 2*y; @*/ int x(int y, int z) { //@ assert y == 1; //@ assert y + z == 3; return 2*y*z1(); } int main() { x(1,2); return 0; } int z1() { return x(2,2); }