Fixed incorrect merge where wrong state is forwarded

viperproject · Dec 2, 2024 · 6cd6ef1 · 6cd6ef1
1 parent 761d4dd
commit 6cd6ef1
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -406,13 +406,13 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         })
         } else {
           if (!moreNeeded) {
-            Q(s, newHeap, None, v)
+            Q(s0, newHeap, None, v)
           } else {
             v.decider.assert(pNeeded === NoPerm) {
               case true =>
-                Q(s, newHeap, None, v)
+                Q(s0, newHeap, None, v)
               case false =>
-                createFailure(ve, v, s, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT)))
+                createFailure(ve, v, s0, pNeeded === NoPerm, pNeededExp.map(pn => ast.EqCmp(pn, ast.NoPerm()())(pn.pos, pn.info, pn.errT)))
             }
           }
         }