From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 28 Jun 2015 01:44:30 +0100
Subject: Normalise line endings using a .gitattributes file. Unfortunately
 this required that this commit globally modify most files. If you want to use
 git blame to see the real author of a line use the ``-w`` flag so that
 whitespace changes are ignored.

---
 Test/generalizedarray/Maps.bpl | 120 ++++++++++++++++++++---------------------
 1 file changed, 60 insertions(+), 60 deletions(-)

(limited to 'Test/generalizedarray')

diff --git a/Test/generalizedarray/Maps.bpl b/Test/generalizedarray/Maps.bpl
index 24521194..89a6403a 100644
--- a/Test/generalizedarray/Maps.bpl
+++ b/Test/generalizedarray/Maps.bpl
@@ -1,61 +1,61 @@
-// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type X;
-
-function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
-function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
-function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
-function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
-function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
-function {:builtin "MapConst"} mapconstint(int) : [X]int;
-function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
-function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
-function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
-function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
-function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
-function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
-function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
-function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
-function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
-function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
-
-
-
-const FF: [X]bool;
-axiom FF == mapconstbool(false);
-
-const TT: [X]bool;
-axiom TT == mapconstbool(true);
-
-const MultisetEmpty: [X]int;
-axiom MultisetEmpty == mapconstint(0);
-
-function {:inline} MultisetSingleton(x: X) : [X]int
-{
-  MultisetEmpty[x := 1]
-}
-
-function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
-{
-  mapadd(a, b)
-}
-
-function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int
-{
-  mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
-}
-
-procedure foo() {
-  var x: X;
-
-  assert FF != TT;
-  assert mapnot(FF) == TT;
-
-  assert MultisetSingleton(x) != MultisetEmpty;
-  assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
-  assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
-  assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
+// RUN: %boogie -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+
+function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} mapconstint(int) : [X]int;
+function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
+function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
+function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
+
+
+
+const FF: [X]bool;
+axiom FF == mapconstbool(false);
+
+const TT: [X]bool;
+axiom TT == mapconstbool(true);
+
+const MultisetEmpty: [X]int;
+axiom MultisetEmpty == mapconstint(0);
+
+function {:inline} MultisetSingleton(x: X) : [X]int
+{
+  MultisetEmpty[x := 1]
+}
+
+function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
+{
+  mapadd(a, b)
+}
+
+function {:inline} MultisetMinus(a: [X]int, b: [X]int)  : [X]int
+{
+  mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
+}
+
+procedure foo() {
+  var x: X;
+
+  assert FF != TT;
+  assert mapnot(FF) == TT;
+
+  assert MultisetSingleton(x) != MultisetEmpty;
+  assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
+  assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
+  assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
 }
\ No newline at end of file
-- 
cgit v1.2.3