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
inox.package$FatalError: Typing context already contains variable x$205
at inox.package$FatalError$.apply(package.scala:24)
at inox.Reporter.onFatal(Reporter.scala:47)
at inox.Reporter.internalError(Reporter.scala:63)
at inox.Reporter.internalError(Reporter.scala:115)
at stainless.verification.TypeCheckerContext$TypingContext.checkFreshTermVariable(TypeCheckerContext.scala:33)
...
The problem stems from a refinement type not being properly freshened.
The first time it happens (without causing a crash) is in
We can see that x$161 is declared twice (which gets replaced by x$205 later on and ultimately causing the error).
It seems that the TypeInstantiator should freshen the instantiated type.
The text was updated successfully, but these errors were encountered:
Originally discovered by @agilot
The following cause a crash in
TypeChecker
:with the following message:
The problem stems from a refinement type not being properly freshened.
The first time it happens (without causing a crash) is in
stainless/core/src/main/scala/stainless/verification/TypeChecker.scala
Line 743 in 9fbc579
This returns the following typed definition:
We can see that
x$161
is declared twice (which gets replaced byx$205
later on and ultimately causing the error).It seems that the
TypeInstantiator
should freshen the instantiated type.The text was updated successfully, but these errors were encountered: