From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/bitvectors/arrays.bpl | 84 +++++++++++++++++++++++-----------------------
 1 file changed, 42 insertions(+), 42 deletions(-)

(limited to 'Test/bitvectors/arrays.bpl')

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
-- 
cgit v1.2.3