summaryrefslogtreecommitdiff
path: root/Test/AbsHoudini/test10.bpl
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-27 19:55:30 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-27 19:55:30 +0100
commit75416c24e78d9992c10fbb86ba458e813acf943d (patch)
tree9d61f88b5a6e7e9b521465f41f2509a445555ad8 /Test/AbsHoudini/test10.bpl
parent07ede3edee0d0a2b1518472d775f3959c84806eb (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.bpl2
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;