Measuring decreasing VC for opaque recursive functions not generated #1271
Description
The following goes through:
import stainless._
import stainless.lang._
import stainless.annotation._
object DecreasesNotDecreasing {
@opaque
def f(x: BigInt): Unit = {
decreases(x)
require(x >= 0)
f(x + 1)
}.ensuring(_ => false)
}Looking at the verification report, it is clear that the VC for "measure decreases" took some holidays...
┌───────────────────┐
╔═╡ stainless summary ╞═════════════════════════════════════════════════════════════════════════════════╗
║ └───────────────────┘ ║
║ f precond. (call f$38(x$111 + BigInt("1"))) valid from cache 1.0 ║
║ Decreases.scala:8:7: f postcondition valid U:smt-z3 0.2 ║
║ Decreases.scala:11:7: f non-negative measure valid from cache 0.0 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 3 valid: 3 (2 from cache) invalid: 0 unknown: 0 time: 1.2 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════════════╝