Test/linear/f2.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
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 {:entrypoint} main() 
{
   var {:linear "1"} x: [int] bool;
   var {:linear "1"} x1: [int] bool;
   var {:linear "1"} x2: [int] bool;

   havoc x;
   assume x == mapconstbool(true);

   call x1, x2 := Split(x);
   assert false;
}