summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots18.v1.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/snapshots/Snapshots18.v1.bpl')
-rw-r--r--Test/snapshots/Snapshots18.v1.bpl48
1 files changed, 24 insertions, 24 deletions
diff --git a/Test/snapshots/Snapshots18.v1.bpl b/Test/snapshots/Snapshots18.v1.bpl
index 76f8c597..262b5e4f 100644
--- a/Test/snapshots/Snapshots18.v1.bpl
+++ b/Test/snapshots/Snapshots18.v1.bpl
@@ -1,24 +1,24 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
- while (true)
- {
- assert 0 == 0;
-
- call N();
- call N();
-
- if (*)
- {
- break;
- }
-
- assert 1 != 1; // error
- }
-
- assert 2 != 2; // error
-}
-
-procedure {:checksum "3"} N();
- ensures true;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+ while (true)
+ {
+ assert 0 == 0;
+
+ call N();
+ call N();
+
+ if (*)
+ {
+ break;
+ }
+
+ assert 1 != 1; // error
+ }
+
+ assert 2 != 2; // error
+}
+
+procedure {:checksum "3"} N();
+ ensures true;