Filter out immutable ValDefs from rewritings.

vkuncak · May 25, 2021 · 7f78b2c · 7f78b2c
1 parent 980ad46
commit 7f78b2c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -411,7 +411,9 @@ trait AntiAliasing
             } else {
               val newScrut = transform(scrut, env)
               val newCases = cses.map { case mc @ MatchCase(pattern, guard, rhs) =>
-                val newRewritings = mapForPattern(newScrut, pattern)
+                val newRewritings =
+                  mapForPattern(newScrut, pattern).filterKeys(v => isMutableType(v.getType))
+
                 val newGuard = guard.map(transform(_, env withRewritings newRewritings))
                 val newRhs = transform(rhs, env withRewritings newRewritings)
                 MatchCase(pattern, newGuard, newRhs).copiedFrom(mc)

diff --git a/frontends/benchmarks/imperative/valid/CastCorrectness.scala b/frontends/benchmarks/imperative/valid/CastCorrectness.scala
@@ -35,7 +35,7 @@ object CastCorrectness {
   }
 
   @pure
-  def remove_from_list(var0: List[Int]): Unit = {
+  def removeFromList(var0: List[Int]): Unit = {
     var list: List[Int] = freshCopy(var0)
     list match {
       case Cons(first_elem, _) =>