There is strange behavior with the gutter icons when verifying refining an abstract modules.

abstract module Test {
  method Encrypt()
    ensures false
}

module Ok refines Test {
  function test(): int {
    2
  }
  // Might not work as expected
  method Encrypt() {
  }
}

See the result here

• The error on the refined module is expressed in the abstract module, which completely breaks not only the gutter icons, but also the outline (there is no method Encrypt in the refined module)

We can use this behavior to pretend we prove false, at least on the gutter icons:

It's even worse when the abstract module is included instead of being in the same file, because its errors are reported on the file containing the refined module, which is out of offset. Look at the postcondition error underlined.... in the comment.