reworked the linear and og implementation based on available variables theory

1 files changed, 2 insertions, 1 deletions

diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 4e4bfbcf..82871466 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -4,6 +4,7 @@ function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
 procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);

 ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);

 

+procedure Allocate() returns ({:linear "1"} x: [int]bool);

 

 procedure {:entrypoint} main() 

 {

@@ -11,7 +12,7 @@ procedure {:entrypoint} main()
    var {:linear "1"} x1: [int] bool;

    var {:linear "1"} x2: [int] bool;

 

-   havoc x;

+   call x := Allocate();

    assume x == mapconstbool(true);

 

    call x1, x2 := Split(x);