Missing refinement check for functions with bodies

[cpitclaudel]

The following code crashes Dafny:

abstract module Interface {
  function method NonZero(): int {
    1
  }
}

abstract module Functor {
  import Obj : Interface

  method Boom() {
    print 1 / Obj.NonZero();
  }
}

module Implementation {
  function method NonZero(): int {
    0
  }
}

module Refinement refines Functor {
  import Obj = Implementation
}

method Main() {
  Refinement.Boom();
}

h/t @davidcok @RustanLeino

[cpitclaudel]

Here is a variant that lets you assert false

abstract module Interface {
  const x : int := 1
}

abstract module Functor {
  import Obj : Interface
  lemma NZ() ensures Obj.x == 1 {}
}

module Implementation {
  const x : int := 0
}

module Refinement refines Functor {
  import Obj = Implementation

  method Unsound() ensures false {
    calc { 0; Obj.x; { NZ(); } 1; }
  }
}

method Main() ensures false {
  Refinement.Unsound();
}