import stainless.lang._
object RefnChecks {
def fun(x: BigInt): Option[Some[BigInt]] = {
(
if (x == 0) Some[Some[BigInt]](Some(x))
else None[Some[BigInt]]()
) match {
case _ => None()
}
}
}
In particular for the VC:
[Warning ] - Result for 'refinements checks for subtyping' VC for fun @6:7:
[Warning ] v$3306.isInstanceOf[Some]
[Warning ] RefnChecks.scala:6:7: => INVALID
if (x == 0) Some[Some[BigInt]](Some(x))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
[Warning ] Found counter-example:
[Warning ] v$3306: Option[BigInt] -> None[BigInt]()
The AdtSpecialization introduces these refinements (this transformation seems to be correct):
def fun(x: BigInt): Option[{ v$3305: Option[BigInt] | v$3305 is Some }] = {
val targetBound$3303: Boolean = x == 0
// v$3306 from the VC stems from here
val targetBound$3304: Option[{ v$3306: Option[BigInt] | v$3306 is Some }] = if (targetBound$3303) {
Some[{ v$3307: Option[BigInt] | v$3307 is Some }](Some[BigInt](x))
} else {
None$325[{ v$3308: Option[BigInt] | v$3308 is Some }]()
}
targetBound$3304 match {
case _ =>
None$325[{ v$3310: Option[BigInt] | v$3310 is Some }]()
}
}
The following snippet is said to be invalid:
In particular for the VC:
The
AdtSpecialization
introduces these refinements (this transformation seems to be correct):