diff options
Diffstat (limited to 'Test/snapshots/Snapshots9.v0.bpl')
| -rw-r--r-- | Test/snapshots/Snapshots9.v0.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/snapshots/Snapshots9.v0.bpl b/Test/snapshots/Snapshots9.v0.bpl index 73dcd9aa..5b2cf68c 100644 --- a/Test/snapshots/Snapshots9.v0.bpl +++ b/Test/snapshots/Snapshots9.v0.bpl @@ -12,4 +12,6 @@ implementation {:id "M"} {:checksum "1"} M(n: int) procedure {:checksum "2"} N(n: int) returns (r: int);
requires 0 < n;
+ requires true;
ensures 0 < r;
+ ensures true;
|