1 files changed, 42 insertions, 42 deletions
diff --git a/Test/civl/new1.bpl b/Test/civl/new1.bpl
index b80b6315..c2feb179 100644
--- a/Test/civl/new1.bpl
+++ b/Test/civl/new1.bpl
@@ -1,42 +1,42 @@
-// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
-
-var {:layer 0,1} g:int;
-
-function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
-{
-  x
-}
-
-procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
-requires {:layer 1} permVar_in[0] && g == 0;
-{
-  var {:linear "Perm"} permVar_out: [int]bool;
-  permVar_out := permVar_in;
-
-  yield;
-  assert {:layer 1} permVar_out[0];
-  assert {:layer 1} g == 0;
-
-  call IncrG();
-
-  yield;
-  assert {:layer 1} permVar_out[0];
-  assert {:layer 1} g == 1;
-}
-
-procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)
-requires {:layer 1} Permissions == mapconstbool(true);
-{
-  yield;
-  call SetG(0);
-  async call PB(Permissions);
-  yield;
-}
-
-procedure {:yields} {:layer 0,1} SetG(val:int);
-ensures {:atomic} |{A: g := val; return true; }|;
-
-procedure {:yields} {:layer 0,1} IncrG();
-ensures {:atomic} |{A: g := g + 1; return true; }|;
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
+
+var {:layer 0,1} g:int;
+
+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
+{
+  x
+}
+
+procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
+requires {:layer 1} permVar_in[0] && g == 0;
+{
+  var {:linear "Perm"} permVar_out: [int]bool;
+  permVar_out := permVar_in;
+
+  yield;
+  assert {:layer 1} permVar_out[0];
+  assert {:layer 1} g == 0;
+
+  call IncrG();
+
+  yield;
+  assert {:layer 1} permVar_out[0];
+  assert {:layer 1} g == 1;
+}
+
+procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)
+requires {:layer 1} Permissions == mapconstbool(true);
+{
+  yield;
+  call SetG(0);
+  async call PB(Permissions);
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} SetG(val:int);
+ensures {:atomic} |{A: g := val; return true; }|;
+
+procedure {:yields} {:layer 0,1} IncrG();
+ensures {:atomic} |{A: g := g + 1; return true; }|;