1
Vote

AbsHoudini tests need to be enabled and fixed

description

The tests in Test/AbsHoudini are currently disabled because some of them are broken. This is bad because we aren't tracking regressions introduced for this feature.
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 (24 of 32)
FAIL: Boogie :: AbsHoudini/quant5.bpl (25 of 32)
The the lit.local.cfg file needs to removed from the directory and then those tests need to be fixed.

comments