reworked the linear and og implementation based on available variables theory

1 files changed, 9 insertions, 8 deletions

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 5d627348..ac4a2e21 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -20,6 +20,9 @@ const nil: X;
 procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

+procedure Allocate() returns ({:linear "tid"} xls: X);

+ensures xls != nil;

+

 procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

 requires tidls' != nil && xls' == All();

 {

@@ -29,19 +32,17 @@ requires tidls' != nil && xls' == All();
     var {:linear "x"} xls1: [X]bool;

     var {:linear "x"} xls2: [X]bool;

 

-    havoc tidls, xls;

-    assume tidls' == tidls && xls' == xls;

+    tidls := tidls';

+    xls := xls';

 

     x := 42;

     yield;

     assert xls == All();

     assert x == 42;

     call xls1, xls2 := Split(xls);

-    havoc lsChild;

-    assume (lsChild != nil);

+    call lsChild := Allocate();

     async call thread(lsChild, xls1);

-    havoc lsChild;

-    assume (lsChild != nil);

+    call lsChild := Allocate();

     async call thread(lsChild, xls2);

 }

 

@@ -51,8 +52,8 @@ requires tidls' != nil && xls' != None();
     var {:linear "x"} xls: [X]bool;

     var {:linear "tid"} tidls: X;

 

-    havoc tidls, xls;

-    assume tidls' == tidls && xls' == xls;

+    tidls := tidls';

+    xls := xls';

 

     assume l == nil;

     l := tidls;