From 564d281acbded9e4c0106f5291e76851ac4ea551 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Tue, 6 Jul 2021 13:06:50 +0200
Subject: [PATCH 01/58] change config flags

---
 src/main/scala/Config.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index df2378ded..7c09a25bd 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -205,7 +205,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val timeout: ScallopOption[Int] = opt[Int]("timeout",
     descr = ( "Time out after approx. n seconds. The timeout is for the whole verification, "
             + "not per method or proof obligation (default: 0, i.e. no timeout)."),
-    default = Some(0),
+    default = Some(180),
     noshort = true
   )
 
@@ -455,7 +455,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val enableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
     descr = "Enable a more complete exhale version.",
-    default = Some(false),
+    default = Some(true),
     noshort = true
   )
 
@@ -468,7 +468,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
     descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
              + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()}"),
-    default = Some(Runtime.getRuntime.availableProcessors()),
+    default = Some(1),
     noshort = true
   )
 

From f003b7c6911fabeb726a997f3b093602e6e04c92 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:12:14 +0200
Subject: [PATCH 02/58] add path condition aware merge

---
 src/main/scala/state/State.scala | 217 ++++++++++++++++++++++++++++++-
 1 file changed, 216 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 51d8d0e62..d8f825049 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -11,8 +11,9 @@ import viper.silver.cfg.silver.SilverCfg
 import viper.silicon.common.Mergeable
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider.RecordedPathConditions
+import viper.silicon.interfaces.state.{Chunk, GeneralChunk}
 import viper.silicon.state.State.OldHeaps
-import viper.silicon.state.terms.{Term, Var}
+import viper.silicon.state.terms.{And, Ite, NoPerm, Term, Var}
 import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder}
 import viper.silicon.{Map, Stack}
 
@@ -198,6 +199,220 @@ object State {
     }
   }
 
+  private def generateStateMismatchErrorMessage(s1: State, s2: State): Nothing = {
+    val err = new StringBuilder()
+    for (ix <- 0 until s1.productArity) yield {
+      val e1 = s1.productElement(ix)
+      val e2 = s2.productElement(ix)
+      if (e1 != e2) {
+        err ++= s"\n\tField index ${s1.productElementName(ix)} not equal"
+        err ++= s"\n\t\t state1: $e1"
+        err ++= s"\n\t\t state2: $e2"
+
+      }
+    }
+    sys.error(s"State merging failed: unexpected mismatch between symbolic states: $err")
+  }
+
+  // Merges two maps based on fOnce, if entry only exists in one map,
+  // and fTwice if entry exists in both maps.
+  private def mergeMaps[K, V, D](map1: Map[K, V], data1: D, map2: Map[K, V], data2: D)
+                                (fOnce: (V, D) => Option[V])
+                                (fTwice: (V, D, V, D) => Option[V])
+  : Map[K, V] = {
+
+    map1.flatMap({ case (k, v1) =>
+      (map2.get(k) match {
+        case Some(v2) => fTwice(v1, data1, v2, data2)
+        case None => fOnce(v1, data1)
+      }).map(v => (k, v))
+    }) ++ map2.flatMap({ case (k, v2) =>
+      (map1.get(k) match {
+        case Some(_) => None // Already considered in first case: Some(fTwice(v1, c1, v2, c2))
+        case None => fOnce(v2, data2)
+      }).map(v => (k, v))
+    })
+  }
+
+
+  private def conditionalizeChunks(h: Iterable[Chunk], cond: Term): Iterable[Chunk] = {
+    h map (c => {
+      c match {
+        case c: GeneralChunk =>
+          c.withPerm(Ite(cond, c.perm, NoPerm()))
+        case _ => sys.error("Chunk type not conditionalizable.")
+      }
+    })
+  }
+
+  private def conditionalizeHeap(h: Heap, cond: Term): Heap = {
+    Heap(conditionalizeChunks(h.values, cond))
+  }
+
+  def mergeHeap(h1: Heap, cond1: Term, h2: Heap, cond2: Term): Heap = {
+    val (unconditionalHeapChunks, h1HeapChunksToConditionalize) = h1.values.partition(c1 => h2.values.exists(_ == c1))
+    val h2HeapChunksToConditionalize = h2.values.filter(c2 => !unconditionalHeapChunks.exists(_ == c2))
+    val h1ConditionalizedHeapChunks = conditionalizeChunks(h1HeapChunksToConditionalize, cond1)
+    val h2ConditionalizedHeapChunks = conditionalizeChunks(h2HeapChunksToConditionalize, cond2)
+    Heap(unconditionalHeapChunks) + Heap(h1ConditionalizedHeapChunks) + Heap(h2ConditionalizedHeapChunks)
+  }
+
+  def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = {
+
+    println("MERGE")
+
+    s1 match {
+      /* Decompose state s1 */
+      case State(g1, h1, oldHeaps1,
+      parallelizeBranches1,
+      recordVisited1, visited1,
+      methodCfg1, invariantContexts1,
+      constrainableARPs1,
+      quantifiedVariables1,
+      retrying1,
+      underJoin1,
+      functionRecorder1,
+      conservingSnapshotGeneration1,
+      recordPossibleTriggers1, possibleTriggers1,
+      triggerExp1,
+      partiallyConsumedHeap1,
+      permissionScalingFactor1,
+      reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
+      applyHeuristics1, heuristicsDepth1, triggerAction1,
+      ssCache1, hackIssue387DisablePermissionConsumption1,
+      qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
+      predicateSnapMap1, predicateFormalVarMap1, hack) =>
+
+        /* Decompose state s2: most values must match those of s1 */
+        s2 match {
+          case State(g2, h2, oldHeaps2,
+          `parallelizeBranches1`,
+          `recordVisited1`, `visited1`,
+          `methodCfg1`, invariantContexts2,
+          constrainableARPs2,
+          `quantifiedVariables1`,
+          `retrying1`,
+          `underJoin1`,
+          functionRecorder2,
+          `conservingSnapshotGeneration1`,
+          `recordPossibleTriggers1`, possibleTriggers2,
+          triggerExp2,
+          partiallyConsumedHeap2,
+          `permissionScalingFactor1`,
+          reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
+          `applyHeuristics1`, `heuristicsDepth1`, `triggerAction1`,
+          ssCache2, `hackIssue387DisablePermissionConsumption1`,
+          `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, smDomainNeeded2,
+          `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`) =>
+
+            val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
+            val triggerExp3 = triggerExp1 && triggerExp2
+            val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2
+            val constrainableARPs3 = constrainableARPs1 ++ constrainableARPs2
+
+            val smDomainNeeded3 = smDomainNeeded1 || smDomainNeeded2 // TODO: Use AND or OR to merge?
+
+            val conditions1 = And(pc1.branchConditions)
+            val conditions2 = And(pc2.branchConditions)
+
+            //var mergePcs: Seq[Term] = Vector.empty
+
+            val mergeStore = (g1: Store, g2: Store) => {
+              Store(mergeMaps(g1.values, conditions1, g2.values, conditions2)
+              ((_, _) => {
+                // If store entry is only on one branch, we can safely discard it.
+                None
+              })
+              ((v1, cond1, v2, cond2) => {
+                if (v1 == v2) {
+                  // Trivial: Both entries are the same.
+                  Some(v1)
+                } else {
+                  assert(v1.sort == v2.sort)
+                  // TODO: Is this faster?
+                  //val t = verifier.decider.fresh(v1.sort)
+                  //mergePcs :+= Implies(cond1, Equals(t, v1))
+                  //mergePcs :+= Implies(cond2, Equals(t, v2))
+                  //Some(t)
+                  Some(Ite(cond1, v1, v2))
+                }
+              }))
+            }
+
+            val g3 = mergeStore(g1, g2)
+
+            val h3 = mergeHeap(h1, conditions1, h2, conditions2)
+
+            val partiallyConsumedHeap3 = (partiallyConsumedHeap1, partiallyConsumedHeap2) match {
+              case (None, None) => None
+              case (Some(pch1), None) => Some(conditionalizeHeap(pch1, conditions1))
+              case (None, Some(pch2)) => Some(conditionalizeHeap(pch2, conditions2))
+              case (Some(pch1), Some(pch2)) => Some(mergeHeap(
+                pch1, conditions1,
+                pch2, conditions2
+              ))
+            }
+
+            val oldHeaps3 = Map.from(mergeMaps(oldHeaps1, conditions1, oldHeaps2, conditions2)
+            ((_, _) => {
+              None
+            })
+            ((heap1, cond1, heap2, cond2) => {
+              Some(mergeHeap(heap1, cond1, heap2, cond2))
+            }))
+
+            //verifier.decider.assume(mergePcs)
+
+            // TODO: InvariantContexts should most likely be the same
+            assert(invariantContexts1.length == invariantContexts2.length)
+            val invariantContexts3 = invariantContexts1
+              .zip(invariantContexts2)
+              .map({case (h1, h2) => mergeHeap(h1, conditions1, h2, conditions2)})
+
+            // TODO: Workout situations in which reserve heaps differ
+            assert(reserveHeaps1.length == reserveHeaps2.length)
+            val reserveHeaps3 = reserveHeaps1
+              .zip(reserveHeaps2)
+              .map({case (h1, h2) => mergeHeap(h1, conditions1, h2, conditions2)})
+
+
+            assert(conservedPcs1.length == conservedPcs2.length)
+            val conservedPcs3 = conservedPcs1
+              .zip(conservedPcs1)
+              .map({case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct})
+
+            //assert(conservedPcs1 == conservedPcs2)
+            //val conservedPcs3 = conservedPcs1
+
+
+            val s3 = s1.copy(functionRecorder = functionRecorder3,
+              possibleTriggers = possibleTriggers3,
+              triggerExp = triggerExp3,
+              constrainableARPs = constrainableARPs3,
+              // TODO: Merge caches.
+              ssCache = Map.empty,
+              smCache = SnapshotMapCache.empty,
+              pmCache = Map.empty,
+              g = g3,
+              h = h3,
+              oldHeaps = oldHeaps3,
+              partiallyConsumedHeap = partiallyConsumedHeap3,
+              smDomainNeeded = smDomainNeeded3,
+              invariantContexts = invariantContexts3,
+              reserveHeaps = reserveHeaps3,
+              conservedPcs = conservedPcs3
+            )
+
+            s3
+
+            //val s4 = verifier.stateConsolidator.consolidate(s3, verifier)
+            //s4
+
+          case _ => generateStateMismatchErrorMessage(s1, s2)
+        }
+    }
+  }
+
   def preserveAfterLocalEvaluation(pre: State, post: State): State = {
     pre.copy(functionRecorder = post.functionRecorder,
              possibleTriggers = post.possibleTriggers,

From 8c81908ac7871f67300d6affca48aba154437655 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:13:52 +0200
Subject: [PATCH 03/58] add moreJoins config flag

---
 src/main/scala/Config.scala | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 69c2d95d5..850237574 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -453,6 +453,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
+    descr = "Enable more joins using a more complete implementation of state merging.",
+    default = Some(false),
+    noshort = true
+  )
+
   val stateConsolidationMode: ScallopOption[StateConsolidationMode] = opt[StateConsolidationMode]("stateConsolidationMode",
     descr = s"One of the following modes:\n${StateConsolidationMode.helpText}",
     default = Some(StateConsolidationMode.Default),

From efcd20d290cb85ea2c240926b24223df8bfe4b0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:18:43 +0200
Subject: [PATCH 04/58] modify joiner to optionally not reset the state

---
 src/main/scala/rules/Joiner.scala | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index ef92fa6c1..96170d08d 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -16,7 +16,7 @@ import viper.silicon.verifier.Verifier
 case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions)
 
 trait JoiningRules extends SymbolicExecutionRules {
-  def join[D, JD](s: State, v: Verifier)
+  def join[D, JD](s: State, v: Verifier, resetState: Boolean = true)
                  (block: (State, Verifier, (State, D, Verifier) => VerificationResult) => VerificationResult)
                  (merge: Seq[JoinDataEntry[D]] => (State, JD))
                  (Q: (State, JD, Verifier) => VerificationResult)
@@ -24,7 +24,7 @@ trait JoiningRules extends SymbolicExecutionRules {
 }
 
 object joiner extends JoiningRules {
-  def join[D, JD](s: State, v: Verifier)
+  def join[D, JD](s: State, v: Verifier, resetState: Boolean = true)
                  (block: (State, Verifier, (State, D, Verifier) => VerificationResult) => VerificationResult)
                  (merge: Seq[JoinDataEntry[D]] => (State, JD))
                  (Q: (State, JD, Verifier) => VerificationResult)
@@ -45,10 +45,16 @@ object joiner extends JoiningRules {
          * affected by the evaluation - such as the store (by let-bindings) or the heap (by
          * state consolidations) to their initial values.
          */
-        val s4 = s3.copy(g = s1.g,
-                         h = s1.h,
-                         oldHeaps = s1.oldHeaps,
-                         underJoin = s1.underJoin)
+        val s4 =
+          if (resetState) {
+            s3.copy(g = s1.g,
+                    h = s1.h,
+                    oldHeaps = s1.oldHeaps,
+                    underJoin = s1.underJoin,
+                    // TODO: Evaluation should not affect partiallyConsumedHeap, probably
+                    ssCache = s1.ssCache,
+                    partiallyConsumedHeap = s1.partiallyConsumedHeap)
+          } else s3
         entries :+= JoinDataEntry(s4, data, v2.decider.pcs.after(preMark))
         Success()
       })

From 3e62dccc64781490b6fc2a150812a38c8a347a4b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:25:17 +0200
Subject: [PATCH 05/58] add support for path condition aware merge in joiner

---
 src/main/scala/rules/Joiner.scala | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index 96170d08d..81b4d0f45 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -13,7 +13,13 @@ import viper.silicon.logger.records.structural.JoiningRecord
 import viper.silicon.state.State
 import viper.silicon.verifier.Verifier
 
-case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions)
+case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions) {
+  // Instead of merging states, we can directly merge JoinDataEntries to obtain new States.
+  // This gives us more information about the path conditions.
+  def pathConditionAwareMerge(other: JoinDataEntry[D]): State = {
+    State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
+  }
+}
 
 trait JoiningRules extends SymbolicExecutionRules {
   def join[D, JD](s: State, v: Verifier, resetState: Boolean = true)

From 712eb2a8b28c45e810112c5dbd94d0f63f67c05f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:33:37 +0200
Subject: [PATCH 06/58] add moreJoins support to consumer

---
 src/main/scala/rules/Consumer.scala | 75 +++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index 0ad29ba90..064b8a126 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -184,6 +184,43 @@ object consumer extends ConsumptionRules {
       v.logger.debug("hR = " + s.reserveHeaps.map(v.stateFormatter.format).mkString("", ",\n     ", ""))
 
     val consumed = a match {
+      case imp @ ast.Implies(e0, a0) if !a.isPure && Verifier.config.moreJoins() =>
+        val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
+        val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord)
+
+        evaluator.eval(s, e0, pve, v)((s1, t0, v1) =>
+          joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) =>
+            branch(s1, t0, v1)(
+              (s2, v2) => consumeR(s2, h, a0, pve, v2)((s3, h1, t1, v3) => {
+                SymbExLogger.currentLog().closeScope(uidImplies)
+                QB(s3, (h1, t1), v3)
+              }),
+              (s2, v2) => {
+                SymbExLogger.currentLog().closeScope(uidImplies)
+                QB(s2, (h, Unit), v2)
+              })
+          )(entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                (entry.s, entry.data)
+              case Seq(entry1, entry2) => // Both branches are alive
+                val mergedData = (
+                  State.mergeHeap(
+                    entry1.data._1, And(entry1.pathConditions.branchConditions),
+                    entry2.data._1, And(entry2.pathConditions.branchConditions),
+                  ),
+                  // Asume that entry1.pcs is inverse of entry2.pcs
+                  Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
+                )
+                (entry1.pathConditionAwareMerge(entry2), mergedData)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")}
+            s2
+          })((s4, data, v4) => {
+            Q(s4, data._1, data._2, v4)
+          })
+        )
+
       case imp @ ast.Implies(e0, a0) if !a.isPure =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
         val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord)
@@ -199,6 +236,44 @@ object consumer extends ConsumptionRules {
               Q(s2, h, Unit, v2)
             }))
 
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && Verifier.config.moreJoins() =>
+        val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
+        val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)
+
+        eval(s, e0, pve, v)((s1, t0, v1) =>
+          joiner.join[(Heap, Term), (Heap, Term)](s1, v1)((s1, v1, QB) => {
+            branch(s1, t0, v1)(
+              (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => {
+                SymbExLogger.currentLog().closeScope(uidCondExp)
+                QB(s3, (h1, t1), v3)
+              }),
+              (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => {
+                SymbExLogger.currentLog().closeScope(uidCondExp)
+                QB(s3, (h1, t1), v3)
+              }))
+          })(entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                (entry.s, entry.data)
+              case Seq(entry1, entry2) => // Both branches are alive
+                val mergedData = (
+                  State.mergeHeap(
+                    entry1.data._1, And(entry1.pathConditions.branchConditions),
+                    entry2.data._1, And(entry2.pathConditions.branchConditions),
+                  ),
+                  // Asume that entry1.pcs is inverse of entry2.pcs
+                  Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
+                )
+                (entry1.pathConditionAwareMerge(entry2), mergedData)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")}
+            s2
+          })((s4, data, v4) => {
+            Q(s4, data._1, data._2, v4)
+          })
+        )
+
+
       case ite @ ast.CondExp(e0, a1, a2) if !a.isPure =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
         val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)

From 7481bc052dc7c1f517ea727c800153001a31279d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 11:44:51 +0200
Subject: [PATCH 07/58] add moreJoins support to producer

---
 src/main/scala/rules/Consumer.scala |  2 +-
 src/main/scala/rules/Producer.scala | 59 +++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index 064b8a126..7bb1c98e4 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -241,7 +241,7 @@ object consumer extends ConsumptionRules {
         val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)
 
         eval(s, e0, pve, v)((s1, t0, v1) =>
-          joiner.join[(Heap, Term), (Heap, Term)](s1, v1)((s1, v1, QB) => {
+          joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) => {
             branch(s1, t0, v1)(
               (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => {
                 SymbExLogger.currentLog().closeScope(uidCondExp)
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 1defb2b3e..8432d935d 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -205,6 +205,38 @@ object producer extends ProductionRules {
       continuation(if (state.exhaleExt) state.copy(reserveHeaps = state.h +: state.reserveHeaps.drop(1)) else state, verifier)
 
     val produced = a match {
+      case imp @ ast.Implies(e0, a0) if !a.isPure && Verifier.config.moreJoins() =>
+        val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "produce")
+        val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord)
+
+        eval(s, e0, pve, v)((s1, t0, v1) =>
+          joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
+            branch(s1, t0, v1)(
+              (s2, v2) => produceR(s2, sf, a0, pve, v2)((s3, v3) => {
+                SymbExLogger.currentLog().closeScope(uidImplies)
+                QB(s3, null, v3)
+              }),
+              (s2, v2) => {
+                v2.decider.assume(sf(sorts.Snap, v2) === Unit)
+                /* TODO: Avoid creating a fresh var (by invoking) `sf` that is not used
+                 * otherwise. In order words, only make this assumption if `sf` has
+                 * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`.
+                 */
+                SymbExLogger.currentLog().closeScope(uidImplies)
+                QB(s2, null, v2)
+              })
+          )(entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                entry.s
+              case Seq(entry1, entry2) => // Both branches are alive
+                entry1.pathConditionAwareMerge(entry2)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")}
+            (s2, null)
+          })((s, _, v) => Q(s, v))
+        )
+
       case imp @ ast.Implies(e0, a0) if !a.isPure =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "produce")
         val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord)
