summaryrefslogtreecommitdiff
path: root/Test/linear/list.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/linear/list.bpl')
-rw-r--r--Test/linear/list.bpl4
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index 9a333351..f4badca9 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -1,3 +1,7 @@
+type X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+
var head: X;
var tail: X;
var {:linear "Mem"} D: [X]bool;