Simplify havoc

viperproject · May 17, 2024 · e669d26 · e669d26
1 parent f306ed7
commit e669d26
Showing 1 changed file with 2 additions and 5 deletions.
diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala
@@ -183,12 +183,9 @@ object havocSupporter extends SymbolicExecutionRules {
 
     val newChunks = relevantChunks.map {
       case ch: MagicWandChunk =>
-        val havockedSnap = freshSnap(sorts.Snap, v)
-        val abstractLhs = freshSnap(sorts.Snap, v)
+        val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
         val cond = replacementCond(lhs, ch.args, condInfo)
-
-        // Define a new `MagicWandSnapshot` that checks the havoc condition when being applied
-        val magicWandSnapshot = magicWandSupporter.createMagicWandSnapshot(abstractLhs, Ite(cond, havockedSnap, MWSFLookup(ch.snap.mwsf, abstractLhs)), v)
+        val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf))
         ch.withSnap(magicWandSnapshot)
 
       case ch =>