Does not locate the line number of a VC

[agilot]

When running the following snippet of code:

object Bug {
  sealed trait State{
    def plant: Tree = {
      this match {
      case Baz(t1, t2) => {
          val kd1 = t1.plant
          val kd2 = t2.plant
          if(kd1.s == Foo && kd1.s == Foo){
              Node(Foo, kd1, kd2)
          }
          else{
              Leaf
          }
      }
      case _ => Leaf
      }
    }
  }
  case object Foo extends State
  case class Bar(s: State) extends State
  case class Baz(s1: State, s2: State) extends State

  sealed trait Tree {

    def s: State = this match {
      case Leaf => Baz(Foo, Foo)
      case Node(s, _, _) => s
    }

    def isFoo: Boolean = {
      this match{
        case Node(s, bkd1, bkd2) => {
          bkd1.isFoo && bkd2.isFoo &&
          bkd1.s == Foo && bkd2.s == Foo
        }
        case _ => false

      }
    }
    
  }
  case object Leaf extends Tree
  case class Node(s: State, bkd1: Tree, bkd2: Tree) extends Tree

  @opaque @pure
  def plantThm(s: State): Unit = {
    s match {
      case Foo => ()
      case Bar(t) => {
        plantThm(t)
      }
      case Baz(t1, t2) => {
        plantThm(t1)
        plantThm(t2)
      }
    }
  }.ensuring(
    s.plant.isFoo
  )
}

one gets the following output:

[Warning ]  - Result for 'postcondition' VC for plantThm @?:?:
[Warning ] s.isInstanceOf[Foo] || !s.isInstanceOf[Bar] || {
[Warning ]   val res: Unit = plantThm(s.s)
[Warning ]   isFoo(plant(s))
[Warning ] }
[Warning ]  => TIMEOUT

even though one would expect the VC to be located.