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/test10.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/test10.bpl')
| -rw-r--r-- | Test/AbsHoudini/test10.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl index a30c3159..76a02e23 100644 --- a/Test/AbsHoudini/test10.bpl +++ b/Test/AbsHoudini/test10.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
+// RUN: %diff %s.expect %t
var sdv_7: int;
var sdv_21: int;
function {:existential true} b1(): bool;
|