From 107dae2093c2049c674cb4a32cd01143765893b9 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <qadeer@microsoft.com>
Date: Sun, 10 Jan 2016 09:19:12 -0800
Subject: fixed a small problem in the precondition for FreeLinear

---
 Test/civl/alloc.bpl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
-- 
cgit v1.2.3