blob: 18f518dab319fb37091e8f400e9c91d252e1b2db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
procedure Split({:linear_in "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 main()
{
var {:linear "1"} x: [int] bool;
var {:linear "1"} x1: [int] bool;
var {:linear "1"} x2: [int] bool;
call x := Allocate();
assume x == mapconstbool(true);
call x1, x2 := Split(x);
assert false;
}
|