Location misreported as <empty tree>[{ x: Object | @dropConjuct false }]

[Maeeen]

Using Stainless 0.9.8.9, the following example:

import stainless.lang.*
import stainless.annotation.*
import stainless.collection.*

def example(x: List[Int]) =
    require(x.forall(_ >= 0))
    require(!x.isEmpty)

    if x.head < 0 then
        assert(false)
    else
        x.head

A verification condition (unknown to me) ends up as <empty tree>[{ x: Object | @dropConjunct false }]:

[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                                                                                               ║
[  Info  ] ║ ./src/Test.scala:9:8:    example  precond. (call head[Int](x))                                                                                 valid  nativez3  0.2 ║
[  Info  ] ║ ./src/Test.scala:10:9:   example  body assertion: Expression of type Nothing: assert(false)
[  Info  ] <empty tree>[{ x: Object | @dropConjunct false }]  valid  nativez3  0.0 ║
[  Info  ] ║ ./src/Test.scala:12:9:   example  precond. (call head[Int](x))                                                                                 valid  nativez3  0.0 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 3    valid: 3    (0 from cache, 0 trivial) invalid: 0    unknown: 0    time:    0.27                                                                         ║
[  Info  ] ╚═════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