From c9832ebd495a1e17d6e249ad4ee43ec8b6f1a9a7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Oct 2024 15:55:16 +0200
Subject: [PATCH] Fixing issue #862

---
 silver                               |  2 +-
 src/main/scala/rules/Evaluator.scala |  2 +-
 src/main/scala/state/State.scala     | 10 ++++++++--
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/silver b/silver
index 10b1b26a..f4a8d5a7 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 10b1b26a20957e5f000bf1bbcd4017145148afd7
+Subproject commit f4a8d5a73e9a823db4247d9d94004ec1133704d7
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 94300224..0570c926 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -1678,7 +1678,7 @@ object evaluator extends EvaluationRules {
           Option.when(withExp)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._2.get)), ast.EqCmp(joinExp.get, entry.data._2.get)())())))
 
 
-        var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) =>sAcc.merge(entry.s))
+        var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s))
         sJoined = sJoined.copy(functionRecorder = sJoined.functionRecorder.recordPathSymbol(joinSymbol))
 
         joinDefEqs foreach { case (t, exp, expNew) => v.decider.assume(t, exp, expNew)}
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 25f9e5fd..141adc9c 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -196,7 +196,7 @@ object State {
                      triggerExp2,
                      `partiallyConsumedHeap1`,
                      `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`,
-                     `reserveHeaps1`, `reserveCfgs1`, `conservedPcs1`, `recordPcs1`, `exhaleExt1`,
+                     `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
                      ssCache2, `hackIssue387DisablePermissionConsumption1`,
                      `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`,
                      `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
@@ -214,6 +214,11 @@ object State {
             val ssCache3 = ssCache1 ++ ssCache2
             val moreCompleteExhale3 = moreCompleteExhale || moreCompleteExhale2
 
+            assert(conservedPcs1.length == conservedPcs2.length)
+            val conservedPcs3 = conservedPcs1
+              .zip(conservedPcs1)
+              .map({ case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct })
+
             s1.copy(functionRecorder = functionRecorder3,
                     possibleTriggers = possibleTriggers3,
                     triggerExp = triggerExp3,
@@ -222,7 +227,8 @@ object State {
                     ssCache = ssCache3,
                     smCache = smCache3,
                     pmCache = pmCache3,
-                    moreCompleteExhale = moreCompleteExhale3)
+                    moreCompleteExhale = moreCompleteExhale3,
+                    conservedPcs = conservedPcs3)
 
           case _ =>
             val err = new StringBuilder()