1 files changed, 42 insertions, 42 deletions
diff --git a/Test/bitvectors/arrays.bpl b/Test/bitvectors/arrays.bpl
index dae54e63..c6368fbe 100644
--- a/Test/bitvectors/arrays.bpl
+++ b/Test/bitvectors/arrays.bpl
@@ -1,43 +1,43 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const unique f1 : Field int;
-const unique f2 : Field bv32;
-const unique f3 : Field bool;
-
-const unique r1 : ref;
-const unique r2 : ref;
-
-var H : <x>[ref,Field x]x;
-
-procedure foo()
-  modifies H;
-{
-  var i : int;
-  var b : bv32;
-  var c : bool;
-
-  H[r1, f1] := 3;
-  H[r1, f2] := 77bv32;
-  H[r1, f3] := true;
-  i := H[r1,f1];
-  b := H[r1,f2];
-  c := H[r1,f3];
-  assert i == 3;
-  assert b == 77bv32;
-  assert H[r1,f3];
-}
-
-var B : [bv32]bv32;
-
-procedure bar()
-  modifies B;
-{
-  var b : bv32;
-
-  B[42bv32] := 77bv32;
-  b := B[42bv32];
-  assert b == 77bv32;
-}
-
-
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const unique f1 : Field int;
+const unique f2 : Field bv32;
+const unique f3 : Field bool;
+
+const unique r1 : ref;
+const unique r2 : ref;
+
+var H : <x>[ref,Field x]x;
+
+procedure foo()
+  modifies H;
+{
+  var i : int;
+  var b : bv32;
+  var c : bool;
+
+  H[r1, f1] := 3;
+  H[r1, f2] := 77bv32;
+  H[r1, f3] := true;
+  i := H[r1,f1];
+  b := H[r1,f2];
+  c := H[r1,f3];
+  assert i == 3;
+  assert b == 77bv32;
+  assert H[r1,f3];
+}
+
+var B : [bv32]bv32;
+
+procedure bar()
+  modifies B;
+{
+  var b : bv32;
+
+  B[42bv32] := 77bv32;
+  b := B[42bv32];
+  assert b == 77bv32;
+}
+
+
 type Field a, ref;
 \ No newline at end of file