@@ -225,6 +257,33 @@ object producer extends ProductionRules {
                 Q(s2, v2)
             }))
 
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && Verifier.config.moreJoins() =>
+        val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "produce")
+        val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)
+
+        eval(s, e0, pve, v)((s1, t0, v1) =>
+          joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
+            branch(s1, t0, v1)(
+              (s2, v2) => produceR(s2, sf, a1, pve, v2)((s3, v3) => {
+                SymbExLogger.currentLog().closeScope(uidCondExp)
+                QB(s3, null, v3)
+              }),
+              (s2, v2) => produceR(s2, sf, a2, pve, v2)((s3, v3) => {
+                SymbExLogger.currentLog().closeScope(uidCondExp)
+                QB(s3, null, v3)
+              }))
+          )(entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                entry.s
+              case Seq(entry1, entry2) => // Both branches are alive
+                entry1.pathConditionAwareMerge(entry2)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")}
+            (s2, null)
+          })((s, _, v) => Q(s, v))
+        )
+
       case ite @ ast.CondExp(e0, a1, a2) if !a.isPure =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "produce")
         val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)

From 02abed7567ab2aee5ed20603c98b097f67823a64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 15:17:46 +0200
Subject: [PATCH 08/58] change config flags

---
 src/main/scala/Config.scala         |  20 ++++-
 src/main/scala/rules/Executor.scala | 126 ++++++++++++++++++++--------
 src/main/scala/state/State.scala    |   9 +-
 3 files changed, 117 insertions(+), 38 deletions(-)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 850237574..8ac2e74d3 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -199,7 +199,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val timeout: ScallopOption[Int] = opt[Int]("timeout",
     descr = ( "Time out after approx. n seconds. The timeout is for the whole verification, "
             + "not per method or proof obligation (default: 0, i.e. no timeout)."),
-    default = Some(0),
+    default = Some(180),
     noshort = true
   )
 
@@ -449,16 +449,30 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val enableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
     descr = "Enable a more complete exhale version.",
-    default = Some(false),
+    default = Some(true),
     noshort = true
   )
 
   val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
     descr = "Enable more joins using a more complete implementation of state merging.",
-    default = Some(false),
+    default = Some(true),
+    noshort = true
+  )
+
+  val disableCaches: ScallopOption[Boolean] = opt[Boolean]("disableCaches",
+    descr = "Disables various caches within the state.",
+    default = Some(true),
     noshort = true
   )
 
+  def mapCache[A](opt: Option[A]): Option[A] = {
+    opt match {
+      case None => None
+      case Some(_) if disableCaches() => None
+      case _ => opt
+    }
+  }
+
   val stateConsolidationMode: ScallopOption[StateConsolidationMode] = opt[StateConsolidationMode]("stateConsolidationMode",
     descr = s"One of the following modes:\n${StateConsolidationMode.helpText}",
     default = Some(StateConsolidationMode.Default),
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 80130b110..d4011d6ef 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -25,6 +25,7 @@ import viper.silicon.state.terms.perms.IsNonNegative
 import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
+import viper.silver.cfg.{ConditionalEdge, StatementBlock}
 
 trait ExecutionRules extends SymbolicExecutionRules {
   def exec(s: State,
@@ -64,29 +65,37 @@ object executor extends ExecutionRules {
       }
     }
 
-    edge match {
-      case ce: cfg.ConditionalEdge[ast.Stmt, ast.Exp] =>
-        val condEdgeRecord = new ConditionalEdgeRecord(ce.condition, s, v.decider.pcs)
-        val sepIdentifier = SymbExLogger.currentLog().openScope(condEdgeRecord)
+    s.joinPoints.headOption match {
+      case Some(joinPoint) if joinPoint == edge.target =>
+        // Join point reached, stop following edges.
         val s1 = handleOutEdge(s, edge, v)
-        eval(s1, ce.condition, IfFailed(ce.condition), v)((s2, tCond, v1) =>
-          /* Using branch(...) here ensures that the edge condition is recorded
-           * as a branch condition on the pathcondition stack.
-           */
-          brancher.branch(s2, tCond, v1)(
-            (s3, v3) =>
-              exec(s3, ce.target, ce.kind, v3)((s4, v4) => {
+        val s2 = s1.copy(joinPoints = s1.joinPoints.tail)
+        Q(s2, v)
+
+      case _ => edge match {
+        case ce: cfg.ConditionalEdge[ast.Stmt, ast.Exp] =>
+          val condEdgeRecord = new ConditionalEdgeRecord(ce.condition, s, v.decider.pcs)
+          val sepIdentifier = SymbExLogger.currentLog().openScope(condEdgeRecord)
+          val s1 = handleOutEdge(s, edge, v)
+          eval(s1, ce.condition, IfFailed(ce.condition), v)((s2, tCond, v1) =>
+            /* Using branch(...) here ensures that the edge condition is recorded
+             * as a branch condition on the pathcondition stack.
+             */
+            brancher.branch(s2, tCond, v1)(
+              (s3, v3) =>
+                exec(s3, ce.target, ce.kind, v3)((s4, v4) => {
+                  SymbExLogger.currentLog().closeScope(sepIdentifier)
+                  Q(s4, v4)
+                }),
+              (_, _)  => {
                 SymbExLogger.currentLog().closeScope(sepIdentifier)
-                Q(s4, v4)
-              }),
-            (_, _)  => {
-              SymbExLogger.currentLog().closeScope(sepIdentifier)
-              Success()
-            }))
-
-      case ue: cfg.UnconditionalEdge[ast.Stmt, ast.Exp] =>
-        val s1 = handleOutEdge(s, edge, v)
-        exec(s1, ue.target, ue.kind, v)(Q)
+                Success()
+              }))
+
+        case ue: cfg.UnconditionalEdge[ast.Stmt, ast.Exp] =>
+          val s1 = handleOutEdge(s, edge, v)
+          exec(s1, ue.target, ue.kind, v)(Q)
+      }
     }
   }
 
@@ -101,20 +110,71 @@ object executor extends ExecutionRules {
       Q(s, v)
     } else if (edges.length == 1) {
       follow(s, edges.head, v)(Q)
-    } else {
-      val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
-      val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
-        case (fatalResult: FatalResult, _) => fatalResult
-        case (_, (edge, edgeIndex)) => {
-          if (edgeIndex != 0) {
-            SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
-          }
-          SymbExLogger.currentLog().markReachable(uidBranchPoint)
-          follow(s, edge, v)(Q)
+    } else if (edges.length == 2) {
+      val edge1 = edges.head.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
+      val edge2 = edges.last.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
+
+      assert(edge1.source == edge2.source)
+      val branchPoint = edge1.source
+
+      s.methodCfg.joinPoints.get(branchPoint) match {
+        case Some(joinPoint) if
+          Verifier.config.moreJoins() &&
+          edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
+          edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
+          edge1.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]] &&
+          edge2.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]]
+        => {
+          // Here we assume that edge1.condition is the negation of edge2.condition.
+          assert((edge1.condition, edge2.condition) match {
+            case (exp1, ast.Not(exp2)) => exp1 == exp2
+            case (ast.Not(exp1), exp2) => exp1 == exp2
+            case _ => false
+          })
+
+          eval(s, edge1.condition, pvef(edge1.condition), v)((s1, t0, v1) =>
+            joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
+              val s3 = s2.copy(joinPoints = joinPoint +: s2.joinPoints)
+              brancher.branch(s3, t0, v2)(
+                // Follow until join point.
+                (s3, v3) => follow(s3, edge1, v3)((s, v) => QB(s, null, v)),
+                (s3, v3) => follow(s3, edge2, v3)((s, v) => QB(s, null, v))
+              )
+            })(entries => {
+              val s2 = entries match {
+                case Seq(entry) => // One branch is dead
+                  entry.s
+                case Seq(entry1, entry2) => // Both branches are alive
+                  entry1.pathConditionAwareMerge(entry2)
+                case _ =>
+                  sys.error(s"Unexpected join data entries: $entries")
+              }
+              (s2, null)
+            })((s4, _, v4) => {
+              // Continue after merging at join point.
+              exec(s4, joinPoint, s4.methodCfg.inEdges(joinPoint).head.kind, v4)(Q)
+            })
+          )
+
         }
+        case _ =>
+          val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
+          val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
+            case (fatalResult: FatalResult, _) => fatalResult
+            case (_, (edge, edgeIndex)) => {
+              if (edgeIndex != 0) {
+                SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
+              }
+              SymbExLogger.currentLog().markReachable(uidBranchPoint)
+              follow(s, edge, v)(Q)
+            }
+          }
+          SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
+          res
       }
-      SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
-      res
+
+    } else {
+      sys.error("At most two out edges expected.")
     }
   }
 
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index d8f825049..ddad81250 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -16,6 +16,7 @@ import viper.silicon.state.State.OldHeaps
 import viper.silicon.state.terms.{And, Ite, NoPerm, Term, Var}
 import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder}
 import viper.silicon.{Map, Stack}
