Open
Description
Verifying the following 2 versions of a file with ViperServer results both times in a successful verification even though the second one should fail (discovered by @tdardinier):
field f: Int
function g(x: Ref): Bool
ensures false
method main(x: Ref)
{
assert false
}
field f: Int
function g(x: Ref): Bool
// ensures false
method main(x: Ref)
{
assert false
}