From 448775ec40c6413811f6c3ac1095e22bd227f7e6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 2 Dec 2024 15:18:34 +0100 Subject: [PATCH] Fixed incorrect merge where wrong state is forwarded (#881) --- src/main/scala/rules/MoreCompleteExhaleSupporter.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index f908c28f..4472c0fb 100644 --- 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))) } } }