From 3b38b009d086c601cae884ad62ceeb9bb16ae5d5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 5 May 2014 19:51:59 +0100
Subject: Enabled most of the name resolution lit tests. They don't all pass
 yet due to a bug in -useBaseNameForFileName.

---
 Test/test0/BadQuantifier.bpl | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Test/test0/BadQuantifier.bpl')

diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl
index b06ab0d9..d202312e 100644
--- a/Test/test0/BadQuantifier.bpl
+++ b/Test/test0/BadQuantifier.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
 
 function f(int) returns (bool);
 axiom (forall int x :: f(x) <== x >= 0);
-- 
cgit v1.2.3