You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
importstainless.lang._objectRefnChecks {
deffun(x: BigInt):Option[Some[BigInt]] = {
(
if (x ==0) Some[Some[BigInt]](Some(x))
elseNone[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):
deffun(x: BigInt):Option[{ v$3305: Option[BigInt] | v$3305 is Some }] = {
valtargetBound$3303:Boolean= x ==0// v$3306 from the VC stems from herevaltargetBound$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$3304match {
case _ =>None$325[{ v$3310: Option[BigInt] | v$3310 is Some }]()
}
}
The text was updated successfully, but these errors were encountered:
The following snippet is said to be invalid:
In particular for the VC:
The
AdtSpecialization
introduces these refinements (this transformation seems to be correct):The text was updated successfully, but these errors were encountered: