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);