Conditional mustTerminate obligation not allowed in loop invariant

[viper-admin]

Created by @vakaras on 2016-03-25 16:04

The following example fails to verify because loop does not promise to terminate:

#!Chalice

class A {
  method test1()
    requires false ==> mustTerminate(1)
  {
  }
  method test2()
  {
    //:: UnexpectedOutput(invariant.not.established:assertion.false, /Chalice2Silver/issue/79/)
    while (true)
      invariant false ==> mustTerminate(1)
    {
    }
  }
}