Merge branch 'master' into meilers_assert_read_only

viperproject · Dec 2, 2024 · b81afe6 · b81afe6
2 parents e6f4a2f + 448775e
commit b81afe6
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
@@ -407,13 +407,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)))
             }
           }
         }