viperproject/silicon

Errors caused by refute statement inside of loop with goto

bruggerl opened this issue · 2 comments

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
}

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
  }
}

Fixed in #774.