`FragmentChecker` does not go trough `ensuring`

[mario-bucev]

In the following snippet, we expect the FragmentChecker to report an error due to using the Scala variant of Option:

object EnsuringMask {
  def test(): Int = {
    val x = scala.Option(2)
    5
  } ensuring (_ == 5)
}

However, it does not, and we instead get a recovery at a later phase:

[ Error  ] test$0 depends on missing dependencies: Option$4, apply$14.
[ Fatal  ] Cannot recover from missing dependencies
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

This issue does not affect StaticChecks (for some reasons)

[mario-bucev]

Not directly related, but the postcondition is also affected as well:

object EnsuringPostcond {
  def test(): Int = {
    5
  } ensuring (_ == {
    val x = scala.Option(2)
    5
  })
}

This time, StaticChecks is also affected.