1 files changed, 5 insertions, 13 deletions
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index f0de76d5..5bc75324 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -10,33 +10,25 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x
 }
 
-procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);
-  ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
-
-
 procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
-   free requires {:layer 1} permVar_in == ch_mapconstbool(true);
-   free requires {:layer 1} permVar_in[0];
-   free requires {:layer 1} x == 0;
+   requires {:layer 1} permVar_in == ch_mapconstbool(true);
+   requires {:layer 1} x == 0;
 {
     var {:linear "Perm"} permVar_out: [int]bool;
-    var {:linear "Perm"} permVarOut2: [int]bool;
 
     permVar_out := permVar_in;
 
     yield;
     assert {:layer 1} x == 0;
-    assert {:layer 1} permVar_out[0];
     assert {:layer 1} permVar_out == ch_mapconstbool(true);
 
-    call permVar_out, permVarOut2 := Split(permVar_out);
-    async call foo(permVarOut2);
+    async call foo(permVar_out);
     yield;
 }
 
 procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 
-  free requires {:layer 1} permVar_in != ch_mapconstbool(false);
-  free requires {:layer 1} permVar_in[1];
+  requires {:layer 1} permVar_in != ch_mapconstbool(false);
+  requires {:layer 1} permVar_in[1];
   requires {:layer 1} x == 0;
 {
   var {:linear "Perm"} permVar_out: [int]bool;