diff options
Diffstat (limited to 'Test/civl/alloc.bpl')
| -rw-r--r-- | Test/civl/alloc.bpl | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl index 56515ba8..68b7e6c6 100644 --- a/Test/civl/alloc.bpl +++ b/Test/civl/alloc.bpl @@ -127,7 +127,7 @@ ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i]; procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int); modifies pool; -requires !dom(pool)[i]; +requires dom(l)[i]; ensures pool == Add(old(pool), i); procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap); |