+import viper.silver.cfg.silver.SilverCfg.SilverBlock
 
 final case class State(g: Store = Store(),
                        h: Heap = Heap(),
@@ -33,6 +34,7 @@ final case class State(g: Store = Store(),
                        quantifiedVariables: Stack[Var] = Nil,
                        retrying: Boolean = false,
                        underJoin: Boolean = false,
+                       joinPoints: Stack[SilverBlock] = Stack.empty,
                        functionRecorder: FunctionRecorder = NoopFunctionRecorder,
                        conservingSnapshotGeneration: Boolean = false,
                        recordPossibleTriggers: Boolean = false,
@@ -133,6 +135,7 @@ object State {
                  quantifiedVariables1,
                  retrying1,
                  underJoin1,
+                 joinPoints1,
                  functionRecorder1,
                  conservingSnapshotGeneration1,
                  recordPossibleTriggers1, possibleTriggers1,
@@ -155,6 +158,7 @@ object State {
                      `quantifiedVariables1`,
                      `retrying1`,
                      `underJoin1`,
+                     `joinPoints1`,
                      functionRecorder2,
                      `conservingSnapshotGeneration1`,
                      `recordPossibleTriggers1`, possibleTriggers2,
@@ -271,6 +275,7 @@ object State {
       quantifiedVariables1,
       retrying1,
       underJoin1,
+      joinPoints1,
       functionRecorder1,
       conservingSnapshotGeneration1,
       recordPossibleTriggers1, possibleTriggers1,
@@ -293,6 +298,7 @@ object State {
           `quantifiedVariables1`,
           `retrying1`,
           `underJoin1`,
+          `joinPoints1`,
           functionRecorder2,
           `conservingSnapshotGeneration1`,
           `recordPossibleTriggers1`, possibleTriggers2,
@@ -384,7 +390,6 @@ object State {
             //assert(conservedPcs1 == conservedPcs2)
             //val conservedPcs3 = conservedPcs1
 
-
             val s3 = s1.copy(functionRecorder = functionRecorder3,
               possibleTriggers = possibleTriggers3,
               triggerExp = triggerExp3,
@@ -400,7 +405,7 @@ object State {
               smDomainNeeded = smDomainNeeded3,
               invariantContexts = invariantContexts3,
               reserveHeaps = reserveHeaps3,
-              conservedPcs = conservedPcs3
+              conservedPcs = conservedPcs3,
             )
 
             s3

From cd9818f715e22ff51b71b9d9aef8bf0254c26684 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Fri, 9 Jul 2021 17:52:11 +0200
Subject: [PATCH 09/58] change flags

---
 src/main/scala/Config.scala | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index e7b292ac9..0565bd719 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -449,7 +449,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val disableCaches: ScallopOption[Boolean] = opt[Boolean]("disableCaches",
     descr = "Disables various caches in Silicon's state.",
-    default = Some(false),
+    default = Some(true),
     noshort = true
   )
 
@@ -470,20 +470,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val disableCaches: ScallopOption[Boolean] = opt[Boolean]("disableCaches",
-    descr = "Disables various caches within the state.",
-    default = Some(true),
-    noshort = true
-  )
-
-  def mapCache[A](opt: Option[A]): Option[A] = {
-    opt match {
-      case None => None
-      case Some(_) if disableCaches() => None
-      case _ => opt
-    }
-  }
-
   val stateConsolidationMode: ScallopOption[StateConsolidationMode] = opt[StateConsolidationMode]("stateConsolidationMode",
     descr = s"One of the following modes:\n${StateConsolidationMode.helpText}",
     default = Some(StateConsolidationMode.Default),
@@ -493,7 +479,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
     descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
              + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()}"),
-    default = Some(Runtime.getRuntime.availableProcessors()),
+    default = Some(1),
     noshort = true
   )
 

From f249db598f5081fdc0738d4c08dfe436e9a1e180 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 12 Jul 2021 15:59:34 +0200
Subject: [PATCH 10/58] remove println

---
 src/main/scala/state/State.scala | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index ddad81250..521847195 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -263,8 +263,6 @@ object State {
 
   def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = {
 
-    println("MERGE")
-
     s1 match {
       /* Decompose state s1 */
       case State(g1, h1, oldHeaps1,

From 8ae3dc29e562143b12887aae2910adf5e0ed0148 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Wed, 14 Jul 2021 09:55:40 +0200
Subject: [PATCH 11/58] bugfix to joiner

---
 src/main/scala/rules/Joiner.scala | 3 ++-
 src/main/scala/state/State.scala  | 7 +++++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index 81b4d0f45..f43e7541b 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -59,7 +59,8 @@ object joiner extends JoiningRules {
                     underJoin = s1.underJoin,
                     // TODO: Evaluation should not affect partiallyConsumedHeap, probably
                     ssCache = s1.ssCache,
-                    partiallyConsumedHeap = s1.partiallyConsumedHeap)
+                    partiallyConsumedHeap = s1.partiallyConsumedHeap,
+                    invariantContexts = s1.invariantContexts)
           } else s3
         entries :+= JoinDataEntry(s4, data, v2.decider.pcs.after(preMark))
         Success()
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 521847195..de7b73134 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -262,7 +262,7 @@ object State {
   }
 
   def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = {
-
+    println("Merge")
     s1 match {
       /* Decompose state s1 */
       case State(g1, h1, oldHeaps1,
@@ -411,7 +411,10 @@ object State {
             //val s4 = verifier.stateConsolidator.consolidate(s3, verifier)
             //s4
 
-          case _ => generateStateMismatchErrorMessage(s1, s2)
+          case _ => {
+            println("Error at new merge function:")
+            generateStateMismatchErrorMessage(s1, s2)
+          }
         }
     }
   }

From 52cd6798bfb1323710f37404a652eb47d4b5a249 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Wed, 14 Jul 2021 10:28:29 +0200
Subject: [PATCH 12/58] remove joinPoints from state

---
 src/main/scala/rules/Executor.scala | 39 ++++++++++++++---------------
 src/main/scala/state/State.scala    |  7 +-----
 2 files changed, 20 insertions(+), 26 deletions(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index d4011d6ef..c07aa1364 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -48,7 +48,7 @@ object executor extends ExecutionRules {
   import evaluator._
   import producer._
 
-  private def follow(s: State, edge: SilverEdge, v: Verifier)
+  private def follow(s: State, edge: SilverEdge, v: Verifier, joinPoint: Option[SilverBlock])
                     (Q: (State, Verifier) => VerificationResult)
                     : VerificationResult = {
 
@@ -65,12 +65,11 @@ object executor extends ExecutionRules {
       }
     }
 
-    s.joinPoints.headOption match {
-      case Some(joinPoint) if joinPoint == edge.target =>
+    joinPoint match {
+      case Some(jp) if jp == edge.target =>
         // Join point reached, stop following edges.
         val s1 = handleOutEdge(s, edge, v)
-        val s2 = s1.copy(joinPoints = s1.joinPoints.tail)
-        Q(s2, v)
+        Q(s1, v)
 
       case _ => edge match {
         case ce: cfg.ConditionalEdge[ast.Stmt, ast.Exp] =>
@@ -83,7 +82,7 @@ object executor extends ExecutionRules {
              */
             brancher.branch(s2, tCond, v1)(
               (s3, v3) =>
-                exec(s3, ce.target, ce.kind, v3)((s4, v4) => {
+                exec(s3, ce.target, ce.kind, v3, joinPoint)((s4, v4) => {
                   SymbExLogger.currentLog().closeScope(sepIdentifier)
                   Q(s4, v4)
                 }),
@@ -94,7 +93,7 @@ object executor extends ExecutionRules {
 
         case ue: cfg.UnconditionalEdge[ast.Stmt, ast.Exp] =>
           val s1 = handleOutEdge(s, edge, v)
-          exec(s1, ue.target, ue.kind, v)(Q)
+          exec(s1, ue.target, ue.kind, v, joinPoint)(Q)
       }
     }
   }
@@ -102,14 +101,15 @@ object executor extends ExecutionRules {
   private def follows(s: State,
                       edges: Seq[SilverEdge],
                       @unused pvef: ast.Exp => PartialVerificationError,
-                      v: Verifier)
+                      v: Verifier,
+                      joinPoint: Option[SilverBlock])
                      (Q: (State, Verifier) => VerificationResult)
                      : VerificationResult = {
 
     if (edges.isEmpty) {
       Q(s, v)
     } else if (edges.length == 1) {
-      follow(s, edges.head, v)(Q)
+      follow(s, edges.head, v, joinPoint)(Q)
     } else if (edges.length == 2) {
       val edge1 = edges.head.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
       val edge2 = edges.last.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
@@ -118,7 +118,7 @@ object executor extends ExecutionRules {
       val branchPoint = edge1.source
 
       s.methodCfg.joinPoints.get(branchPoint) match {
-        case Some(joinPoint) if
+        case Some(newJoinPoint) if
           Verifier.config.moreJoins() &&
           edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
           edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
@@ -134,11 +134,10 @@ object executor extends ExecutionRules {
 
           eval(s, edge1.condition, pvef(edge1.condition), v)((s1, t0, v1) =>
             joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
-              val s3 = s2.copy(joinPoints = joinPoint +: s2.joinPoints)
-              brancher.branch(s3, t0, v2)(
+              brancher.branch(s2, t0, v2)(
                 // Follow until join point.
-                (s3, v3) => follow(s3, edge1, v3)((s, v) => QB(s, null, v)),
-                (s3, v3) => follow(s3, edge2, v3)((s, v) => QB(s, null, v))
+                (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)),
+                (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint))((s, v) => QB(s, null, v))
               )
             })(entries => {
               val s2 = entries match {
@@ -152,7 +151,7 @@ object executor extends ExecutionRules {
               (s2, null)
             })((s4, _, v4) => {
               // Continue after merging at join point.
-              exec(s4, joinPoint, s4.methodCfg.inEdges(joinPoint).head.kind, v4)(Q)
+              exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint)(Q)
             })
           )
 
@@ -166,7 +165,7 @@ object executor extends ExecutionRules {
                 SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
               }
               SymbExLogger.currentLog().markReachable(uidBranchPoint)
-              follow(s, edge, v)(Q)
+              follow(s, edge, v, joinPoint)(Q)
             }
           }
           SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
@@ -182,17 +181,17 @@ object executor extends ExecutionRules {
           (Q: (State, Verifier) => VerificationResult)
           : VerificationResult = {
 
-    exec(s, graph.entry, cfg.Kind.Normal, v)(Q)
+    exec(s, graph.entry, cfg.Kind.Normal, v, None)(Q)
   }
 
-  def exec(s: State, block: SilverBlock, incomingEdgeKind: cfg.Kind.Value, v: Verifier)
+  def exec(s: State, block: SilverBlock, incomingEdgeKind: cfg.Kind.Value, v: Verifier, joinPoint: Option[SilverBlock])
           (Q: (State, Verifier) => VerificationResult)
           : VerificationResult = {
 
     block match {
       case cfg.StatementBlock(stmt) =>
         execs(s, stmt, v)((s1, v1) =>
-          follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1)(Q))
+          follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint)(Q))
 
       case   _: cfg.PreconditionBlock[ast.Stmt, ast.Exp]
            | _: cfg.PostconditionBlock[ast.Stmt, ast.Exp] =>
@@ -264,7 +263,7 @@ object executor extends ExecutionRules {
                         else {
                           execs(s3, stmts, v2)((s4, v3) => {
                             v3.decider.prover.comment("Loop head block: Follow loop-internal edges")
-                            follows(s4, sortedEdges, WhileFailed, v3)(Q)})}})}})}))
+                            follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})}))
 
           case _ =>
             /* We've reached a loop head block via an edge other than an in-edge: a normal edge or
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index de7b73134..7f0785dea 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -34,7 +34,6 @@ final case class State(g: Store = Store(),
                        quantifiedVariables: Stack[Var] = Nil,
                        retrying: Boolean = false,
                        underJoin: Boolean = false,
-                       joinPoints: Stack[SilverBlock] = Stack.empty,
                        functionRecorder: FunctionRecorder = NoopFunctionRecorder,
                        conservingSnapshotGeneration: Boolean = false,
                        recordPossibleTriggers: Boolean = false,
@@ -135,7 +134,6 @@ object State {
                  quantifiedVariables1,
                  retrying1,
                  underJoin1,
-                 joinPoints1,
                  functionRecorder1,
                  conservingSnapshotGeneration1,
                  recordPossibleTriggers1, possibleTriggers1,
@@ -158,7 +156,6 @@ object State {
                      `quantifiedVariables1`,
                      `retrying1`,
                      `underJoin1`,
-                     `joinPoints1`,
                      functionRecorder2,
                      `conservingSnapshotGeneration1`,
                      `recordPossibleTriggers1`, possibleTriggers2,
@@ -262,7 +259,7 @@ object State {
   }
 
   def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = {
-    println("Merge")
+    //println("Merge")
     s1 match {
       /* Decompose state s1 */
       case State(g1, h1, oldHeaps1,
@@ -273,7 +270,6 @@ object State {
       quantifiedVariables1,
       retrying1,
       underJoin1,
-      joinPoints1,
       functionRecorder1,
       conservingSnapshotGeneration1,
       recordPossibleTriggers1, possibleTriggers1,
@@ -296,7 +292,6 @@ object State {
           `quantifiedVariables1`,
           `retrying1`,
           `underJoin1`,
-          `joinPoints1`,
           functionRecorder2,
           `conservingSnapshotGeneration1`,
           `recordPossibleTriggers1`, possibleTriggers2,

From a52a1f8914e6930406fe3e884d4c50e06ec3da12 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Thu, 22 Jul 2021 13:53:23 +0200
Subject: [PATCH 13/58] add comments

---
 src/main/scala/rules/Joiner.scala | 15 +++++++++------
 src/main/scala/state/State.scala  | 20 +++++++-------------
 2 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index f43e7541b..677d52e86 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -46,13 +46,13 @@ object joiner extends JoiningRules {
       val s2 = s1.copy(underJoin = true)
 
       block(s2, v1, (s3, data, v2) => {
-        /* In order to prevent mismatches between different final states of the evaluation
-         * paths that are to be joined, we reset certain state properties that may have been
-         * affected by the evaluation - such as the store (by let-bindings) or the heap (by
-         * state consolidations) to their initial values.
-         */
         val s4 =
           if (resetState) {
+            /* In order to prevent mismatches between different final states of the evaluation
+             * paths that are to be joined, we reset certain state properties that may have been
+             * affected by the evaluation - such as the store (by let-bindings) or the heap (by
+             * state consolidations) to their initial values.
+             */
             s3.copy(g = s1.g,
                     h = s1.h,
                     oldHeaps = s1.oldHeaps,
@@ -61,7 +61,10 @@ object joiner extends JoiningRules {
                     ssCache = s1.ssCache,
                     partiallyConsumedHeap = s1.partiallyConsumedHeap,
                     invariantContexts = s1.invariantContexts)
-          } else s3
+          } else {
+            // For more joins, state shouldn't be reset.
+            s3
+          }
         entries :+= JoinDataEntry(s4, data, v2.decider.pcs.after(preMark))
         Success()
       })
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 7f0785dea..ff260db2d 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -200,6 +200,7 @@ object State {
     }
   }
 
+  // Lists all fields which do not match in two states.
   private def generateStateMismatchErrorMessage(s1: State, s2: State): Nothing = {
     val err = new StringBuilder()
     for (ix <- 0 until s1.productArity) yield {
@@ -217,6 +218,7 @@ object State {
 
   // Merges two maps based on fOnce, if entry only exists in one map,
   // and fTwice if entry exists in both maps.
+  // Used to merge the Store.
   private def mergeMaps[K, V, D](map1: Map[K, V], data1: D, map2: Map[K, V], data2: D)
                                 (fOnce: (V, D) => Option[V])
                                 (fTwice: (V, D, V, D) => Option[V])
@@ -235,7 +237,7 @@ object State {
     })
   }
 
-
+  // Puts a collection of chunks under a condition.
   private def conditionalizeChunks(h: Iterable[Chunk], cond: Term): Iterable[Chunk] = {
     h map (c => {
       c match {
@@ -246,10 +248,14 @@ object State {
     })
   }
 
+  // Puts a heap under a condition.
   private def conditionalizeHeap(h: Heap, cond: Term): Heap = {
     Heap(conditionalizeChunks(h.values, cond))
   }
 
+  // Merges two heaps together, by putting h1 under condition cond1,
+  // and h2 under cond2.
+  // Assumes that cond1 is the negation of cond2.
   def mergeHeap(h1: Heap, cond1: Term, h2: Heap, cond2: Term): Heap = {
     val (unconditionalHeapChunks, h1HeapChunksToConditionalize) = h1.values.partition(c1 => h2.values.exists(_ == c1))
     val h2HeapChunksToConditionalize = h2.values.filter(c2 => !unconditionalHeapChunks.exists(_ == c2))
@@ -314,8 +320,6 @@ object State {
             val conditions1 = And(pc1.branchConditions)
             val conditions2 = And(pc2.branchConditions)
 
-            //var mergePcs: Seq[Term] = Vector.empty
-
             val mergeStore = (g1: Store, g2: Store) => {
               Store(mergeMaps(g1.values, conditions1, g2.values, conditions2)
               ((_, _) => {
@@ -328,11 +332,6 @@ object State {
                   Some(v1)
                 } else {
                   assert(v1.sort == v2.sort)
-                  // TODO: Is this faster?
-                  //val t = verifier.decider.fresh(v1.sort)
-                  //mergePcs :+= Implies(cond1, Equals(t, v1))
-                  //mergePcs :+= Implies(cond2, Equals(t, v2))
-                  //Some(t)
                   Some(Ite(cond1, v1, v2))
                 }
               }))
@@ -360,8 +359,6 @@ object State {
               Some(mergeHeap(heap1, cond1, heap2, cond2))
             }))
 
-            //verifier.decider.assume(mergePcs)
-
             // TODO: InvariantContexts should most likely be the same
             assert(invariantContexts1.length == invariantContexts2.length)
             val invariantContexts3 = invariantContexts1
@@ -380,9 +377,6 @@ object State {
               .zip(conservedPcs1)
               .map({case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct})
 
-            //assert(conservedPcs1 == conservedPcs2)
-            //val conservedPcs3 = conservedPcs1
-
             val s3 = s1.copy(functionRecorder = functionRecorder3,
               possibleTriggers = possibleTriggers3,
               triggerExp = triggerExp3,

From 539e6d1eb9470c35805e87c7fbb42fe7142cecff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Thu, 22 Jul 2021 13:54:17 +0200
Subject: [PATCH 14/58] reset default config

---
 src/main/scala/Config.scala | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 0565bd719..0c185b823 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -199,7 +199,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val timeout: ScallopOption[Int] = opt[Int]("timeout",
     descr = ( "Time out after approx. n seconds. The timeout is for the whole verification, "
             + "not per method or proof obligation (default: 0, i.e. no timeout)."),
-    default = Some(180),
+    default = Some(0),
     noshort = true
   )
 
@@ -449,7 +449,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val disableCaches: ScallopOption[Boolean] = opt[Boolean]("disableCaches",
     descr = "Disables various caches in Silicon's state.",
-    default = Some(true),
+    default = Some(false),
     noshort = true
   )
 
@@ -460,13 +460,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   val enableMoreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
     descr = "Enable a more complete exhale version.",
-    default = Some(true),
+    default = Some(false),
     noshort = true
   )
 
   val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
     descr = "Enable more joins using a more complete implementation of state merging.",
-    default = Some(true),
+    default = Some(false),
     noshort = true
   )
 
@@ -479,7 +479,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
     descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
              + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()}"),
-    default = Some(1),
+    default = Some(Runtime.getRuntime.availableProcessors()),
     noshort = true
   )
 

From 19fc8bc6acec968bae4314733ad23d6304c88cac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Thu, 22 Jul 2021 16:23:49 +0200
Subject: [PATCH 15/58] add more comments

---
 src/main/scala/rules/Executor.scala | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index c07aa1364..d5cb8c8cd 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -118,6 +118,9 @@ object executor extends ExecutionRules {
       val branchPoint = edge1.source
 
       s.methodCfg.joinPoints.get(branchPoint) match {
+        // If a join point was found, the config argument is enabled,
+        // and the source of both conditional edges was a statement block
+        // (we are at an if-statement), we may join the resulting branches again.
         case Some(newJoinPoint) if
           Verifier.config.moreJoins() &&
           edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
@@ -135,7 +138,7 @@ object executor extends ExecutionRules {
           eval(s, edge1.condition, pvef(edge1.condition), v)((s1, t0, v1) =>
             joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
               brancher.branch(s2, t0, v2)(
-                // Follow until join point.
+                // Follow only until join point.
                 (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)),
                 (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint))((s, v) => QB(s, null, v))
               )

From 672a92d1b39d012088225621c39d753afc274ab4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 14:42:37 +0200
Subject: [PATCH 16/58] clarify comment

---
 src/main/scala/rules/Consumer.scala | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index 080eae6f1..2527a5249 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -204,12 +204,14 @@ object consumer extends ConsumptionRules {
               case Seq(entry) => // One branch is dead
                 (entry.s, entry.data)
               case Seq(entry1, entry2) => // Both branches are alive
+                // Here we merge additional data collected in each branch.
+                // We assume that entry1.pcs is negation of entry2.pcs.
                 val mergedData = (
+                  // The partially consumed heap is merged based on the corresponding branch conditions of each branch.
                   State.mergeHeap(
                     entry1.data._1, And(entry1.pathConditions.branchConditions),
                     entry2.data._1, And(entry2.pathConditions.branchConditions),
                   ),
-                  // Asume that entry1.pcs is inverse of entry2.pcs
                   Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
                 )
                 (entry1.pathConditionAwareMerge(entry2), mergedData)

From be98b513d1993556dc0d9ae90b691628deb9e3a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 14:50:55 +0200
Subject: [PATCH 17/58] align return argument

---
 src/main/scala/state/State.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index ff260db2d..1c215af96 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -222,7 +222,7 @@ object State {
   private def mergeMaps[K, V, D](map1: Map[K, V], data1: D, map2: Map[K, V], data2: D)
                                 (fOnce: (V, D) => Option[V])
                                 (fTwice: (V, D, V, D) => Option[V])
-  : Map[K, V] = {
+                                : Map[K, V] = {
 
     map1.flatMap({ case (k, v1) =>
       (map2.get(k) match {

From 9bd736f04939816f0189a78f60d9959dd31752c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 14:53:57 +0200
Subject: [PATCH 18/58] remove comment

---
 src/main/scala/state/State.scala | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 1c215af96..0a22fe903 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -265,7 +265,6 @@ object State {
   }
 
   def merge(s1: State, pc1: RecordedPathConditions, s2: State, pc2: RecordedPathConditions): State = {
-    //println("Merge")
     s1 match {
       /* Decompose state s1 */
       case State(g1, h1, oldHeaps1,

From ba421cca17c6151ac5f1bf1f8cdcfd00185599b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 14:56:09 +0200
Subject: [PATCH 19/58] indentation

---
 src/main/scala/state/State.scala | 72 ++++++++++++++++----------------
 1 file changed, 36 insertions(+), 36 deletions(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 0a22fe903..865f9374e 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -268,46 +268,46 @@ object State {
     s1 match {
       /* Decompose state s1 */
       case State(g1, h1, oldHeaps1,
-      parallelizeBranches1,
-      recordVisited1, visited1,
-      methodCfg1, invariantContexts1,
-      constrainableARPs1,
-      quantifiedVariables1,
-      retrying1,
-      underJoin1,
-      functionRecorder1,
-      conservingSnapshotGeneration1,
-      recordPossibleTriggers1, possibleTriggers1,
-      triggerExp1,
-      partiallyConsumedHeap1,
-      permissionScalingFactor1,
-      reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
-      applyHeuristics1, heuristicsDepth1, triggerAction1,
-      ssCache1, hackIssue387DisablePermissionConsumption1,
-      qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
-      predicateSnapMap1, predicateFormalVarMap1, hack) =>
+                 parallelizeBranches1,
+                 recordVisited1, visited1,
+                 methodCfg1, invariantContexts1,
+                 constrainableARPs1,
+                 quantifiedVariables1,
+                 retrying1,
+                 underJoin1,
+                 functionRecorder1,
+                 conservingSnapshotGeneration1,
+                 recordPossibleTriggers1, possibleTriggers1,
+                 triggerExp1,
+                 partiallyConsumedHeap1,
+                 permissionScalingFactor1,
+                 reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
+                 applyHeuristics1, heuristicsDepth1, triggerAction1,
+                 ssCache1, hackIssue387DisablePermissionConsumption1,
+                 qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
+                 predicateSnapMap1, predicateFormalVarMap1, hack) =>
 
         /* Decompose state s2: most values must match those of s1 */
         s2 match {
           case State(g2, h2, oldHeaps2,
-          `parallelizeBranches1`,
-          `recordVisited1`, `visited1`,
-          `methodCfg1`, invariantContexts2,
-          constrainableARPs2,
-          `quantifiedVariables1`,
-          `retrying1`,
-          `underJoin1`,
-          functionRecorder2,
-          `conservingSnapshotGeneration1`,
-          `recordPossibleTriggers1`, possibleTriggers2,
-          triggerExp2,
-          partiallyConsumedHeap2,
-          `permissionScalingFactor1`,
-          reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
-          `applyHeuristics1`, `heuristicsDepth1`, `triggerAction1`,
-          ssCache2, `hackIssue387DisablePermissionConsumption1`,
-          `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, smDomainNeeded2,
-          `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`) =>
+                     `parallelizeBranches1`,
+                     `recordVisited1`, `visited1`,
+                     `methodCfg1`, invariantContexts2,
+                     constrainableARPs2,
+                     `quantifiedVariables1`,
+                     `retrying1`,
+                     `underJoin1`,
+                     functionRecorder2,
+                     `conservingSnapshotGeneration1`,
+                     `recordPossibleTriggers1`, possibleTriggers2,
+                     triggerExp2,
+                     partiallyConsumedHeap2,
+                     `permissionScalingFactor1`,
+                     reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
+                     `applyHeuristics1`, `heuristicsDepth1`, `triggerAction1`,
+                     ssCache2, `hackIssue387DisablePermissionConsumption1`,
+                     `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, smDomainNeeded2,
+                     `predicateSnapMap1`, `predicateFormalVarMap1`, `hack`) =>
 
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2

From 26b4f4b49974a8e6fbcc8b8bf031ca859e907fcd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 14:58:45 +0200
Subject: [PATCH 20/58] indentation, one comment

---
 src/main/scala/state/State.scala | 33 ++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 865f9374e..c2c82143d 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -377,25 +377,26 @@ object State {
               .map({case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct})
 
             val s3 = s1.copy(functionRecorder = functionRecorder3,
-              possibleTriggers = possibleTriggers3,
-              triggerExp = triggerExp3,
-              constrainableARPs = constrainableARPs3,
-              // TODO: Merge caches.
-              ssCache = Map.empty,
-              smCache = SnapshotMapCache.empty,
-              pmCache = Map.empty,
-              g = g3,
-              h = h3,
-              oldHeaps = oldHeaps3,
-              partiallyConsumedHeap = partiallyConsumedHeap3,
-              smDomainNeeded = smDomainNeeded3,
-              invariantContexts = invariantContexts3,
-              reserveHeaps = reserveHeaps3,
-              conservedPcs = conservedPcs3,
-            )
+                             possibleTriggers = possibleTriggers3,
+                             triggerExp = triggerExp3,
+                             constrainableARPs = constrainableARPs3,
+                             // TODO: Merge caches.
+                             ssCache = Map.empty,
+                             smCache = SnapshotMapCache.empty,
+                             pmCache = Map.empty,
+                             g = g3,
+                             h = h3,
+                             oldHeaps = oldHeaps3,
+                             partiallyConsumedHeap = partiallyConsumedHeap3,
+                             smDomainNeeded = smDomainNeeded3,
+                             invariantContexts = invariantContexts3,
+                             reserveHeaps = reserveHeaps3,
+                             conservedPcs = conservedPcs3)
 
             s3
 
+            // Optionally, we could also do a state consolidation after each
+            // state merging, but this has shown to decrease performance a bit.
             //val s4 = verifier.stateConsolidator.consolidate(s3, verifier)
             //s4
 

From 367423950271556cae0f841cae980c61ed412342 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 19:21:21 +0200
Subject: [PATCH 21/58] clarify comment

---
 src/main/scala/rules/Joiner.scala | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index 677d52e86..7bb28f5d8 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -14,8 +14,9 @@ import viper.silicon.state.State
 import viper.silicon.verifier.Verifier
 
 case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions) {
-  // Instead of merging states, we can directly merge JoinDataEntries to obtain new States.
-  // This gives us more information about the path conditions.
+  // Instead of merging states by calling State.merge,
+  // we can directly merge JoinDataEntries to obtain new States,
+  // and the join data entries themselves provide information about the path conditions to State.merge.
   def pathConditionAwareMerge(other: JoinDataEntry[D]): State = {
     State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
   }

From 97b129551e3b822f795542395b3062e7b42d832f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Mon, 26 Jul 2021 19:30:33 +0200
Subject: [PATCH 22/58] clarify the use of scala.Null as a type argument

---
 src/main/scala/rules/Executor.scala | 1 +
 src/main/scala/rules/Producer.scala | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 35ebd5eba..7830a85df 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -135,6 +135,7 @@ object executor extends ExecutionRules {
           })
 
           eval(s, edge1.condition, pvef(edge1.condition), v)((s1, t0, v1) =>
+            // The type arguments here are Null because there is no need to pass any join data.
             joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
               brancher.branch(s2, t0, v2)(
                 // Follow only until join point.
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 6f5a6e267..069674d46 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -211,6 +211,7 @@ object producer extends ProductionRules {
         val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord)
 
         eval(s, e0, pve, v)((s1, t0, v1) =>
+          // The type arguments here are Null because there is no need to pass any join data.
           joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
             branch(s1, t0, v1)(
               (s2, v2) => produceR(s2, sf, a0, pve, v2)((s3, v3) => {
@@ -263,6 +264,7 @@ object producer extends ProductionRules {
         val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord)
 
         eval(s, e0, pve, v)((s1, t0, v1) =>
+          // The type arguments here are Null because there is no need to pass any join data.
           joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
             branch(s1, t0, v1)(
               (s2, v2) => produceR(s2, sf, a1, pve, v2)((s3, v3) => {

From c4c8eb3644748f7a586ee19968da508e6c4b0c37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Tue, 27 Jul 2021 18:37:36 +0200
Subject: [PATCH 23/58] rewrite joining in executor

---
 src/main/scala/rules/Executor.scala | 72 +++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 7830a85df..d53e58a10 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -105,6 +105,76 @@ object executor extends ExecutionRules {
                      (Q: (State, Verifier) => VerificationResult)
                      : VerificationResult = {
 
+    // Find join point if it exists.
+    val jp: Option[SilverBlock] = edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+
+    (edges, jp) match {
+      case (Seq(), _) => Q(s, v)
+      case (Seq(edge), _) => follow(s, edge, v, joinPoint)(Q)
+      case (Seq(edge1, edge2), Some(newJoinPoint)) if
+          Verifier.config.moreJoins() &&
+          // Can't directly match type because of type erasure ...
+          edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
+          edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
+          // We only join branches that originate from if statements
+          // this is the case if the source is a statement block,
+          // as opposed to a loop head block.
+          edge1.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]] &&
+          edge2.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]] =>
+
+        assert(edge1.source == edge2.source)
+
+        val cedge1 = edge1.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
+        val cedge2 = edge2.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
+
+        // Here we assume that edge1.condition is the negation of edge2.condition.
+        assert((cedge1.condition, cedge2.condition) match {
+          case (exp1, ast.Not(exp2)) => exp1 == exp2
+          case (ast.Not(exp1), exp2) => exp1 == exp2
+          case _ => false
+        })
+
+        eval(s, cedge1.condition, pvef(cedge1.condition), v)((s1, t0, v1) =>
+          // The type arguments here are Null because there is no need to pass any join data.
+          joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
+            brancher.branch(s2, t0, v2)(
+              // Follow only until join point.
+              (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)),
+              (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint))((s, v) => QB(s, null, v))
+            )
+          })(entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                entry.s
+              case Seq(entry1, entry2) => // Both branches are alive
+                entry1.pathConditionAwareMerge(entry2)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")
+            }
+            (s2, null)
+          })((s4, _, v4) => {
+            // Continue after merging at join point.
+            exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint)(Q)
+          })
+        )
+
+      case _ =>
+        val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
+        val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
+          case (fatalResult: FatalResult, _) => fatalResult
+          case (_, (edge, edgeIndex)) => {
+            if (edgeIndex != 0) {
+              SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
+            }
+            SymbExLogger.currentLog().markReachable(uidBranchPoint)
+            follow(s, edge, v, joinPoint)(Q)
+          }
+        }
+        SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
+        res
+    }
+
+    /*
     if (edges.isEmpty) {
       Q(s, v)
     } else if (edges.length == 1) {
@@ -178,6 +248,8 @@ object executor extends ExecutionRules {
     } else {
       sys.error("At most two out edges expected.")
     }
+    */
+
   }
 
   def exec(s: State, graph: SilverCfg, v: Verifier)

From dda02c8c2ee02184326cc866423ed61e7f8fab6a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabian=20B=C3=B6siger?= <boesiger.fabian@outlook.com>
Date: Wed, 28 Jul 2021 08:53:17 +0200
Subject: [PATCH 24/58] remove commented out code

---
 src/main/scala/rules/Executor.scala | 77 -----------------------------
 1 file changed, 77 deletions(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index d53e58a10..004458083 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -173,83 +173,6 @@ object executor extends ExecutionRules {
         SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
         res
     }
-
-    /*
-    if (edges.isEmpty) {
-      Q(s, v)
-    } else if (edges.length == 1) {
-      follow(s, edges.head, v, joinPoint)(Q)
-    } else if (edges.length == 2) {
-      val edge1 = edges.head.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
-      val edge2 = edges.last.asInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]]
-
-      assert(edge1.source == edge2.source)
-      val branchPoint = edge1.source
-
-      s.methodCfg.joinPoints.get(branchPoint) match {
-        // If a join point was found, the config argument is enabled,
-        // and the source of both conditional edges was a statement block
-        // (we are at an if-statement), we may join the resulting branches again.
-        case Some(newJoinPoint) if
-          Verifier.config.moreJoins() &&
-          edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
-          edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
-          edge1.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]] &&
-          edge2.source.isInstanceOf[StatementBlock[ast.Stmt, ast.Exp]]
-        => {
-          // Here we assume that edge1.condition is the negation of edge2.condition.
-          assert((edge1.condition, edge2.condition) match {
-            case (exp1, ast.Not(exp2)) => exp1 == exp2
-            case (ast.Not(exp1), exp2) => exp1 == exp2
-            case _ => false
-          })
-
-          eval(s, edge1.condition, pvef(edge1.condition), v)((s1, t0, v1) =>
-            // The type arguments here are Null because there is no need to pass any join data.
-            joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => {
-              brancher.branch(s2, t0, v2)(
-                // Follow only until join point.
-                (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)),
-                (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint))((s, v) => QB(s, null, v))
-              )
-            })(entries => {
-              val s2 = entries match {
-                case Seq(entry) => // One branch is dead
-                  entry.s
-                case Seq(entry1, entry2) => // Both branches are alive
-                  entry1.pathConditionAwareMerge(entry2)
-                case _ =>
-                  sys.error(s"Unexpected join data entries: $entries")
-              }
-              (s2, null)
-            })((s4, _, v4) => {
-              // Continue after merging at join point.
-              exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint)(Q)
-            })
-          )
-
-        }
-        case _ =>
-          val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length)
-          val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
-            case (fatalResult: FatalResult, _) => fatalResult
-            case (_, (edge, edgeIndex)) => {
-              if (edgeIndex != 0) {
-                SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint)
-              }
-              SymbExLogger.currentLog().markReachable(uidBranchPoint)
-              follow(s, edge, v, joinPoint)(Q)
-            }
-          }
-          SymbExLogger.currentLog().endBranchPoint(uidBranchPoint)
-          res
-      }
-
-    } else {
-      sys.error("At most two out edges expected.")
-    }
-    */
-
   }
 
   def exec(s: State, graph: SilverCfg, v: Verifier)

From 0b89740aa9c8c30a9acd7e023b463a3c34fe18c0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 6 Jun 2023 14:17:59 +0200
Subject: [PATCH 25/58] Alternative heuristics for consumeSingle that emulate
 greedy behavior

---
 .../scala/rules/QuantifiedChunkSupport.scala  | 36 +++++++++++++++++--
 1 file changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 857bacb02..a01928083 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1231,8 +1231,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       case Some(heuristics) =>
         heuristics
       case None =>
-        quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(
-          quantifiedChunkSupporter.extractHints(None, arguments))
+        quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(arguments,
+          quantifiedChunkSupporter.extractHints(None, arguments), v)
     }
 
     if (s.exhaleExt) {
@@ -1364,7 +1364,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       // that already exists.
       // During function verification, we should not define macros, since they could contain resullt, which is not
       // defined elsewhere.
-      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight
+      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight && ch.singletonArguments.isEmpty
 
       val permsProvided = ch.perm
       val permsTaken = if (declareMacro) {
@@ -1734,6 +1734,36 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       matchingChunks ++ otherChunks
     }
 
+  def singleReceiverChunkOrderHeuristic(receiver: Seq[Term], hints: Seq[Term], v: Verifier)
+                                       : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = {
+    // Heuristic that emulates greedy Silicon behavior for consuming single-receiver permissions.
+    // First:  Find singleton chunks that have the same receiver syntactically.
+    //         If so, consider those first, then all others.
+    // Second: If nothing matches syntactically, try to find a chunk that matches the receiver using the decider.
+    //         If that's the case, consider that chunk first, then all others.
+    // Third:  As a fallback, use the standard hint based heuristics.
+    val fallback = hintBasedChunkOrderHeuristic(hints)
+
+    (chunks: Seq[QuantifiedBasicChunk]) => {
+      val (syntacticMatches, others) = chunks.partition(c => c.singletonArguments.contains(receiver))
+      if (syntacticMatches.nonEmpty) {
+        syntacticMatches ++ others
+      } else {
+        val greedyMatch = chunks.find(c => c.singletonArguments match {
+          case Some(args) if args.length == receiver.length =>
+            args.zip(receiver).forall(ts => v.decider.check(ts._1 === ts._2, Verifier.config.checkTimeout()))
+          case _ =>
+            false
+        }).toSeq
+        if (greedyMatch.nonEmpty) {
+          greedyMatch ++ chunks.diff(greedyMatch)
+        } else {
+          fallback(chunks)
+        }
+      }
+    }
+  }
+
   def extractHints(cond: Option[Term], arguments: Seq[Term]): Seq[Term] = {
     var hints =
       arguments.flatMap {

From 92be50726f41303d88650822a57cb2d87a909c1a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 6 Jun 2023 15:39:42 +0200
Subject: [PATCH 26/58] Using better hints also in Executor

---
 src/main/scala/rules/Executor.scala               | 2 +-
 src/main/scala/rules/QuantifiedChunkSupport.scala | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 24d2c602d..b9ef20052 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -313,7 +313,7 @@ object executor extends ExecutionRules {
             val (relevantChunks, otherChunks) =
               quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s2.h, BasicChunkIdentifier(field.name))
             val hints = quantifiedChunkSupporter.extractHints(None, Seq(tRcvr))
-            val chunkOrderHeuristics = quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(hints)
+            val chunkOrderHeuristics = quantifiedChunkSupporter.singleReceiverChunkOrderHeuristic(Seq(tRcvr), hints, v2)
             val s2p = if (s2.heapDependentTriggers.contains(field)){
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index a01928083..d1f6102df 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1364,7 +1364,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       // that already exists.
       // During function verification, we should not define macros, since they could contain resullt, which is not
       // defined elsewhere.
-      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight && ch.singletonArguments.isEmpty
+      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight
 
       val permsProvided = ch.perm
       val permsTaken = if (declareMacro) {

From 9716a0aca308113dfad1422faacc3282288799e9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 6 Jun 2023 17:45:09 +0200
Subject: [PATCH 27/58] Reverting tests back to normal

---
 src/test/scala/SiliconTests.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala
index 61e9ec65f..027bd3da2 100644
--- a/src/test/scala/SiliconTests.scala
+++ b/src/test/scala/SiliconTests.scala
@@ -56,5 +56,5 @@ class SiliconTests extends SilSuite {
   }
 
   val commandLineArguments: Seq[String] =
-    Seq("--timeout", "600" /* seconds */, "--moreJoins", "--enableMoreCompleteExhale", "--parallelizeBranches")
+    Seq("--timeout", "600" /* seconds */)
 }

From 87fe3e05e3e445554c9fa399ef3627e11c80b3aa Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 6 Jun 2023 20:34:33 +0200
Subject: [PATCH 28/58] No longer stopping on FatalResult (this broke refute)

---
 src/main/scala/rules/Executor.scala | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index f8d973978..dad36f6b8 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -178,13 +178,12 @@ object executor extends ExecutionRules {
       case _ =>
         val uidBranchPoint = v.symbExLog.insertBranchPoint(edges.length)
         val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) {
-          case (fatalResult: FatalResult, _) => fatalResult
-          case (_, (edge, edgeIndex)) => {
+          case (result: VerificationResult, (edge, edgeIndex)) => {
             if (edgeIndex != 0) {
               v.symbExLog.switchToNextBranch(uidBranchPoint)
             }
             v.symbExLog.markReachable(uidBranchPoint)
-            follow(s, edge, v, joinPoint)(Q)
+            result combine follow(s, edge, v, joinPoint)(Q)
           }
         }
         v.symbExLog.endBranchPoint(uidBranchPoint)

From ea2173c0d94e5a79ff5b0dae1a1f942e17ef9c67 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 24 Aug 2023 16:34:55 +0200
Subject: [PATCH 29/58] Adjusting no of errors reported in branch
 parallelization code, slightly better parameter naming

---
 src/main/scala/decider/Decider.scala | 4 ++--
 src/main/scala/rules/Brancher.scala  | 5 +++++
 src/main/scala/rules/Executor.scala  | 2 +-
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index 5ab109ea4..8b6c13384 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -379,8 +379,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions
     def freshMacros: Vector[MacroDecl] = _declaredFreshMacros
 
-    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit = {
-      if (!toStack) {
+    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
+      if (!toSymbolStack) {
         functions foreach prover.declare
 
         _declaredFreshFunctions = _declaredFreshFunctions ++ functions
diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
index cfde932d3..b2ab162f0 100644
--- a/src/main/scala/rules/Brancher.scala
+++ b/src/main/scala/rules/Brancher.scala
@@ -91,6 +91,7 @@ object brancher extends BranchingRules {
     var functionsOfElseBranchDecider: Set[FunctionDecl] = null
     var macrosOfElseBranchDecider: Seq[MacroDecl] = null
     var pcsForElseBranch: PathConditionStack = null
+    var noOfErrors = 0
 
     val elseBranchVerificationTask: Verifier => VerificationResult =
       if (executeElseBranch) {
@@ -106,6 +107,7 @@ object brancher extends BranchingRules {
           functionsOfCurrentDecider = v.decider.freshFunctions
           macrosOfCurrentDecider = v.decider.freshMacros
           pcsForElseBranch = v.decider.pcs.duplicate()
+          noOfErrors = v.errorsReportedSoFar.get()
         }
 
         (v0: Verifier) => {
@@ -129,6 +131,7 @@ object brancher extends BranchingRules {
 
             v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
             v0.decider.setPcs(pcsForElseBranch)
+            v0.errorsReportedSoFar.set(noOfErrors)
           }
           elseBranchVerifier = v0.uniqueId
 
@@ -193,6 +196,7 @@ object brancher extends BranchingRules {
       try {
         if (parallelizeElseBranch) {
           val pcsAfterThenBranch = v.decider.pcs.duplicate()
+          val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get()
 
           val pcsBefore = v.decider.pcs
 
@@ -202,6 +206,7 @@ object brancher extends BranchingRules {
             // we have done other work during the join, need to reset
             v.decider.prover.comment(s"Resetting path conditions after interruption")
             v.decider.setPcs(pcsAfterThenBranch)
+            v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch)
             v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
           }
         }else{
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index eef39839b..782cad60d 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -260,7 +260,7 @@ object executor extends ExecutionRules {
                       intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => {
                         eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) =>
                           Success())})}})})
-            && executionFlowController.locally(s, v)((s0, v0) => {
+            combine executionFlowController.locally(s, v)((s0, v0) => {
                 v0.decider.prover.comment("Loop head block: Establish invariant")
                 consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")

From 9b62b97765ffc2db805e3be4853515268ba55cda Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 12 Sep 2023 00:57:50 +0200
Subject: [PATCH 30/58] De-prioritize singleton chunks when we know none of
 them definitely fits

---
 src/main/scala/rules/QuantifiedChunkSupport.scala | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 09f1dca3b..67211833f 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1761,7 +1761,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         if (greedyMatch.nonEmpty) {
           greedyMatch ++ chunks.diff(greedyMatch)
         } else {
-          fallback(chunks)
+          // It doesn't seem to be any of the singletons. Use the fallback on the non-singletons.
+          val (qpChunks, singletons) = chunks.partition(_.singletonArguments.isEmpty)
+          fallback(qpChunks) ++ singletons
         }
       }
     }

From 9069f59626d820e605456d5d09816587e2d49b6e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 22 Sep 2023 13:43:49 +0200
Subject: [PATCH 31/58] Fixing unknown function error by recording snapshot
 masks

---
 src/main/scala/rules/Evaluator.scala | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 610cc514e..d8688acc8 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -1416,13 +1416,15 @@ object evaluator extends EvaluationRules {
         triggerAxioms = triggerAxioms ++ axioms
         smDefs = smDefs ++ smDef
       case pa: ast.PredicateAccess if s.heapDependentTriggers.contains(pa.loc(s.program)) =>
-        val (axioms, trigs, _) = generatePredicateTrigger(pa, s, pve, v)
+        val (axioms, trigs, _, smDef) = generatePredicateTrigger(pa, s, pve, v)
         triggers = triggers ++ trigs
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case wand: ast.MagicWand if s.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program)) =>
-        val (axioms, trigs, _) = generateWandTrigger(wand, s, pve, v)
+        val (axioms, trigs, _, smDef) = generateWandTrigger(wand, s, pve, v)
         triggers = triggers ++ trigs
         triggerAxioms = triggerAxioms ++ axioms
+        smDefs = smDefs ++ smDef
       case e => evalTrigger(s, Seq(e), pve, v)((_, t, _) => {
         triggers = triggers ++ t
         Success()
@@ -1502,7 +1504,11 @@ object evaluator extends EvaluationRules {
   }
 
   /* TODO: Try to unify with generateFieldTrigger above, or at least with generateWandTrigger below */
-  private def generatePredicateTrigger(pa: ast.PredicateAccess, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = {
+  private def generatePredicateTrigger(pa: ast.PredicateAccess,
+                                       s: State,
+                                       pve: PartialVerificationError,
+                                       v: Verifier)
+                                      : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = {
     var axioms = Seq.empty[Term]
     var triggers = Seq.empty[Term]
     var mostRecentTrig: PredicateTrigger = null
@@ -1524,11 +1530,15 @@ object evaluator extends EvaluationRules {
       Success()
     })
 
-    (axioms, triggers, mostRecentTrig)
+    (axioms, triggers, mostRecentTrig, Seq(smDef1))
   }
 
   /* TODO: See comments for generatePredicateTrigger above */
-  private def generateWandTrigger(wand: ast.MagicWand, s: State, pve: PartialVerificationError, v: Verifier): (Seq[Term], Seq[Term], PredicateTrigger) = {
+  private def generateWandTrigger(wand: ast.MagicWand,
+                                  s: State,
+                                  pve: PartialVerificationError,
+                                  v: Verifier)
+                                 : (Seq[Term], Seq[Term], PredicateTrigger, Seq[SnapshotMapDefinition]) = {
     var axioms = Seq.empty[Term]
     var triggers = Seq.empty[Term]
     var mostRecentTrig: PredicateTrigger = null
@@ -1552,7 +1562,7 @@ object evaluator extends EvaluationRules {
       Success()
     })
 
-    (axioms, triggers, mostRecentTrig)
+    (axioms, triggers, mostRecentTrig, Seq(smDef1))
   }
 
   /* Evaluate a sequence of expressions in Order

From e355cd86a90efdfd44de71675c416a85bc3da2ba Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 25 Sep 2023 18:18:00 +0200
Subject: [PATCH 32/58] Fixing issue 751

---
 src/main/scala/decider/TermToZ3APIConverter.scala | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
index 8cf6d83fe..c591aec27 100644
--- a/src/main/scala/decider/TermToZ3APIConverter.scala
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -471,9 +471,17 @@ class TermToZ3APIConverter
     // workaround: since we cannot create a function application with just the name, we let Z3 parse
     // a string that uses the function, take the AST, and get the func decl from there, so that we can
     // programmatically create a func app.
-    val decls = args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ")
+
+
+    val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort.
+    // ME: The parsing happens in a fresh context that doesn't know any of our current declarations.
+    // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there
+    // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however,
+    // such functions exist. So we re-declare *only* this sort.
+    val decls = declPreamble + args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ")
     val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
     val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
+    println(assertion)
     val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
     val app = workaround(0).getArgs()(0)
     val decl = app.getFuncDecl

From 6b85bac8a47a89b7ac8ddb1d686ee6f64468384d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 25 Sep 2023 18:41:18 +0200
Subject: [PATCH 33/58] Caching for SMT func decls

---
 .../scala/decider/TermToZ3APIConverter.scala  | 47 +++++++++++--------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
index c591aec27..4ba1b4776 100644
--- a/src/main/scala/decider/TermToZ3APIConverter.scala
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -30,6 +30,7 @@ class TermToZ3APIConverter
 
   val sortCache = mutable.HashMap[Sort, Z3Sort]()
   val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]()
+  val smtFuncDeclCache = mutable.HashMap[(String, Seq[Sort]), (Z3FuncDecl, Seq[Z3Expr])]()
   val termCache = mutable.HashMap[Term, Z3Expr]()
 
   def convert(s: Sort): Z3Sort = convertSort(s)
@@ -472,26 +473,33 @@ class TermToZ3APIConverter
     // a string that uses the function, take the AST, and get the func decl from there, so that we can
     // programmatically create a func app.
 
-
-    val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort.
-    // ME: The parsing happens in a fresh context that doesn't know any of our current declarations.
-    // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there
-    // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however,
-    // such functions exist. So we re-declare *only* this sort.
-    val decls = declPreamble + args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ")
-    val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
-    val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
-    println(assertion)
-    val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
-    val app = workaround(0).getArgs()(0)
-    val decl = app.getFuncDecl
-    val actualArgs =  if (decl.getArity > args.length){
-      // the function name we got wasn't just a function name but also contained a first argument.
-      // this happens with float operations where functionName contains a rounding mode.
-      app.getArgs.toSeq.slice(0, decl.getArity - args.length) ++ args.map(convertTerm(_))
-    }else {
-      args.map(convertTerm(_))
+    val cacheKey = (functionName, args.map(_.sort))
+    val (decl, additionalArgs: Seq[Z3Expr]) = if (smtFuncDeclCache.contains(cacheKey)) {
+      smtFuncDeclCache(cacheKey)
+    } else {
+      val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort.
+      // ME: The parsing happens in a fresh context that doesn't know any of our current declarations.
+      // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there
+      // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however,
+      // such functions exist. So we re-declare *only* this sort.
+      val decls = declPreamble + args.zipWithIndex.map { case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})" }.mkString(" ")
+      val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
+      val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
+      val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
+      val app = workaround(0).getArgs()(0)
+      val decl = app.getFuncDecl
+      val additionalArgs = if (decl.getArity > args.length) {
+        // the function name we got wasn't just a function name but also contained a first argument.
+        // this happens with float operations where functionName contains a rounding mode.
+        app.getArgs.toSeq.slice(0, decl.getArity - args.length)
+      } else {
+        Seq()
+      }
+      smtFuncDeclCache.put(cacheKey, (decl, additionalArgs))
+      (decl, additionalArgs)
     }
+
+    val actualArgs = additionalArgs ++ args.map(convertTerm(_))
     ctx.mkApp(decl, actualArgs.toArray : _*)
   }
 
@@ -530,6 +538,7 @@ class TermToZ3APIConverter
     sanitizedNamesCache.clear()
     macros.clear()
     funcDeclCache.clear()
+    smtFuncDeclCache.clear()
     sortCache.clear()
     termCache.clear()
     unitConstructor = null

From e28254a7b6c89d1fc044f27f5f3ddb8d85dbbb5b Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 26 Sep 2023 03:31:16 +0200
Subject: [PATCH 34/58] Improved filtering of bad triggers

---
 src/main/scala/decider/Z3ProverAPI.scala | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala
index d5b9dfe77..c5b5c9b42 100644
--- a/src/main/scala/decider/Z3ProverAPI.scala
+++ b/src/main/scala/decider/Z3ProverAPI.scala
@@ -10,7 +10,7 @@ import com.typesafe.scalalogging.LazyLogging
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
 import viper.silicon.state.IdentifierFactory
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts}
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, Var, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
@@ -258,11 +258,12 @@ class Z3ProverAPI(uniqueId: String,
     triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
     val cleanTerm = term.transform {
       case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
-        val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect {
+        val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn =>
+          ptrn.isInstanceOf[Var] || ptrn.shallowCollect {
           case t => triggerGenerator.isForbiddenInTrigger(t)
         }.nonEmpty))
         q.copy(triggers = goodTriggers)
-    }()
+    }({t => true})
     cleanTerm
   }
 

From 8527848dc9f12bb5da739874f2a9259bd3c85575 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 26 Sep 2023 10:56:43 +0200
Subject: [PATCH 35/58] Fixing issue #707 for Z3 API as well

---
 src/main/scala/decider/TermToZ3APIConverter.scala | 5 ++++-
 src/main/scala/decider/Z3ProverAPI.scala          | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
index 4ba1b4776..7b177ceea 100644
--- a/src/main/scala/decider/TermToZ3APIConverter.scala
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -483,7 +483,10 @@ class TermToZ3APIConverter
       // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however,
       // such functions exist. So we re-declare *only* this sort.
       val decls = declPreamble + args.zipWithIndex.map { case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})" }.mkString(" ")
-      val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
+      val funcAppString = if (args.nonEmpty)
+        s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})"
+      else
+        functionName
       val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))"
       val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null)
       val app = workaround(0).getArgs()(0)
diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala
index c5b5c9b42..c0cdbe12f 100644
--- a/src/main/scala/decider/Z3ProverAPI.scala
+++ b/src/main/scala/decider/Z3ProverAPI.scala
@@ -263,7 +263,7 @@ class Z3ProverAPI(uniqueId: String,
           case t => triggerGenerator.isForbiddenInTrigger(t)
         }.nonEmpty))
         q.copy(triggers = goodTriggers)
-    }({t => true})
+    }(_ => true)
     cleanTerm
   }
 

From e957272d696ef46fdd29c531660f933e93912a34 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 23:44:10 +0200
Subject: [PATCH 36/58] Unfold, unfolding and fold no longer allowed with
 none-permission

---
 src/main/scala/rules/Evaluator.scala          |  4 ++--
 src/main/scala/rules/Executor.scala           |  4 ++--
 .../scala/rules/PermissionSupporter.scala     | 19 +++++++++++++++++--
 3 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 610cc514e..a8be60cf4 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -791,7 +791,7 @@ object evaluator extends EvaluationRules {
         if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) {
           evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) =>
             eval(s1, ePerm, pve, v1)((s2, tPerm, v2) =>
-              v2.decider.assert(IsNonNegative(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
+              v2.decider.assert(IsPositive(tPerm)) {
                 case true =>
                   joiner.join[Term, Term](s2, v2)((s3, v3, QB) => {
                     val s4 = s3.incCycleCounter(predicate)
@@ -832,7 +832,7 @@ object evaluator extends EvaluationRules {
                         eval(s10, eIn, pve, v5)(QB)})})
                   })(join(v2.symbolConverter.toSort(eIn.typ), "joined_unfolding", s2.relevantQuantifiedVariables, v2))(Q)
                 case false =>
-                  createFailure(pve dueTo NegativePermission(ePerm), v2, s2)}))
+                  createFailure(pve dueTo NonPositivePermission(ePerm), v2, s2)}))
         } else {
           val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables)
           Q(s, unknownValue, v)
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 24d2c602d..33abac61b 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -507,7 +507,7 @@ object executor extends ExecutionRules {
         val pve = FoldFailed(fold)
         evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) =>
           eval(s1, ePerm, pve, v1)((s2, tPerm, v2) =>
-            permissionSupporter.assertNotNegative(s2, tPerm, ePerm, pve, v2)((s3, v3) => {
+            permissionSupporter.assertPositive(s2, tPerm, ePerm, pve, v2)((s3, v3) => {
               val wildcards = s3.constrainableARPs -- s1.constrainableARPs
               predicateSupporter.fold(s3, predicate, tArgs, tPerm, wildcards, pve, v3)(Q)})))
 
@@ -529,7 +529,7 @@ object executor extends ExecutionRules {
               s2.smCache
             }
 
-            permissionSupporter.assertNotNegative(s2, tPerm, ePerm, pve, v2)((s3, v3) => {
+            permissionSupporter.assertPositive(s2, tPerm, ePerm, pve, v2)((s3, v3) => {
               val wildcards = s3.constrainableARPs -- s1.constrainableARPs
               predicateSupporter.unfold(s3.copy(smCache = smCache1), predicate, tArgs, tPerm, wildcards, pve, v3, pa)(Q)
             })
diff --git a/src/main/scala/rules/PermissionSupporter.scala b/src/main/scala/rules/PermissionSupporter.scala
index 63cd54194..1dd0daae1 100644
--- a/src/main/scala/rules/PermissionSupporter.scala
+++ b/src/main/scala/rules/PermissionSupporter.scala
@@ -10,9 +10,9 @@ import viper.silver.ast
 import viper.silver.verifier.PartialVerificationError
 import viper.silicon.interfaces.VerificationResult
 import viper.silicon.state.State
-import viper.silicon.state.terms.{Term, perms, Var}
+import viper.silicon.state.terms.{Term, Var, perms}
 import viper.silicon.verifier.Verifier
-import viper.silver.verifier.reasons.NegativePermission
+import viper.silver.verifier.reasons.{NegativePermission, NonPositivePermission}
 
 object permissionSupporter extends SymbolicExecutionRules {
   def assertNotNegative(s: State, tPerm: Term, ePerm: ast.Exp, pve: PartialVerificationError, v: Verifier)
@@ -29,4 +29,19 @@ object permissionSupporter extends SymbolicExecutionRules {
         }
     }
   }
+
+  def assertPositive(s: State, tPerm: Term, ePerm: ast.Exp, pve: PartialVerificationError, v: Verifier)
+                    (Q: (State, Verifier) => VerificationResult)
+  : VerificationResult = {
+
+    tPerm match {
+      case k: Var if s.constrainableARPs.contains(k) =>
+        Q(s, v)
+      case _ =>
+        v.decider.assert(perms.IsPositive(tPerm)) {
+          case true => Q(s, v)
+          case false => createFailure(pve dueTo NonPositivePermission(ePerm), v, s)
+        }
+    }
+  }
 }

From 987be744b9ed09307e9f6f6b532c9ba6610bffd7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 23:56:58 +0200
Subject: [PATCH 37/58] Updated silver version

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 65ec3412b..e678cd731 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4
+Subproject commit e678cd731b4bc7dd7e9f79ae7627d08891158f2c

From d3f5d84379051dbe81c9204445015a239ffb7b0b Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 4 Oct 2023 23:58:10 +0200
Subject: [PATCH 38/58] Updated silver version

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index e678cd731..67fa15588 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit e678cd731b4bc7dd7e9f79ae7627d08891158f2c
+Subproject commit 67fa155884a51d17d25a496bda73d76b31a5c889

From fab9efe45076832265d59d3fa8ee6b801ed441d7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 5 Oct 2023 00:40:27 +0200
Subject: [PATCH 39/58] Updated silver version

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 67fa15588..820db76e9 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 67fa155884a51d17d25a496bda73d76b31a5c889
+Subproject commit 820db76e92646c57b180c7ccdc8dee0465118e62

From 6617d23eb5b4742f3afd08f4c26a7f58ebedd65d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Sat, 7 Oct 2023 00:55:04 +0200
Subject: [PATCH 40/58] Update submodules (#755)

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 65ec3412b..07dce2bf8 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4
+Subproject commit 07dce2bf8a90f6be9443ece6d1697b0e2767fb48

From 53cccb9c1a117b77c0a338c0cec29d5835825842 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 8 Oct 2023 00:53:41 +0200
Subject: [PATCH 41/58] Attempting to replace the current wand path condition
 workaround with something cleaner

---
 src/main/scala/decider/Decider.scala          | 18 +++++--
 src/main/scala/decider/PathConditions.scala   | 50 +++++++++++++++++++
 src/main/scala/rules/Evaluator.scala          |  4 +-
 src/main/scala/rules/Executor.scala           |  6 +--
 src/main/scala/rules/MagicWandSupporter.scala |  8 +--
 .../rules/MoreCompleteExhaleSupporter.scala   |  2 +-
 src/main/scala/rules/PredicateSupporter.scala |  2 +-
 src/main/scala/rules/Producer.scala           |  2 +-
 .../scala/rules/QuantifiedChunkSupport.scala  |  2 +-
 9 files changed, 76 insertions(+), 18 deletions(-)

diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index 145fcceb0..169a265d8 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -40,7 +40,8 @@ trait Decider {
   def setPathConditionMark(): Mark
 
   def assume(t: Term): Unit
-  def assume(ts: InsertionOrderedSet[Term], enforceAssumption: Boolean = false): Unit
+  def assumeDefinition(t: Term): Unit
+  def assume(ts: InsertionOrderedSet[Term], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit
   def assume(ts: Iterable[Term]): Unit
 
   def check(t: Term, timeout: Int): Boolean
@@ -209,23 +210,30 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       assume(InsertionOrderedSet(Seq(t)), false)
     }
 
+    override def assumeDefinition(t: Term): Unit =
+      assume(InsertionOrderedSet(Seq(t)), false, true)
+
     def assume(terms: Iterable[Term]): Unit =
       assume(InsertionOrderedSet(terms), false)
 
-    def assume(terms: InsertionOrderedSet[Term], enforceAssumption: Boolean = false): Unit = {
+    def assume(terms: InsertionOrderedSet[Term], enforceAssumption: Boolean = false, isDefinition: Boolean = false): Unit = {
       val filteredTerms =
         if (enforceAssumption) terms
         else terms filterNot isKnownToBeTrue
 
-      if (filteredTerms.nonEmpty) assumeWithoutSmokeChecks(filteredTerms)
+      if (filteredTerms.nonEmpty) assumeWithoutSmokeChecks(filteredTerms, isDefinition)
     }
 
-    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term]) = {
+    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term], isDefinition: Boolean = false) = {
       val assumeRecord = new DeciderAssumeRecord(terms)
       val sepIdentifier = symbExLog.openScope(assumeRecord)
 
       /* Add terms to Silicon-managed path conditions */
-      terms foreach pathConditions.add
+      if (isDefinition) {
+        terms foreach pathConditions.addDefinition
+      } else {
+        terms foreach pathConditions.add
+      }
 
       /* Add terms to the prover's assumptions */
       terms foreach prover.assume
diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 8f53ac589..1da350c53 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -24,8 +24,11 @@ trait RecordedPathConditions {
   def branchConditions: Stack[Term]
   def branchConditionExps: Stack[Option[ast.Exp]]
   def assumptions: InsertionOrderedSet[Term]
+  def definingAssumptions: InsertionOrderedSet[Term]
   def declarations: InsertionOrderedSet[Decl]
 
+  def definitionsOnly: RecordedPathConditions
+
   def contains(assumption: Term): Boolean
 
   def conditionalized: Seq[Term]
@@ -42,6 +45,7 @@ trait RecordedPathConditions {
 trait PathConditionStack extends RecordedPathConditions {
   def setCurrentBranchCondition(condition: Term, conditionExp: Option[ast.Exp]): Unit
   def add(assumption: Term): Unit
+  def addDefinition(assumption: Term): Unit
   def add(declaration: Decl): Unit
   def pushScope(): Unit
   def popScope(): Unit
@@ -64,17 +68,26 @@ private class PathConditionStackLayer
   private var _branchConditionExp: Option[Option[ast.Exp]] = None
   private var _globalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _nonGlobalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  private var _globalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _declarations: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   def branchCondition: Option[Term] = _branchCondition
   def branchConditionExp: Option[Option[ast.Exp]] = _branchConditionExp
   def globalAssumptions: InsertionOrderedSet[Term] = _globalAssumptions
+  def definingAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
   def nonGlobalAssumptions: InsertionOrderedSet[Term] = _nonGlobalAssumptions
   def declarations: InsertionOrderedSet[Decl] = _declarations
 
   def assumptions: InsertionOrderedSet[Term] = globalAssumptions ++ nonGlobalAssumptions
   def pathConditions: InsertionOrderedSet[Term] = assumptions ++ branchCondition
 
+  def definitionsOnly(): PathConditionStackLayer = {
+    val result = new PathConditionStackLayer
+    result._globalAssumptions = _globalDefiningAssumptions
+    result._declarations = _declarations
+    result
+  }
+
   def branchCondition_=(condition: Term): Unit = {
     assert(_branchCondition.isEmpty,
              s"Branch condition is already set (to ${_branchCondition.get}), "
@@ -104,6 +117,16 @@ private class PathConditionStackLayer
       _nonGlobalAssumptions += assumption
   }
 
+  def addDefinition(assumption: Term): Unit = {
+    assert(
+      !assumption.isInstanceOf[And],
+      s"Unexpectedly found a conjunction (should have been split): $assumption")
+
+    //assert(PathConditions.isGlobal(assumption))
+    _globalAssumptions += assumption
+    _globalDefiningAssumptions += assumption
+  }
+
   def add(declaration: Decl): Unit = _declarations += declaration
 
   def contains(pathCondition: Term): Boolean = {
@@ -134,6 +157,9 @@ private trait LayeredPathConditionStackLike {
   protected def assumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
     InsertionOrderedSet(layers.flatMap(_.assumptions)) // Note: Performance?
 
+  protected def definingAssumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
+    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+
   protected def declarations(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
@@ -199,12 +225,17 @@ private class DefaultRecordedPathConditions(from: Stack[PathConditionStackLayer]
   val branchConditions: Stack[Term] = branchConditions(from)
   val branchConditionExps: Stack[Option[ast.Exp]] = branchConditionExps(from)
   val assumptions: InsertionOrderedSet[Term] = assumptions(from)
+  val definingAssumptions: InsertionOrderedSet[Term] = definingAssumptions(from)
   val declarations: InsertionOrderedSet[Decl] = declarations(from)
 
   def contains(assumption: Term): Boolean = contains(from, assumption)
 
   val conditionalized: Seq[Term] = conditionalized(from)
 
+  def definitionsOnly(): RecordedPathConditions = {
+    new DefaultRecordedPathConditions(from.map(_.definitionsOnly))
+  }
+
   def quantified(quantifier: Quantifier,
                  qvars: Seq[Var],
                  triggers: Seq[Trigger],
@@ -248,6 +279,15 @@ private[decider] class LayeredPathConditionStack
     allAssumptions ++= tlcs
   }
 
+  def addDefinition(assumption: Term): Unit = {
+    /* TODO: Would be cleaner to not add assumptions that are already set as branch conditions */
+
+    val tlcs = assumption.topLevelConjuncts
+
+    tlcs foreach layers.head.addDefinition
+    allAssumptions ++= tlcs
+  }
+
   def add(declaration: Decl): Unit = {
     layers.head.add(declaration)
   }
@@ -311,6 +351,9 @@ private[decider] class LayeredPathConditionStack
   def declarations: InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
+  def definingAssumptions: InsertionOrderedSet[Term] =
+    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+
   def contains(assumption: Term): Boolean = allAssumptions.contains(assumption)
 
   def conditionalized: Seq[Term] = conditionalized(layers)
@@ -357,6 +400,13 @@ private[decider] class LayeredPathConditionStack
     clonedStack
   }
 
+  override def definitionsOnly: RecordedPathConditions = {
+    val result = duplicate()
+    result.layers = layers map (_.definitionsOnly())
+    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.definingAssumptions))
+    result
+  }
+
   override def toString: String =  {
     val sb = new StringBuilder(s"${this.getClass.getSimpleName}:\n")
     val sep = s" ${"-" * 10}\n"
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index d8688acc8..315ce2fac 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -171,7 +171,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints) = v.decider.freshARP()
-        v.decider.assume(tConstraints)
+        v.decider.assumeDefinition(tConstraints)
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
          *       from State.constrainableARPs (potentially inefficient, but should be sound).
@@ -292,7 +292,7 @@ object evaluator extends EvaluationRules {
       case ast.Let(x, e0, e1) =>
         eval(s, e0, pve, v)((s1, t0, v1) => {
           val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
-          v1.decider.assume(t === t0)
+          v1.decider.assumeDefinition(t === t0)
           val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
           eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
         })
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 69fe5e98a..e9607dc1d 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -339,7 +339,7 @@ object executor extends ExecutionRules {
                 val h3 = Heap(remainingChunks ++ otherChunks)
                 val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v2)
                 v1.decider.prover.comment("Definitional axioms for singleton-FVF's value")
-                v1.decider.assume(smValueDef)
+                v1.decider.assumeDefinition(smValueDef)
                 val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program)
                 if (s3.heapDependentTriggers.contains(field))
                   v1.decider.assume(FieldTrigger(field.name, sm, tRcvr))
@@ -374,7 +374,7 @@ object executor extends ExecutionRules {
           if (s.qpFields.contains(field)) {
             val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v)
             v.decider.prover.comment("Definitional axioms for singleton-FVF's value")
-            v.decider.assume(smValueDef)
+            v.decider.assumeDefinition(smValueDef)
             quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), p, sm, s.program)
           } else {
             BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), snap, p)
@@ -627,7 +627,7 @@ object executor extends ExecutionRules {
           *   reported by Silicon issue #328.
           */
          val t = v.decider.fresh(name, v.symbolConverter.toSort(typ))
-         v.decider.assume(t === rhs)
+         v.decider.assumeDefinition(t === rhs)
 
          t
      }
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index 8b509f3a6..1e5e05953 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -273,15 +273,15 @@ object magicWandSupporter extends SymbolicExecutionRules {
         // it is, we don't record (any further) path conditions.
         // TODO: Fix this. Might require a substantial redesign of Silicon's path conditions, though.
 
-        if (!v4.decider.checkSmoke()) {
-          conservedPcs = s5.conservedPcs.head :+ pcs
+        //if (!v4.decider.checkSmoke()) {
+          conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly
 
           conservedPcsStack =
             s5.conservedPcs.tail match {
               case empty @ Seq() => empty
               case head +: tail => (head ++ conservedPcs) +: tail
             }
-        }
+        //}
 
         val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs)
 
@@ -296,7 +296,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
           val (sm, smValueDef) =
             quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4)
           v4.decider.prover.comment("Definitional axioms for singleton-SM's value")
-          v4.decider.assume(smValueDef)
+          v4.decider.assumeDefinition(smValueDef)
           val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program)
           appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4)
           Success()
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 6abf20ff3..732e03fa7 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -114,7 +114,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     }
     val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
 
-    v.decider.assume(And(snapDefs))
+    v.decider.assumeDefinition(And(snapDefs))
 //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
 
     val s2 =
diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala
index da0661fe8..30d6ffc3b 100644
--- a/src/main/scala/rules/PredicateSupporter.scala
+++ b/src/main/scala/rules/PredicateSupporter.scala
@@ -72,7 +72,7 @@ object predicateSupporter extends PredicateSupportRules {
         val (sm, smValueDef) =
           quantifiedChunkSupporter.singletonSnapshotMap(s2, predicate, tArgs, predSnap, v1)
         v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
-        v1.decider.assume(smValueDef)
+        v1.decider.assumeDefinition(smValueDef)
         val ch =
           quantifiedChunkSupporter.createSingletonQuantifiedChunk(
             formalArgs, predicate, tArgs, tPerm, sm, s.program)
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index a29672f59..0edfb5bde 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -301,7 +301,7 @@ object producer extends ProductionRules {
             quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1)
           v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
           val definitionalAxiomMark = v1.decider.setPathConditionMark()
-          v1.decider.assume(smValueDef)
+          v1.decider.assumeDefinition(smValueDef)
           val conservedPcs =
             if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail
             else s1.conservedPcs
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 67211833f..69199735c 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -967,7 +967,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, resource, tArgs, tSnap, v)
     v.decider.prover.comment("Definitional axioms for singleton-SM's value")
     val definitionalAxiomMark = v.decider.setPathConditionMark()
-    v.decider.assume(smValueDef)
+    v.decider.assumeDefinition(smValueDef)
     val conservedPcs =
       if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail
       else s.conservedPcs

From 05a71462f92ce797e66bfcee19c958d1d9e12db6 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 10 Oct 2023 15:14:28 +0200
Subject: [PATCH 42/58] Added test in silver

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 07dce2bf8..769b09f70 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 07dce2bf8a90f6be9443ece6d1697b0e2767fb48
+Subproject commit 769b09f7071d2c97b50587dddbb7fce17fee1110

From 4d107f0fd9e356a853c4d393e3ab95b629c9c1d2 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 10 Oct 2023 15:17:28 +0200
Subject: [PATCH 43/58] Cleanup

---
 src/main/scala/rules/MagicWandSupporter.scala | 29 +++++++------------
 1 file changed, 10 insertions(+), 19 deletions(-)

diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index 1e5e05953..928faf062 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -261,27 +261,18 @@ object magicWandSupporter extends SymbolicExecutionRules {
         var conservedPcs: Vector[RecordedPathConditions] = Vector.empty
         var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs
 
-        // Do not record further path conditions if the current state is inconsistent.
-        // This is an ad-hoc workaround to mitigate the following problem: producing a wand's LHS
-        // and executing the packaging proof code can introduce definitional path conditions, e.g.
+        // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g.
         // new permission and snapshot maps, which are in general necessary to proceed after the
         // package statement, e.g. to know which permissions have been consumed.
-        // Since the current implementation doesn't properly differentiate between definitional
-        // and arbitrary path conditions, all path conditions are recorded — which is unsound.
-        // To somewhat improve the situation, such that "non-malevolent" usage of wands works
-        // as expected, we simply check if the current state is known to be inconsistent, and if
-        // it is, we don't record (any further) path conditions.
-        // TODO: Fix this. Might require a substantial redesign of Silicon's path conditions, though.
-
-        //if (!v4.decider.checkSmoke()) {
-          conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly
-
-          conservedPcsStack =
-            s5.conservedPcs.tail match {
-              case empty @ Seq() => empty
-              case head +: tail => (head ++ conservedPcs) +: tail
-            }
-        //}
+        // Here, we want to keep *only* the definitions, but no other path conditions.
+
+        conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly
+
+        conservedPcsStack =
+          s5.conservedPcs.tail match {
+            case empty @ Seq() => empty
+            case head +: tail => (head ++ conservedPcs) +: tail
+          }
 
         val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs)
 

From 3e146d882f97634d871806fbfa7bd622888d2ba8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 12 Oct 2023 11:16:45 +0200
Subject: [PATCH 44/58] update submodules (#758)

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 820db76e9..38fd6b0c1 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 820db76e92646c57b180c7ccdc8dee0465118e62
+Subproject commit 38fd6b0c133b14677a7eb4a56c6c5b8f40276db7

From df1428b6335e093d829b55d684ff8a94f826dea4 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Oct 2023 22:47:57 +0200
Subject: [PATCH 45/58] Remove restriction that disables MCE for function
 verification

---
 src/main/scala/rules/ChunkSupporter.scala | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala
index fe88e765b..7b8c2d3b4 100644
--- a/src/main/scala/rules/ChunkSupporter.scala
+++ b/src/main/scala/rules/ChunkSupporter.scala
@@ -108,8 +108,7 @@ object chunkSupporter extends ChunkSupportRules {
         Q(s1, h, optCh.flatMap(ch => Some(ch.snap)), v1))
     } else {
       executionFlowController.tryOrFail2[Heap, Option[Term]](s.copy(h = h), v)((s1, v1, QS) =>
-        // 2022-05-07 MHS: MoreCompleteExhale isn't yet integrated into function verification, hence the limitation to method verification
-        if (s.isMethodVerification && s1.moreCompleteExhale) {
+        if (s1.moreCompleteExhale) {
           moreCompleteExhaleSupporter.consumeComplete(s1, s1.h, resource, args, perms, ve, v1)((s2, h2, snap2, v2) => {
             QS(s2.copy(h = s.h), h2, snap2, v2)
           })
@@ -206,7 +205,7 @@ object chunkSupporter extends ChunkSupportRules {
 
     executionFlowController.tryOrFail2[Heap, Term](s.copy(h = h), v)((s1, v1, QS) => {
       val lookupFunction =
-        if (s.isMethodVerification && s1.moreCompleteExhale) moreCompleteExhaleSupporter.lookupComplete _
+        if (s1.moreCompleteExhale) moreCompleteExhaleSupporter.lookupComplete _
         else lookupGreedy _
       lookupFunction(s1, s1.h, resource, args, ve, v1)((s2, tSnap, v2) =>
         QS(s2.copy(h = s.h), s2.h, tSnap, v2))

From ba914dd3d7b46a9ff6cfeb2f14c4890e102f06f7 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Oct 2023 23:29:31 +0200
Subject: [PATCH 46/58] Adding MCE test with disjunctive aliasing in function
 and method

---
 .../disjunctiveAliasing.vpr                   | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 src/test/resources/moreCompleteExhale/disjunctiveAliasing.vpr

diff --git a/src/test/resources/moreCompleteExhale/disjunctiveAliasing.vpr b/src/test/resources/moreCompleteExhale/disjunctiveAliasing.vpr
new file mode 100644
index 000000000..a95bb5b45
--- /dev/null
+++ b/src/test/resources/moreCompleteExhale/disjunctiveAliasing.vpr
@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function fn(x: Ref, y: Ref, z: Ref): Int
+  requires acc(x.f) && acc(y.f)
+  requires (z == x) || (z == y)
+{
+  z.f
+}
+
+method m(x: Ref, y: Ref, z: Ref)
+  requires acc(x.f) && acc(y.f)
+  requires (z == x) || (z == y)
+{
+  var tmp: Int
+  tmp := z.f
+}
+

From 8b55d3d24174c171f63d85c3e1db8d36c2011d36 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Oct 2023 23:31:14 +0200
Subject: [PATCH 47/58] Pull non-global assumptions that are independent of
 quantified variables out of quantifier

---
 src/main/scala/decider/PathConditions.scala | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 8f53ac589..6cc9af88e 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -176,13 +176,24 @@ private trait LayeredPathConditionStackLike {
     val ignores = ignore.topLevelConjuncts
 
     for (layer <- layers) {
-      globals ++= layer.globalAssumptions
+      val actualBranchCondition = layer.branchCondition.getOrElse(True)
+      val relevantNonGlobals = layer.nonGlobalAssumptions -- ignores
+      val (trueNonGlobals, additionalGlobals) = if (qvars.forall(qv => !actualBranchCondition.contains(qv))) {
+        // The branch condition is independent of all quantified variables
+        // Any assumptions that are also independent of all quantified variables can be treated as global assumptions.
+        val (trueNonGlobals, unconditionalGlobals) = relevantNonGlobals.partition(a => qvars.exists(a.contains(_)))
+        (trueNonGlobals, unconditionalGlobals.map(Implies(actualBranchCondition, _)))
+      } else {
+        (relevantNonGlobals, Seq())
+      }
+
+      globals ++= layer.globalAssumptions ++ additionalGlobals
 
       nonGlobals :+=
         Quantification(
           quantifier,
           qvars,
-          Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)),
+          Implies(actualBranchCondition, And(trueNonGlobals)),
           triggers,
           name,
           isGlobal)

From ec367019ab28a59fcc0e5e1cbbd3521ca128c1b6 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Oct 2023 23:50:12 +0200
Subject: [PATCH 48/58] Added test

---
 .../resources/moreCompleteExhale/0557.vpr     | 71 +++++++++++++++++++
 1 file changed, 71 insertions(+)
 create mode 100644 src/test/resources/moreCompleteExhale/0557.vpr

diff --git a/src/test/resources/moreCompleteExhale/0557.vpr b/src/test/resources/moreCompleteExhale/0557.vpr
new file mode 100644
index 000000000..4dc907a95
--- /dev/null
+++ b/src/test/resources/moreCompleteExhale/0557.vpr
@@ -0,0 +1,71 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+// first version of the example
+
+domain ArrayDomain {}
+
+field val_int: Int
+field val_ref: Ref
+
+function idx_into(a: ArrayDomain, a_len: Int): Int
+function array_len(a: ArrayDomain): Int
+function to_domain(self: Ref): ArrayDomain
+  requires acc(Array(self), read$())
+
+function read$(): Perm
+  ensures none < result
+  ensures result < write
+
+predicate Array(self: Ref)
+predicate usize(self: Ref) {
+  acc(self.val_int, write)
+}
+
+method foo() {
+  var a: Ref
+  var a_len: Int
+  var _3: Ref
+  var unknown: Ref
+  var i: Ref
+  inhale acc(a.val_ref, write) && acc(Array(a.val_ref), write)
+
+  inhale acc(_3.val_ref, write) && acc(usize(unknown), read$()) // <- removing this makes it pass
+
+  exhale acc(a.val_ref, read$())
+
+  inhale acc(usize(i), write) && acc(a.val_ref, read$())
+
+  inhale (unfolding acc(usize(i), write) in
+      (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
+        !(q < i.val_int) ||
+        idx_into(to_domain(a.val_ref), q) <=
+        idx_into(to_domain(a.val_ref), i.val_int)))
+  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/557/)
+  assert (unfolding acc(usize(i), write) in
+      (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
+        !(q < i.val_int) ||
+        idx_into(to_domain(a.val_ref), q) <=
+        idx_into(to_domain(a.val_ref), i.val_int)))
+}
+
+
+// second version of the example
+
+function holds(a: Ref, b: Int): Bool
+
+method foo2() {
+  var a: Ref
+  var _3: Ref
+
+  inhale acc(a.val_ref, write)
+
+  inhale acc(_3.val_ref, write) // <- removing this makes it pass
+
+  exhale acc(a.val_ref, 1 / 2)
+  inhale acc(a.val_ref, 1 / 2)
+
+  inhale forall q: Int :: holds(a.val_ref, q)
+  assert forall q: Int :: holds(a.val_ref, q)
+}
\ No newline at end of file

From cd9e2b026a38084014d87c9c3b54b7e3a139480d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Oct 2023 23:58:22 +0200
Subject: [PATCH 49/58] Moved test

---
 .../{moreCompleteExhale/0557.vpr => issue387/jonas_viktor.vpr}  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename src/test/resources/{moreCompleteExhale/0557.vpr => issue387/jonas_viktor.vpr} (99%)

diff --git a/src/test/resources/moreCompleteExhale/0557.vpr b/src/test/resources/issue387/jonas_viktor.vpr
similarity index 99%
rename from src/test/resources/moreCompleteExhale/0557.vpr
rename to src/test/resources/issue387/jonas_viktor.vpr
index 4dc907a95..2859a762a 100644
--- a/src/test/resources/moreCompleteExhale/0557.vpr
+++ b/src/test/resources/issue387/jonas_viktor.vpr
@@ -42,7 +42,7 @@ method foo() {
         !(q < i.val_int) ||
         idx_into(to_domain(a.val_ref), q) <=
         idx_into(to_domain(a.val_ref), i.val_int)))
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/557/)
+  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/387/)
   assert (unfolding acc(usize(i), write) in
       (forall q: Int :: { idx_into(to_domain(a.val_ref), q) }
         !(q < i.val_int) ||

From b6ac0cf704cc53aa2244b905d65e71d91c9c0f99 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 13 Oct 2023 13:42:50 +0200
Subject: [PATCH 50/58] Changed test setup s.t. issue387 tests are tested with
 MCE on instead of off.

---
 src/test/scala/SiliconTests.scala                   | 2 +-
 src/test/scala/SiliconTestsMoreCompleteExhale.scala | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala
index 027bd3da2..1a8669c43 100644
--- a/src/test/scala/SiliconTests.scala
+++ b/src/test/scala/SiliconTests.scala
@@ -15,7 +15,7 @@ import viper.silver.verifier.Verifier
 
 class SiliconTests extends SilSuite {
   private val siliconTestDirectories =
-    Seq("consistency", "issue387")
+    Seq("consistency")
 
   private val silTestDirectories =
     Seq("all",
diff --git a/src/test/scala/SiliconTestsMoreCompleteExhale.scala b/src/test/scala/SiliconTestsMoreCompleteExhale.scala
index 0266bae68..910a66f92 100644
--- a/src/test/scala/SiliconTestsMoreCompleteExhale.scala
+++ b/src/test/scala/SiliconTestsMoreCompleteExhale.scala
@@ -7,7 +7,7 @@
 package viper.silicon.tests
 
 class SiliconTestsMoreCompleteExhale extends SiliconTests {
-  override val testDirectories: Seq[String] = Seq("moreCompleteExhale")
+  override val testDirectories: Seq[String] = Seq("moreCompleteExhale", "issue387")
 
  override val commandLineArguments: Seq[String] = Seq(
     "--timeout", "300" /* seconds */,

From 0e35d5d31f73b19b490cfd611ad7ed631a979079 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 13 Oct 2023 13:55:57 +0200
Subject: [PATCH 51/58] Separating global and non-global defining assumptions

---
 src/main/scala/decider/PathConditions.scala | 22 ++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 1da350c53..61b8b0c59 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -69,12 +69,14 @@ private class PathConditionStackLayer
   private var _globalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _nonGlobalAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _globalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  private var _nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private var _declarations: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   def branchCondition: Option[Term] = _branchCondition
   def branchConditionExp: Option[Option[ast.Exp]] = _branchConditionExp
   def globalAssumptions: InsertionOrderedSet[Term] = _globalAssumptions
-  def definingAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
+  def globalDefiningAssumptions: InsertionOrderedSet[Term] = _globalDefiningAssumptions
+  def nonGlobalDefiningAssumptions: InsertionOrderedSet[Term] = _nonGlobalDefiningAssumptions
   def nonGlobalAssumptions: InsertionOrderedSet[Term] = _nonGlobalAssumptions
   def declarations: InsertionOrderedSet[Decl] = _declarations
 
@@ -84,6 +86,7 @@ private class PathConditionStackLayer
   def definitionsOnly(): PathConditionStackLayer = {
     val result = new PathConditionStackLayer
     result._globalAssumptions = _globalDefiningAssumptions
+    result._nonGlobalDefiningAssumptions = _nonGlobalDefiningAssumptions
     result._declarations = _declarations
     result
   }
@@ -122,9 +125,13 @@ private class PathConditionStackLayer
       !assumption.isInstanceOf[And],
       s"Unexpectedly found a conjunction (should have been split): $assumption")
 
-    //assert(PathConditions.isGlobal(assumption))
-    _globalAssumptions += assumption
-    _globalDefiningAssumptions += assumption
+    if (PathConditions.isGlobal(assumption)) {
+      _globalAssumptions += assumption
+      _globalDefiningAssumptions += assumption
+    } else {
+      _nonGlobalAssumptions += assumption
+      _nonGlobalDefiningAssumptions += assumption
+    }
   }
 
   def add(declaration: Decl): Unit = _declarations += declaration
@@ -158,7 +165,7 @@ private trait LayeredPathConditionStackLike {
     InsertionOrderedSet(layers.flatMap(_.assumptions)) // Note: Performance?
 
   protected def definingAssumptions(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Term] =
-    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
 
   protected def declarations(layers: Stack[PathConditionStackLayer]): InsertionOrderedSet[Decl] =
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
@@ -352,7 +359,7 @@ private[decider] class LayeredPathConditionStack
     InsertionOrderedSet(layers.flatMap(_.declarations)) // Note: Performance?
 
   def definingAssumptions: InsertionOrderedSet[Term] =
-    InsertionOrderedSet(layers.flatMap(_.definingAssumptions)) // Note: Performance?
+    InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++ layers.flatMap(_.nonGlobalDefiningAssumptions)) // Note: Performance?
 
   def contains(assumption: Term): Boolean = allAssumptions.contains(assumption)
 
@@ -403,7 +410,8 @@ private[decider] class LayeredPathConditionStack
   override def definitionsOnly: RecordedPathConditions = {
     val result = duplicate()
     result.layers = layers map (_.definitionsOnly())
-    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.definingAssumptions))
+    result.allAssumptions = InsertionOrderedSet(layers.flatMap(_.globalDefiningAssumptions) ++
+      layers.flatMap(_.nonGlobalDefiningAssumptions))
     result
   }
 

From 94ce3dfb8e3e9d763d0e6cb70ec313369b43ea96 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 13 Oct 2023 14:43:45 +0200
Subject: [PATCH 52/58] Fixed definitionsOnly implementation for non-global
 definitions

---
 src/main/scala/decider/PathConditions.scala | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 61b8b0c59..93e5dcff7 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -86,6 +86,8 @@ private class PathConditionStackLayer
   def definitionsOnly(): PathConditionStackLayer = {
     val result = new PathConditionStackLayer
     result._globalAssumptions = _globalDefiningAssumptions
+    result._globalDefiningAssumptions = _globalDefiningAssumptions
+    result._nonGlobalAssumptions = _nonGlobalDefiningAssumptions
     result._nonGlobalDefiningAssumptions = _nonGlobalDefiningAssumptions
     result._declarations = _declarations
     result

From 3e4ccf7b69c13bd834deb9f403c35d6ca2eb86c9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 13 Oct 2023 14:50:53 +0200
Subject: [PATCH 53/58] More efficient check if path conditions are independent
 of quantified variables

---
 src/main/scala/decider/PathConditions.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala
index 6cc9af88e..8a5dd27a5 100644
--- a/src/main/scala/decider/PathConditions.scala
+++ b/src/main/scala/decider/PathConditions.scala
@@ -178,10 +178,10 @@ private trait LayeredPathConditionStackLike {
     for (layer <- layers) {
       val actualBranchCondition = layer.branchCondition.getOrElse(True)
       val relevantNonGlobals = layer.nonGlobalAssumptions -- ignores
-      val (trueNonGlobals, additionalGlobals) = if (qvars.forall(qv => !actualBranchCondition.contains(qv))) {
+      val (trueNonGlobals, additionalGlobals) = if (!actualBranchCondition.existsDefined{ case t if qvars.contains(t) => }) {
         // The branch condition is independent of all quantified variables
         // Any assumptions that are also independent of all quantified variables can be treated as global assumptions.
-        val (trueNonGlobals, unconditionalGlobals) = relevantNonGlobals.partition(a => qvars.exists(a.contains(_)))
+        val (trueNonGlobals, unconditionalGlobals) = relevantNonGlobals.partition(a => a.existsDefined{ case t if qvars.contains(t) => })
         (trueNonGlobals, unconditionalGlobals.map(Implies(actualBranchCondition, _)))
       } else {
         (relevantNonGlobals, Seq())

From 42e0d8a5523c7280779d56dded3ab43891a13634 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sat, 14 Oct 2023 16:13:29 +0200
Subject: [PATCH 54/58] Incorporated review feedback, also turning off
 moreJoins for function preconditions, since that occasionally breaks things

---
 src/main/scala/rules/Brancher.scala           |   4 +-
 src/main/scala/rules/Consumer.scala           | 122 ++++++++----------
 src/main/scala/rules/Evaluator.scala          |  24 ++--
 src/main/scala/rules/Executor.scala           |   6 +-
 src/main/scala/rules/Producer.scala           |  16 +--
 src/main/scala/state/State.scala              |  27 ++--
 .../scala/verifier/DefaultMainVerifier.scala  |   7 +-
 7 files changed, 96 insertions(+), 110 deletions(-)

diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
index b2ab162f0..f482a2eae 100644
--- a/src/main/scala/rules/Brancher.scala
+++ b/src/main/scala/rules/Brancher.scala
@@ -23,7 +23,6 @@ trait BranchingRules extends SymbolicExecutionRules {
              condition: Term,
              conditionExp: Option[ast.Exp],
              v: Verifier,
-             sequentialOnly: Boolean = false,
              fromShortCircuitingAnd: Boolean = false)
             (fTrue: (State, Verifier) => VerificationResult,
              fFalse: (State, Verifier) => VerificationResult)
@@ -35,7 +34,6 @@ object brancher extends BranchingRules {
              condition: Term,
              conditionExp: Option[ast.Exp],
              v: Verifier,
-             sequentialOnly: Boolean = false,
              fromShortCircuitingAnd: Boolean = false)
             (fThen: (State, Verifier) => VerificationResult,
              fElse: (State, Verifier) => VerificationResult)
@@ -66,7 +64,7 @@ object brancher extends BranchingRules {
       || skipPathFeasibilityCheck
       || !v.decider.check(condition, Verifier.config.checkTimeout()))
 
-    val parallelizeElseBranch = s.parallelizeBranches && !sequentialOnly && executeThenBranch && executeElseBranch
+    val parallelizeElseBranch = s.parallelizeBranches && executeThenBranch && executeElseBranch
 
 //    val additionalPaths =
 //      if (executeThenBranch && exploreFalseBranch) 1
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index cc49ca5cc..0da3269b7 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -183,44 +183,10 @@ object consumer extends ConsumptionRules {
       v.logger.debug("hR = " + s.reserveHeaps.map(v.stateFormatter.format).mkString("", ",\n     ", ""))
 
     val consumed = a match {
-      case imp @ ast.Implies(e0, a0) if !a.isPure && Verifier.config.moreJoins() =>
+      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
         val uidImplies = v.symbExLog.openScope(impliesRecord)
-
-        evaluator.eval(s, e0, pve, v)((s1, t0, v1) =>
-          joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) =>
-            branch(s1, t0, Some(e0), v1, true)(
-              (s2, v2) => consumeR(s2, h, a0, pve, v2)((s3, h1, t1, v3) => {
-                v.symbExLog.closeScope(uidImplies)
-                QB(s3, (h1, t1), v3)
-              }),
-              (s2, v2) => {
-                v.symbExLog.closeScope(uidImplies)
-                QB(s2, (h, Unit), v2)
-              })
-          )(entries => {
-            val s2 = entries match {
-              case Seq(entry) => // One branch is dead
-                (entry.s, entry.data)
-              case Seq(entry1, entry2) => // Both branches are alive
-                // Here we merge additional data collected in each branch.
-                // We assume that entry1.pcs is negation of entry2.pcs.
-                val mergedData = (
-                  // The partially consumed heap is merged based on the corresponding branch conditions of each branch.
-                  State.mergeHeap(
-                    entry1.data._1, And(entry1.pathConditions.branchConditions),
-                    entry2.data._1, And(entry2.pathConditions.branchConditions),
-                  ),
-                  Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
-                )
-                (entry1.pathConditionAwareMerge(entry2, v1), mergedData)
-              case _ =>
-                sys.error(s"Unexpected join data entries: $entries")}
-            s2
-          })((s4, data, v4) => {
-            Q(s4, data._1, data._2, v4)
-          })
-        )
+        consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, pve, v)(Q)
 
       case imp @ ast.Implies(e0, a0) if !a.isPure =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
@@ -237,43 +203,10 @@ object consumer extends ConsumptionRules {
               Q(s2, h, Unit, v2)
             }))
 
-      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && Verifier.config.moreJoins() =>
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
-
-        eval(s, e0, pve, v)((s1, t0, v1) =>
-          joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) => {
-            branch(s1, t0, Some(e0), v1, true)(
-              (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => {
-                v3.symbExLog.closeScope(uidCondExp)
-                QB(s3, (h1, t1), v3)
-              }),
-              (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => {
-                v3.symbExLog.closeScope(uidCondExp)
-                QB(s3, (h1, t1), v3)
-              }))
-          })(entries => {
-            val s2 = entries match {
-              case Seq(entry) => // One branch is dead
-                (entry.s, entry.data)
-              case Seq(entry1, entry2) => // Both branches are alive
-                val mergedData = (
-                  State.mergeHeap(
-                    entry1.data._1, And(entry1.pathConditions.branchConditions),
-                    entry2.data._1, And(entry2.pathConditions.branchConditions),
-                  ),
-                  // Asume that entry1.pcs is inverse of entry2.pcs
-                  Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
-                )
-                (entry1.pathConditionAwareMerge(entry2, v1), mergedData)
-              case _ =>
-                sys.error(s"Unexpected join data entries: $entries")}
-            s2
-          })((s4, data, v4) => {
-            Q(s4, data._1, data._2, v4)
-          })
-        )
-
+        consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, pve, v)(Q)
 
       case ite @ ast.CondExp(e0, a1, a2) if !a.isPure =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
@@ -530,6 +463,53 @@ object consumer extends ConsumptionRules {
     consumed
   }
 
+  private def consumeConditionalTlcMoreJoins(s: State, h: Heap, e0: ast.Exp, a1: ast.Exp, a2: Option[ast.Exp], scopeUid: Int,
+                                             pve: PartialVerificationError, v: Verifier)
+                                            (Q: (State, Heap, Term, Verifier) => VerificationResult)
+                                            : VerificationResult = {
+    eval(s, e0, pve, v)((s1, t0, v1) =>
+      joiner.join[(Heap, Term), (Heap, Term)](s1, v1, resetState = false)((s1, v1, QB) => {
+        branch(s1.copy(parallelizeBranches = false), t0, Some(e0), v1)(
+          (s2, v2) =>
+            consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a1, pve, v2)((s3, h1, t1, v3) => {
+            v3.symbExLog.closeScope(scopeUid)
+            QB(s3, (h1, t1), v3)
+          }),
+          (s2, v2) =>
+            a2 match {
+              case Some(a2) => consumeR(s2.copy(parallelizeBranches = s1.parallelizeBranches), h, a2, pve, v2)((s3, h1, t1, v3) => {
+                v3.symbExLog.closeScope(scopeUid)
+                QB(s3, (h1, t1), v3)
+              })
+              case None =>
+                v2.symbExLog.closeScope(scopeUid)
+                QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (h, Unit), v2)
+            })
+      })(entries => {
+        val s2 = entries match {
+          case Seq(entry) => // One branch is dead
+            (entry.s, entry.data)
+          case Seq(entry1, entry2) => // Both branches are alive
+            val mergedData = (
+              State.mergeHeap(
+                entry1.data._1, And(entry1.pathConditions.branchConditions),
+                entry2.data._1, And(entry2.pathConditions.branchConditions),
+              ),
+              // Asume that entry1.pcs is inverse of entry2.pcs
+              Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
+            )
+            (entry1.pathConditionAwareMerge(entry2, v1), mergedData)
+          case _ =>
+            sys.error(s"Unexpected join data entries: $entries")
+        }
+        s2
+      })((s4, data, v4) => {
+        Q(s4, data._1, data._2, v4)
+      })
+    )
+  }
+
+
   private def evalAndAssert(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier)
                            (Q: (State, Term, Verifier) => VerificationResult)
                            : VerificationResult = {
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 27a31fc36..b3576e074 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -330,9 +330,9 @@ object evaluator extends EvaluationRules {
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
         eval(s, e0, pve, v)((s1, t0, v1) =>
           joiner.join[Term, Term](s1, v1)((s2, v2, QB) =>
-            brancher.branch(s2, t0, Some(e0), v2, true)(
-              (s3, v3) => eval(s3, e1, pve, v3)(QB),
-              (s3, v3) => eval(s3, e2, pve, v3)(QB))
+            brancher.branch(s2.copy(parallelizeBranches = false), t0, Some(e0), v2)(
+              (s3, v3) => eval(s3.copy(parallelizeBranches = s2.parallelizeBranches), e1, pve, v3)(QB),
+              (s3, v3) => eval(s3.copy(parallelizeBranches = s2.parallelizeBranches), e2, pve, v3)(QB))
           )(entries => {
             /* TODO: If branch(...) took orElse-continuations that are executed if a branch is dead, then then
                 comparisons with t0/Not(t0) wouldn't be necessary. */
@@ -762,7 +762,8 @@ object evaluator extends EvaluationRules {
                                  * of the recorded snapshots - which is wrong (probably only
                                  * incomplete).
                                  */
-                             smDomainNeeded = true)
+                             smDomainNeeded = true,
+                             moreJoins = false)
             consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
@@ -776,7 +777,8 @@ object evaluator extends EvaluationRules {
                                recordVisited = s2.recordVisited,
                                functionRecorder = fr5,
                                smDomainNeeded = s2.smDomainNeeded,
-                               hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption)
+                               hackIssue387DisablePermissionConsumption = s.hackIssue387DisablePermissionConsumption,
+                               moreJoins = s2.moreJoins)
               QB(s5, tFApp, v3)})
             /* TODO: The join-function is heap-independent, and it is not obvious how a
              *       joined snapshot could be defined and represented
@@ -1091,9 +1093,9 @@ object evaluator extends EvaluationRules {
                          : VerificationResult = {
 
     joiner.join[Term, Term](s, v)((s1, v1, QB) =>
-      brancher.branch(s1, tLhs, eLhs, v1, true, fromShortCircuitingAnd)(
-        (s2, v2) => eval(s2, eRhs, pve, v2)(QB),
-        (s2, v2) => QB(s2, True, v2))
+      brancher.branch(s1.copy(parallelizeBranches = false), tLhs, eLhs, v1, fromShortCircuitingAnd = fromShortCircuitingAnd)(
+        (s2, v2) => eval(s2.copy(parallelizeBranches = s1.parallelizeBranches), eRhs, pve, v2)(QB),
+        (s2, v2) => QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), True, v2))
     )(entries => {
       assert(entries.length <= 2)
       val s1 = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s))
@@ -1595,9 +1597,9 @@ object evaluator extends EvaluationRules {
         case `stop` => Q(s1, t0, v1) // Done, if last expression was true/false for or/and (optimisation)
         case _ =>
           joiner.join[Term, Term](s1, v1)((s2, v2, QB) =>
-            brancher.branch(s2, t0, Some(viper.silicon.utils.ast.BigAnd(exps)), v2, true, true) _ tupled swapIfAnd(
-              (s3, v3) => QB(s3, constructor(Seq(t0)), v3),
-              (s3, v3) => evalSeqShortCircuit(constructor, s3, exps.tail, pve, v3)(QB))
+            brancher.branch(s2.copy(parallelizeBranches = false), t0, Some(viper.silicon.utils.ast.BigAnd(exps)), v2, fromShortCircuitingAnd = true) _ tupled swapIfAnd(
+              (s3, v3) => QB(s3.copy(parallelizeBranches = s2.parallelizeBranches), constructor(Seq(t0)), v3),
+              (s3, v3) => evalSeqShortCircuit(constructor, s3.copy(parallelizeBranches = s2.parallelizeBranches), exps.tail, pve, v3)(QB))
             ){case Seq(ent) =>
                 (ent.s, ent.data)
               case Seq(ent1, ent2) =>
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index af5e38ad1..88e469e1c 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -65,9 +65,9 @@ object executor extends ExecutionRules {
             /* Using branch(...) here ensures that the edge condition is recorded
              * as a branch condition on the pathcondition stack.
              */
-            brancher.branch(s2, tCond, Some(ce.condition), v1, true)(
+            brancher.branch(s2.copy(parallelizeBranches = false), tCond, Some(ce.condition), v1)(
               (s3, v3) =>
-                exec(s3, ce.target, ce.kind, v3, joinPoint)((s4, v4) => {
+                exec(s3.copy(parallelizeBranches = s2.parallelizeBranches), ce.target, ce.kind, v3, joinPoint)((s4, v4) => {
                   v4.symbExLog.closeScope(sepIdentifier)
                   Q(s4, v4)
                 }),
@@ -111,7 +111,7 @@ object executor extends ExecutionRules {
       case (Seq(), _) => Q(s, v)
       case (Seq(edge), _) => follow(s, edge, v, joinPoint)(Q)
       case (Seq(edge1, edge2), Some(newJoinPoint)) if
-          Verifier.config.moreJoins() &&
+          s.moreJoins &&
           // Can't directly match type because of type erasure ...
           edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
           edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 9f8eb9a0c..01ae6dd5f 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -214,15 +214,15 @@ object producer extends ProductionRules {
       continuation(if (state.exhaleExt) state.copy(reserveHeaps = state.h +: state.reserveHeaps.drop(1)) else state, verifier)
 
     val produced = a match {
-      case imp @ ast.Implies(e0, a0) if !a.isPure && Verifier.config.moreJoins() =>
+      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "produce")
         val uidImplies = v.symbExLog.openScope(impliesRecord)
 
         eval(s, e0, pve, v)((s1, t0, v1) =>
           // The type arguments here are Null because there is no need to pass any join data.
           joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
-            branch(s1, t0, Some(e0), v1, true)(
-              (s2, v2) => produceR(s2, sf, a0, pve, v2)((s3, v3) => {
+            branch(s1.copy(parallelizeBranches = false), t0, Some(e0), v1)(
+              (s2, v2) => produceR(s2.copy(parallelizeBranches = s1.parallelizeBranches), sf, a0, pve, v2)((s3, v3) => {
                 v3.symbExLog.closeScope(uidImplies)
                 QB(s3, null, v3)
               }),
@@ -233,7 +233,7 @@ object producer extends ProductionRules {
                  * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`.
                  */
                 v2.symbExLog.closeScope(uidImplies)
-                QB(s2, null, v2)
+                QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), null, v2)
               })
           )(entries => {
             val s2 = entries match {
@@ -267,19 +267,19 @@ object producer extends ProductionRules {
                 Q(s2, v2)
             }))
 
-      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && Verifier.config.moreJoins() =>
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "produce")
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
 
         eval(s, e0, pve, v)((s1, t0, v1) =>
           // The type arguments here are Null because there is no need to pass any join data.
           joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s1, v1, QB) =>
-            branch(s1, t0, Some(e0), v1, true)(
-              (s2, v2) => produceR(s2, sf, a1, pve, v2)((s3, v3) => {
+            branch(s1.copy(parallelizeBranches = false), t0, Some(e0), v1)(
+              (s2, v2) => produceR(s2.copy(parallelizeBranches = s1.parallelizeBranches), sf, a1, pve, v2)((s3, v3) => {
                 v3.symbExLog.closeScope(uidCondExp)
                 QB(s3, null, v3)
               }),
-              (s2, v2) => produceR(s2, sf, a2, pve, v2)((s3, v3) => {
+              (s2, v2) => produceR(s2.copy(parallelizeBranches = s1.parallelizeBranches), sf, a2, pve, v2)((s3, v3) => {
                 v3.symbExLog.closeScope(uidCondExp)
                 QB(s3, null, v3)
               }))
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 0b7325fee..0833fffc9 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -69,7 +69,8 @@ final case class State(g: Store = Store(),
                        retryLevel: Int = 0,
                        /* ast.Field, ast.Predicate, or MagicWandIdentifier */
                        heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
-                       moreCompleteExhale: Boolean = false)
+                       moreCompleteExhale: Boolean = false,
+                       moreJoins: Boolean = false)
     extends Mergeable[State] {
 
   val isMethodVerification: Boolean = {
@@ -157,7 +158,7 @@ object State {
                  ssCache1, hackIssue387DisablePermissionConsumption1,
                  qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
                  predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
-                 moreCompleteExhale) =>
+                 moreCompleteExhale, moreJoins) =>
 
         /* Decompose state s2: most values must match those of s1 */
         s2 match {
@@ -182,7 +183,7 @@ object State {
                      ssCache2, `hackIssue387DisablePermissionConsumption1`,
                      `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, `smDomainNeeded1`,
                      `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
-                     moreCompleteExhale2) =>
+                     moreCompleteExhale2, `moreJoins`) =>
 
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2
@@ -307,7 +308,7 @@ object State {
       ssCache1, hackIssue387DisablePermissionConsumption1,
       qpFields1, qpPredicates1, qpMagicWands1, smCache1, pmCache1, smDomainNeeded1,
       predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
-      moreCompleteExhale) =>
+      moreCompleteExhale, moreJoins) =>
 
         /* Decompose state s2: most values must match those of s1 */
         s2 match {
@@ -330,14 +331,15 @@ object State {
           reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
           ssCache2, `hackIssue387DisablePermissionConsumption1`,
           `qpFields1`, `qpPredicates1`, `qpMagicWands1`, smCache2, pmCache2, smDomainNeeded2,
-          `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`, moreCompleteExhale2) =>
+          `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
+          moreCompleteExhale2, `moreJoins`) =>
 
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2
             val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2
             val constrainableARPs3 = constrainableARPs1 ++ constrainableARPs2
 
-            val smDomainNeeded3 = smDomainNeeded1 || smDomainNeeded2 // TODO: Use AND or OR to merge?
+            val smDomainNeeded3 = smDomainNeeded1 || smDomainNeeded2
 
             val conditions1 = And(pc1.branchConditions)
             val conditions2 = And(pc2.branchConditions)
@@ -381,13 +383,11 @@ object State {
               Some(mergeHeap(heap1, cond1, heap2, cond2))
             }))
 
-            // TODO: InvariantContexts should most likely be the same
             assert(invariantContexts1.length == invariantContexts2.length)
             val invariantContexts3 = invariantContexts1
               .zip(invariantContexts2)
               .map({case (h1, h2) => mergeHeap(h1, conditions1, h2, conditions2)})
 
-            // TODO: Workout situations in which reserve heaps differ
             assert(reserveHeaps1.length == reserveHeaps2.length)
             val reserveHeaps3 = reserveHeaps1
               .zip(reserveHeaps2)
@@ -399,14 +399,17 @@ object State {
               .zip(conservedPcs1)
               .map({case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct})
 
+            val ssCache3 = ssCache1 ++ ssCache2
+            val smCache3 = smCache1.union(smCache2)
+            val pmCache3 = pmCache1 ++ pmCache2
+
             val s3 = s1.copy(functionRecorder = functionRecorder3,
                              possibleTriggers = possibleTriggers3,
                              triggerExp = triggerExp3,
                              constrainableARPs = constrainableARPs3,
-                             // TODO: Merge caches.
-                             ssCache = Map.empty,
-                             smCache = SnapshotMapCache.empty,
-                             pmCache = Map.empty,
+                             ssCache = ssCache3,
+                             smCache = smCache3,
+                             pmCache = pmCache3,
                              g = g3,
                              h = h3,
                              oldHeaps = oldHeaps3,
diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala
index 4e3809788..c2d41d192 100644
--- a/src/main/scala/verifier/DefaultMainVerifier.scala
+++ b/src/main/scala/verifier/DefaultMainVerifier.scala
@@ -317,6 +317,7 @@ class DefaultMainVerifier(config: Config,
         }
       case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete
     }
+    val moreJoins = Verifier.config.moreJoins() && member.isInstanceOf[ast.Method]
 
     State(program = program,
           functionData = functionData,
@@ -328,7 +329,8 @@ class DefaultMainVerifier(config: Config,
           predicateFormalVarMap = predSnapGenerator.formalVarMap,
           currentMember = Some(member),
           heapDependentTriggers = resourceTriggers,
-          moreCompleteExhale = mce)
+          moreCompleteExhale = mce,
+          moreJoins = moreJoins)
   }
 
   private def createInitialState(@unused cfg: SilverCfg,
@@ -349,7 +351,8 @@ class DefaultMainVerifier(config: Config,
       qpMagicWands = quantifiedMagicWands,
       predicateSnapMap = predSnapGenerator.snapMap,
       predicateFormalVarMap = predSnapGenerator.formalVarMap,
-      moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete)
+      moreCompleteExhale = Verifier.config.exhaleMode == ExhaleMode.MoreComplete,
+      moreJoins = Verifier.config.moreJoins())
   }
 
   private def excludeMethod(method: ast.Method) = (

From ae780f07d12785173c0bfd491dbb0018eb4b84bc Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Tue, 17 Oct 2023 15:36:45 +0200
Subject: [PATCH 55/58] update silver automatically

---
 .github/workflows/update-submodules.yml | 65 +++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 .github/workflows/update-submodules.yml

diff --git a/.github/workflows/update-submodules.yml b/.github/workflows/update-submodules.yml
new file mode 100644
index 000000000..bf72e2513
--- /dev/null
+++ b/.github/workflows/update-submodules.yml
@@ -0,0 +1,65 @@
+# This Source Code Form is subject to the terms of the Mozilla Public
+# License, v. 2.0. If a copy of the MPL was not distributed with this
+# file, You can obtain one at http://mozilla.org/MPL/2.0/.
+#
+# Copyright (c) 2011-2022 ETH Zurich.
+
+name: Update Submodules
+
+on:
+  workflow_dispatch: # allow to manually trigger this workflow
+  schedule:
+    - cron: '0 6 * * *' # run every day at 06:00 UTC
+
+jobs:
+  # Update silver and create a PR if there are any changes
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out the repo
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+
+      - name: Get current commits
+        run: echo "PREV_SILVER_REF=$(git -C silver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Update Silver submodule
+        run: git checkout master && git pull
+        working-directory: silver
+
+      - name: Get new commits
+        run: echo "CUR_SILVER_REF=$(git -C silver rev-parse HEAD)" >> $GITHUB_ENV
+
+      - name: Create PR body
+        run: |
+          if [[ "${{ env.PREV_SILVER_REF }}" != "${{ env.CUR_SILVER_REF }}" ]]; then
+            echo 'PR_BODY_LINE=* Updates Silver from `${{ env.PREV_SILVER_REF }}` to `${{ env.CUR_SILVER_REF }}`.' >> $GITHUB_ENV
+          else
+            echo 'PR_BODY_LINE=' >> $GITHUB_ENV
+          fi
+
+      - name: Open a pull request
+        id: pr
+        uses: peter-evans/create-pull-request@v4
+        if: (env.PREV_SILVER_REF != env.CUR_SILVER_REF)
+        with:
+          # Use viper-admin's token to workaround a restriction of GitHub.
+          # See: https://github.com/peter-evans/create-pull-request/issues/48
+          token: ${{ secrets.UPDATE_SILVER }}
+          commit-message: Updates submodules
+          title: Update Submodules
+          branch: auto-update-submodules
+          delete-branch: true
+          labels: |
+            automated pr
+          body: |
+            ${{ env.PR_BODY_LINE1 }}
+
+      - name: Enable auto-merge of PR
+        uses: peter-evans/create-or-update-comment@v2
+        if: (env.PREV_SILVER_REF != env.CUR_SILVER_REF)
+        with:
+          token: ${{ secrets.UPDATE_SILVER }}
+          issue-number: ${{ steps.pr.outputs.pull-request-number }}"
+          body: bors merge

From bbfe9b821dccb083404d3e56af39c1818f34c80a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 17 Oct 2023 18:15:54 +0200
Subject: [PATCH 56/58] Validation and a better explanation for the
 --numberOfParallelVerifiers command line option.

---
 src/main/scala/Config.scala | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 068bcc03e..9dc28bb7a 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -684,8 +684,10 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
   )(singleArgConverter(mode => StateConsolidationMode(mode.toInt)))
 
   val numberOfParallelVerifiers: ScallopOption[Int] = opt[Int]("numberOfParallelVerifiers",
-    descr = (  "Number of verifiers run in parallel. This number plus one is the number of provers "
-             + s"run in parallel (default: ${Runtime.getRuntime.availableProcessors()})"),
+    descr = ( "Number of verifiers (and therefore also prover instances) run in parallel for method verification." +
+              "A value of 1 leads to sequential method verification. " +
+              "Functions and predicates are always verified sequentially on a separate prover instance. " +
+             s"Default: ${Runtime.getRuntime.availableProcessors()}"),
     default = Some(Runtime.getRuntime.availableProcessors()),
     noshort = true
   )
@@ -815,6 +817,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => Right(())
   }
 
+  validateOpt(numberOfParallelVerifiers) {
+    case Some(n) if n <= 0 => Left(s"Number of parallel verifiers must be positive, but $n was provided")
+    case _ => Right()
+  }
+
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)

From 36c611ff0a222ed98e33ef9b28eb7dc4eac13182 Mon Sep 17 00:00:00 2001
From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Date: Wed, 18 Oct 2023 08:51:38 +0200
Subject: [PATCH 57/58] Updates submodules (#763)

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 769b09f70..09956bec6 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 769b09f7071d2c97b50587dddbb7fce17fee1110
+Subproject commit 09956bec6c03a0eb7333ec651ebfd7145a3e339e

From 118f5a663ec3c4fab4c1d3008c7b5a07b9690a82 Mon Sep 17 00:00:00 2001
From: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com>
Date: Thu, 19 Oct 2023 10:34:59 +0200
Subject: [PATCH 58/58] Updates submodules (#764)

Co-authored-by: Dspil <Dspil@users.noreply.github.com>
---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 09956bec6..ce5523d0c 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 09956bec6c03a0eb7333ec651ebfd7145a3e339e
+Subproject commit ce5523d0c902f5ff61c8af49f80cd180f758c5b5