summaryrefslogtreecommitdiff
path: root/Test/civl/alloc.bpl
diff options
context:
space:
mode:
authorGravatar Shaz Qadeer <qadeer@microsoft.com>2016-01-10 09:19:12 -0800
committerGravatar Shaz Qadeer <qadeer@microsoft.com>2016-01-10 09:19:12 -0800
commit107dae2093c2049c674cb4a32cd01143765893b9 (patch)
tree14d73f35d87b2cd5befc72e3f0e33c9ffcf8d3c6 /Test/civl/alloc.bpl
parent24a49931e1c7d456008296e1255d8506d28cb18b (diff)
fixed a small problem in the precondition for FreeLinear
Diffstat (limited to 'Test/civl/alloc.bpl')
-rw-r--r--Test/civl/alloc.bpl2
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);