From abee810ceedbf551194788164fdf723edc511c0c Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 12 Feb 2016 16:47:14 -0800
Subject: (Honestly, I don't know what I'm doing. I'm trying to revert these
 changes, but Git doesn't actually say what sort of commit I'm doing. Well,
 here goes.)

---
 Test/snapshots/Snapshots41.v0.bpl | 70 +++++++++++++++++------------------
 Test/snapshots/Snapshots41.v1.bpl | 78 +++++++++++++++++++--------------------
 2 files changed, 74 insertions(+), 74 deletions(-)

diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
index 631fe544..dbfe3e2d 100644
--- a/Test/snapshots/Snapshots41.v0.bpl
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -1,35 +1,35 @@
-procedure {:checksum "0"} M(x: int);
-implementation {:id "M"} {:checksum "1"} M(x: int)
-{                     assert x < 20 || 10 <= x;  // always true
-  assert x < 10;  // error
-  call Other(x);  // error: precondition violation
-}
-
-procedure {:checksum "10"} Other(y: int);
-  requires 0 <= y;
-implementation {:id "Other"} {:checksum "11"} Other(y: int)
-{
-}
-
-procedure {:checksum "20"} Posty() returns (z: int);
-  ensures 2 <= z;  // error: postcondition violation
-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
-{
-  var t: int;
-  t := 20;
-  if (t < z) {
-  } else {  // the postcondition violation occurs on this 'else' branch
-  }
-}
-
-procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
-implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
-{
-  assert u != 53;  // error
-}
-
-procedure {:checksum "40"} NoChangeAndCorrect();
-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
-{
-  assert true;
-}
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{                     assert x < 20 || 10 <= x;  // always true
+  assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+}
+
+procedure {:checksum "10"} Other(y: int);
+  requires 0 <= y;
+implementation {:id "Other"} {:checksum "11"} Other(y: int)
+{
+}
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+{
+  assert u != 53;  // error
+}
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
+{
+  assert true;
+}
diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
index 0cd9fbf9..9864e0e4 100644
--- a/Test/snapshots/Snapshots41.v1.bpl
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -1,39 +1,39 @@
-procedure {:checksum "0"} M(x: int);
-implementation {:id "M"} {:checksum "1"} M(x: int)
-{
-assert x < 20 || 10 <= x;  // always true
-  
-       assert x < 10;  // error
-  call Other(x);  // error: precondition violation
-  assert x == 7;  // error: this is a new error in v1
-}
-
-
-       procedure {:checksum "10"} Other(y: int);
-         requires 0 <= y;
-       implementation {:id "Other"} {:checksum "11"} Other(y: int)
-       {
-       }
-
-
-
-procedure {:checksum "20"} Posty() returns (z: int);
-  ensures 2 <= z;  // error: postcondition violation
-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
-{
-  var t: int;
-  t := 20;
-  if (t < z) {
-    assert true;  // this is a new assert
-  } else {  // the postcondition violation occurs on this 'else' branch
-  }
-}
-
-  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
-  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
-  {
-       assert u != 53;  // error
-  }
-
-procedure {:checksum "40"} NoChangeAndCorrect();
-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{
+assert x < 20 || 10 <= x;  // always true
+  
+       assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+  assert x == 7;  // error: this is a new error in v1
+}
+
+
+       procedure {:checksum "10"} Other(y: int);
+         requires 0 <= y;
+       implementation {:id "Other"} {:checksum "11"} Other(y: int)
+       {
+       }
+
+
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+    assert true;  // this is a new assert
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
+  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+  {
+       assert u != 53;  // error
+  }
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
-- 
cgit v1.2.3