Fix multiple apply of magic wands with quantified expressions

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -316,7 +316,7 @@ class TermToSMTLib2Converter
       parens(text("let") <+> parens(docBindings) <+> render(body))
 
     case MagicWandSnapshot(mwsf) => render(mwsf)
-    case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+    case MWSFApply(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
 
     case _: MagicWandChunkTerm
        | _: Quantification =>

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -445,7 +445,7 @@ class TermToZ3APIConverter
       case Let(bindings, body) =>
         convert(body.replace(bindings))
 
-      case MWSFLookup(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+      case MWSFApply(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
 
       case _: MagicWandChunkTerm
          | _: Quantification =>

src/main/scala/rules/Evaluator.scala

@@ -715,7 +715,7 @@ object evaluator extends EvaluationRules {
           if (pos.end.isEmpty) {
             fallbackName
           } else {
-            val file = pos.file.toString()
+            val file = pos.file.getFileName.toString
             val end = pos.end.get
             s"$file@${pos.start.line}@${pos.start.column}@${end.line}@${end.column}"
           }

src/main/scala/state/Chunks.scala

@@ -131,7 +131,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
                                     hints: Seq[Term] = Nil)
     extends QuantifiedBasicChunk {
 
-  require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.Snap, s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
+  require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.Snap, s"Quantified magic wand chunk values must be of sort Snap ($wsf), but found ${wsf.sort}")
   require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}")
 
   override val resourceID = MagicWandID

src/main/scala/state/Identifiers.scala

@@ -18,6 +18,12 @@ sealed trait Identifier {
     withSuffix(Identifier.defaultSeparator, suffix)
 
   def withSuffix(separator: String, suffix: String): SuffixedIdentifier
+
+  override def equals(obj: Any): Boolean =
+    obj match {
+      case that: Identifier => this.toString == that.toString
+      case _ => false
+    }
 }
 
 /* TODO: Remove object Identifier, make concrete identifiers' constructors private, and force all

src/main/scala/state/Terms.scala

@@ -2315,15 +2315,6 @@ class MagicWandSnapshot(val mwsf: Term) extends Term with ConditionalFlyweight[T
   override lazy val toString = s"wandSnap($mwsf)"
 
   override val equalityDefiningMembers: Term = mwsf
-
-  /**
-   * Apply the given snapshot of the left-hand side to the magic wand map to get the snapshot of the right-hand side
-   * which includes the values of the left-hand side.
-   *
-   * @param snapLhs The snapshot of the left-hand side that should be applied to the magic wand map.
-   * @return The snapshot of the right-hand side that preserves the values of the left-hand side.
-   */
-  def applyToMWSF(snapLhs: Term): Term = MWSFLookup(mwsf, snapLhs)
 }
 
 object MagicWandSnapshot extends PreciseCondFlyweightFactory[Term, MagicWandSnapshot]  {
@@ -2339,24 +2330,24 @@ object MagicWandSnapshot extends PreciseCondFlyweightFactory[Term, MagicWandSnap
  * @param mwsf Term of sort [[sorts.MagicWandSnapFunction]]. Function from `Snap` to `Snap`.
  * @param snap Term of sort [[sorts.Snap]] to which the MWSF is applied to. It represents the values of the wand's LHS.
  */
-class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFLookup] {
+class MWSFApply(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFApply] {
   val sort: Sort = sorts.Snap
   override def p0: Term = mwsf
   override def p1: Term = snap
   override lazy val toString = s"$mwsf[$snap]"
 }
 
-object MWSFLookup extends PreciseCondFlyweightFactory[(Term, Term), MWSFLookup] {
-  override def apply(pair: (Term, Term)): MWSFLookup = {
+object MWSFApply extends PreciseCondFlyweightFactory[(Term, Term), MWSFApply] {
+  override def apply(pair: (Term, Term)): MWSFApply = {
     val (mwsf, snap) = pair
     utils.assertSort(mwsf, "mwsf", sorts.MagicWandSnapFunction)
     utils.assertSort(snap, "snap", sorts.Snap)
     createIfNonExistent(pair)
   }
 
-  /** Create an instance of [[viper.silicon.state.terms.MWSFLookup]]. */
-  override def actualCreate(args: (Term, Term)): MWSFLookup =
-    new MWSFLookup(args._1, args._2)
+  /** Create an instance of [[viper.silicon.state.terms.MWSFApply]]. */
+  override def actualCreate(args: (Term, Term)): MWSFApply =
+    new MWSFApply(args._1, args._2)
 }
 
 class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] {

src/main/scala/state/Utils.scala

@@ -91,7 +91,7 @@ package object utils {
     case PredicatePermLookup(_, pm, args) => Seq(pm) ++ args
     case FieldTrigger(_, fvf, at) => fvf :: at :: Nil
     case PredicateTrigger(_, psf, args) => psf +: args
-
+    case MagicWandSnapshot(mwsf) => mwsf :: Nil
   }
 
   /** @see [[viper.silver.ast.utility.Simplifier.simplify]] */
@@ -197,7 +197,7 @@ package object utils {
       case MapDomain(t) => MapDomain(go(t))
       case MapRange(t) => MapRange(go(t))
       case MagicWandSnapshot(t) => MagicWandSnapshot(go(t))
-      case MWSFLookup(t0, t1) => MWSFLookup(go(t0), go(t1))
+      case MWSFApply(t0, t1) => MWSFApply(go(t0), go(t1))
       case Combine(t0, t1) => Combine(go(t0), go(t1))
       case First(t) => First(go(t))
       case Second(t) => Second(go(t))