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/quant3.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/quant3.bpl')
| -rw-r--r-- | Test/AbsHoudini/quant3.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl index cc0ef79e..10fb72c7 100644 --- a/Test/AbsHoudini/quant3.bpl +++ b/Test/AbsHoudini/quant3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:HoudiniConst -z3opt:MBQI=true %s > %t
+// RUN: %diff %s.expect %t
function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;
procedure foo ()
|