ID0000846: **This issue was created automatically from Mantis Issue 846. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000846 | Frama-C | Plug-in > jessie | public | 2011-05-30 | 2011-05-30 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - | ### Description : Jessie reports an uncaught exception: Failure("Unexpected internal region in logic") on the attached file. That message vanishes if either - the array access "b[f]" in line 4 is replaced e.g. by "0", - the "decreases" clause in line 8 is deleted, or - the recursive call in line 11 is deleted. (The code is nonsensical, but has been boiled down from a reasonable program.) ## Attachments - [ftest.c](/uploads/9f30f7973db62f3510ab1bdb277ee75a/ftest.c)