summaryrefslogtreecommitdiff
path: root/Test/linear/allocator.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/linear/allocator.bpl')
-rw-r--r--Test/linear/allocator.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index 4b162a83..d723cbed 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -3,7 +3,7 @@ procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
call i := A(i);
assert false;
}