diff options
Diffstat (limited to 'Test/AbsHoudini/f1.bpl')
| -rw-r--r-- | Test/AbsHoudini/f1.bpl | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/AbsHoudini/f1.bpl b/Test/AbsHoudini/f1.bpl index 5ea6797b..e5ed85ef 100644 --- a/Test/AbsHoudini/f1.bpl +++ b/Test/AbsHoudini/f1.bpl @@ -26,7 +26,7 @@ procedure foo() }
procedure {:template} summaryTemplate();
- ensures g == old(g) + 1;
- ensures g == old(g) + 2;
- ensures g == old(g) + 3;
+ ensures {:post} g == old(g) + 1;
+ ensures {:post} g == old(g) + 2;
+ ensures {:post} g == old(g) + 3;
ensures {:pre} old(g) == 0;
|