From 5c9156cb9422477f0fc1cd34d50753a6f7de09dc Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 7 May 2014 21:20:35 +0100
Subject: Enabled "linear type checking" lit tests.

---
 Test/linear/typecheck.bpl | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Test/linear/typecheck.bpl')

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index c8510909..72067494 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory  %s > %t
+// RUN: %diff %s.expect %t
 type X;
 
 procedure A()
-- 
cgit v1.2.3