require condition disappear in presence of statements

[mario-bucev]

@samuelchassot discovered a bug where having statements within require somehow make the required condition go away.
For instance, this should go through, but does not:

object BlindRequire {
  def myLemma(x: BigInt): Unit = {
    ()
  }.ensuring(_ => x + x == 2 * x)

  def blind(x: BigInt): Unit = {
    require {
      myLemma(x)
      x >= 0
    }
    assert(x >= 0) // fails
  }
}

[mario-bucev]

Oh no, it's imperative again :(

[ Debug  ] Symbols before ImperativeCodeElimination
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def myLemma((x: BigInt) @pure): Unit = {
[ Debug  ]   ()
[ Debug  ] } ensuring {
[ Debug  ]   (_$1: Unit) => x + x == 2 * x
[ Debug  ] }
[ Debug  ] 
[ Debug  ] def blind((x: BigInt) @pure): Unit = {
[ Debug  ]   myLemma(x)
[ Debug  ]   require(x >= 0)
[ Debug  ]   assert(x >= 0)
[ Debug  ]   ()
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Symbols after ImperativeCodeElimination
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def myLemma((x: BigInt) @pure): Unit = {
[ Debug  ]   ()
[ Debug  ] } ensuring {
[ Debug  ]   (_$1: Unit) => x + x == 2 * x
[ Debug  ] }
[ Debug  ] 
[ Debug  ] def blind((x: BigInt) @pure): Unit = {
[ Debug  ]   val tmp: Unit = myLemma(x)
[ Debug  ]   assert(x >= 0)
[ Debug  ]   require(x >= 0)
[ Debug  ]   ()
[ Debug  ] }