From ce2783c76457d04bab57e116ef14f106c2d8edda Mon Sep 17 00:00:00 2001
From: Robert <27515600+RobertMensing@users.noreply.github.com>
Date: Thu, 28 Nov 2024 12:57:40 +0100
Subject: [PATCH] Fixed scoping of let in PureMethodsToFunctions

---
 .../vct/rewrite/PureMethodsToFunctions.scala  | 31 ++++++++++---------
 1 file changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala
index ff0c37ed0..c3d17d891 100644
--- a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala
+++ b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala
@@ -33,9 +33,6 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] {
 
   val currentAbstractMethod: ScopedStack[AbstractMethod[Pre]] = ScopedStack()
 
-  private val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] =
-    SuccessionMap()
-
   def countAssignments(v: Variable[Pre], s: Statement[Pre]): Option[Int] =
     s match {
       case Return(_) => Some(0)
@@ -98,18 +95,22 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] {
         }
         toExpression(impl, alt)
       case Assign(Local(ref), e) =>
-        alt match {
-          case Some(exprAlt) =>
-            val vDecl = variableMap.getOrElseUpdate(
-              ref.decl,
-              variables.collect { dispatch(ref.decl) }._1.head,
-            )
-            Some(Let[Post](vDecl, dispatch(e), exprAlt))
-          case None =>
-            throw MethodCannotIntoFunction(
-              currentAbstractMethod.top,
-              "Pure method cannot end with assign statement",
-            )
+        localHeapVariables.scope {
+          variables.scope {
+            alt match {
+              case Some(exprAlt) =>
+                Some(Let[Post](
+                  variables.collect { dispatch(ref.decl) }._1.head,
+                  dispatch(e),
+                  exprAlt,
+                ))
+              case None =>
+                throw MethodCannotIntoFunction(
+                  currentAbstractMethod.top,
+                  "Pure method cannot end with assign statement",
+                )
+            }
+          }
         }
 
       case _ => None