diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 19:55:30 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-27 19:55:30 +0100 |
| commit | 75416c24e78d9992c10fbb86ba458e813acf943d (patch) | |
| tree | 9d61f88b5a6e7e9b521465f41f2509a445555ad8 /Test/AbsHoudini/pred5.bpl | |
| parent | 07ede3edee0d0a2b1518472d775f3959c84806eb (diff) | |
Convert the AbsHoudini tests to lit tests. They weren't being run by the old
infrastructure so I have not bothered to update the Answer file. These tests
are still disabled by the lit.local.cfg file in the AbsHoudini folder because
the following tests fail or weren't even being run previously (these are left
unresolved because I do not know how these tests are meant to be run)
UNRESOLVED: Boogie :: AbsHoudini/f1.bpl (1 of 32)
UNRESOLVED: Boogie :: AbsHoudini/imp1.bpl (7 of 32)
UNRESOLVED: Boogie :: AbsHoudini/int1.bpl (8 of 32)
UNRESOLVED: Boogie :: AbsHoudini/multi.bpl (9 of 32)
FAIL: Boogie :: AbsHoudini/quant3.bpl (22 of 32)
FAIL: Boogie :: AbsHoudini/quant5.bpl (28 of 32)
Diffstat (limited to 'Test/AbsHoudini/pred5.bpl')
| -rw-r--r-- | Test/AbsHoudini/pred5.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl index 6940e820..762a354f 100644 --- a/Test/AbsHoudini/pred5.bpl +++ b/Test/AbsHoudini/pred5.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:PredicateAbs %s > %t
+// RUN: %diff %s.expect %t
function {:existential true} b1(x: bool) : bool;
procedure main()
|