Errors caused by refute statement inside of loop with goto
bruggerl opened this issue · 2 comments
bruggerl commented
When verifying the following method, Silicon throws an exception (leading to a "Verification aborted exceptionally" error) and also falsely reports that the refute
statement does not hold:
method test()
{
label l0
refute false
goto l0
}
marcoeilers commented
The refute plugin generates this code, which looks fine to me but makes Silicon crash:
method test()
{
{
label l0
{
var __plugin_refute_nondet1: Bool
if (__plugin_refute_nondet1) {
assert false
inhale false
}
}
goto l0
}
}
marcoeilers commented
Fixed in #774.