insertion of "assert true" after a statement influences provability of the statement's contract
ID0002226: This issue was created automatically from Mantis Issue 2226. Further discussion may take place here.
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp p1on.c" on the attached program proves both the statement contract in line 9 and the trivial assertion in line 11, as expected.
However, if line 11 is commented out, Alt-Ergo immediately reports "unknown" on line 9. (Cvc4 runs into its timeout then.) The file "foo_stmt_post_Alt-Ergo.mlw" contains the goal "goal foo_stmt_post: false" for some reason.
It seems that the statement contract is translated in a wrong way, unless the final trivla assertion is present in line 11.