From 8ed856180b243cecbfce8edb2db06856c003fffb Mon Sep 17 00:00:00 2001
From: David Ewert <dewert10@gmail.com>
Date: Mon, 6 Jun 2022 18:48:22 -0700
Subject: [PATCH 1/2] Fixed issue where magic wands with differently named let
 bound variables were treated as different

---
 .../scala/viper/silver/ast/Expression.scala     | 12 +++++++++---
 src/test/resources/all/issues/silver/0586.vpr   | 17 +++++++++++++++++
 2 files changed, 26 insertions(+), 3 deletions(-)
 create mode 100644 src/test/resources/all/issues/silver/0586.vpr

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index c3f5966c0..acf5a3d27 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -164,11 +164,11 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
      *   - Replace holes in the wand (subexpressions to evaluate) by local variables
      *     whose names are the type of the hole. E.g. "n + 1" is replaced by an
      *     artificial variable with name "int" and similarly, "n < m" by "bool".
-     *   - Quantified variables are given canonical names based on their depth/level
+     *   - Bound variables are given canonical names based on their depth/level
      *     of nesting in the overall wand. E.g. the subexpression
-     *     "(forall x, y :: b1(x, y) ==> forall z :: b2(x, y, z)) && forall x :: b3(x)"
+     *     "(forall x, y :: b1(x, y) ==> forall z :: b2(x, y, z)) && (let v == (0) in v == 0)"
      *     is transformed into
-     *     "(forall q1, q2 :: b1(q1, q2) ==> forall q3 :: b2(q1, q2, q3)) && forall q1 :: b3(q1)".
+     *     "(forall q1, q2 :: b1(q1, q2) ==> forall q3 :: b2(q1, q2, q3)) && (let q1 == (0) in q1 == 0)".
      *
      * Wands transformed in this way can be compared for equality as follows: an initial
      * syntactic comparison can be used to check if the wands match structurally, a subsequent
@@ -215,6 +215,12 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
           val variables = renameDecls(quant.variables, bindings)
 
           (quant.withVariables(variables), context.updateContext(extendBindings(context.c, quant.variables)))
+        case (let: Let, context) =>
+          val oldVars = Seq(let.variable)
+          val bindings = extendBindings(context.c, oldVars)
+          val variables = renameDecls(oldVars, bindings)
+          (Let(variables.head, let.exp, let.body)(let.pos, let.info, let.errT),
+            context.updateContext(extendBindings(context.c, oldVars)))
 
         case (lv: LocalVar, context) =>
           context.c.get(lv.name) match {
diff --git a/src/test/resources/all/issues/silver/0586.vpr b/src/test/resources/all/issues/silver/0586.vpr
new file mode 100644
index 000000000..441bdeaba
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0586.vpr
@@ -0,0 +1,17 @@
+field val: Int
+
+define NodeSeg(n) (
+    (let x == (0) in acc(n.val))
+)
+
+method test1(head: Ref)
+{
+	package (NodeSeg(head)) --* true
+	exhale (NodeSeg(head)) --* true
+}
+
+method test2(head: Ref)
+{
+	package (let x == (0) in acc(head.val)) --* true
+	exhale  (let x == (0) in acc(head.val)) --* true
+}
\ No newline at end of file

From 4336024487a192dae6c5470253a322b0f9454778 Mon Sep 17 00:00:00 2001
From: David Ewert <dewert10@gmail.com>
Date: Tue, 7 Jun 2022 10:41:26 -0700
Subject: [PATCH 2/2] Added intentionally failing test

---
 src/test/resources/all/issues/silver/0586.vpr | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/test/resources/all/issues/silver/0586.vpr b/src/test/resources/all/issues/silver/0586.vpr
index 441bdeaba..0f7cb7f9f 100644
--- a/src/test/resources/all/issues/silver/0586.vpr
+++ b/src/test/resources/all/issues/silver/0586.vpr
@@ -12,6 +12,13 @@ method test1(head: Ref)
 
 method test2(head: Ref)
 {
-	package (let x == (0) in acc(head.val)) --* true
-	exhale  (let x == (0) in acc(head.val)) --* true
+	package (let x == (head) in acc(x.val)) --* true
+	exhale  (let y == (head) in acc(y.val)) --* true
+}
+
+method test3(head: Ref) {
+  package (let x == (head) in let y == (0) in acc(x.val)) --* true
+  //:: ExpectedOutput(exhale.failed:wand.not.found)
+  exhale  (let y == (0) in let x == (head) in acc(x.val)) --* true
+  /* Current wand lookup algorithm is too syntactical/structural */
 }
\ No newline at end of file