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 01/32] 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 02/32] 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 3b3b4befb716fc9df4606909ff25162a5c8563a8 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 17 Jul 2023 09:57:25 +0000
Subject: [PATCH 03/32] Update silver submodule

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

diff --git a/silver b/silver
index a28b06fde..c2c1b1183 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit a28b06fdee4947b49e1765fb3596e7bf44a0d757
+Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d

From 064be39d20d092bd5b057178fe7b7983d71d4875 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Wed, 19 Jul 2023 14:04:54 +0000
Subject: [PATCH 04/32] Update silver submodule

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

diff --git a/silver b/silver
index c2c1b1183..cafd01198 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d
+Subproject commit cafd01198d92fb5941e8444df26500d6c41d135a

From 8e3190bc05a110e636aa3882504165de23ab2e19 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Thu, 20 Jul 2023 19:10:52 +0000
Subject: [PATCH 05/32] Update silver submodule

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

diff --git a/silver b/silver
index cafd01198..7f1385bfc 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit cafd01198d92fb5941e8444df26500d6c41d135a
+Subproject commit 7f1385bfc648e3e8296e60d1d7fc46aeaade3261

From e1d9cd5b4ae0a1a3a2c2a7f34d42ad7265e14110 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 27 Jul 2023 00:46:09 +0200
Subject: [PATCH 06/32] Allowing counterexamples wiht MCE on demand option

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

diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 141efe9a4..068bcc03e 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -807,8 +807,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
 
   validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
     case (Some(_), Some(false), None) |
-         (Some(_), Some(_), Some(ExhaleMode.Greedy)) |
-         (Some(_), Some(_), Some(ExhaleMode.MoreCompleteOnDemand)) =>
+         (Some(_), Some(_), Some(ExhaleMode.Greedy)) =>
       Left(s"Option ${counterexample.name} requires setting "
         + s"${exhaleModeOption.name} to 1 (more complete exhale)")
     case (_, Some(true), Some(m)) if m != ExhaleMode.MoreComplete =>

From 7fe4d9f0919dca2b503fff9967eb1e0c4ba748b3 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Wed, 2 Aug 2023 01:56:36 +0000
Subject: [PATCH 07/32] Update silver submodule

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

diff --git a/silver b/silver
index 7f1385bfc..87f83ec95 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 7f1385bfc648e3e8296e60d1d7fc46aeaade3261
+Subproject commit 87f83ec957c78062837f85547d326c90efb3eaad

From 7251bc6ddc657ee00bc2997d6fc3672ef46c70f5 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Thu, 3 Aug 2023 14:34:55 +0000
Subject: [PATCH 08/32] Update silver submodule

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

diff --git a/silver b/silver
index 87f83ec95..9f5b214fb 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 87f83ec957c78062837f85547d326c90efb3eaad
+Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536

From c9a680043d39175f19c7c112a08c46bcd5429bf5 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Fri, 4 Aug 2023 14:49:13 +0000
Subject: [PATCH 09/32] Update silver submodule

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

diff --git a/silver b/silver
index 9f5b214fb..04df2df94 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536
+Subproject commit 04df2df94858240769c851e2a1aba43c35976232

From e07b53607720d114883df8d9cb68dd1ac4982eb0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 12:58:03 +0200
Subject: [PATCH 10/32] Don't always stop verification on FatalResult (fixes
 issue #740)

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

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 24d2c602d..d15793a22 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -203,9 +203,9 @@ object executor extends ExecutionRules {
                                               v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */)
                   v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
                   edgeConditions.foldLeft(Success(): VerificationResult) {
-                    case (fatalResult: FatalResult, _) => fatalResult
+                    case (result, _) if !result.continueVerification => result
                     case (intermediateResult, eCond) =>
-                      intermediateResult && executionFlowController.locally(s1, v1)((s2, v2) => {
+                      intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => {
                         eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) =>
                           Success())})}})})
             && executionFlowController.locally(s, v)((s0, v0) => {
@@ -213,10 +213,10 @@ object executor extends ExecutionRules {
                 consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")
                   phase1data.foldLeft(Success(): VerificationResult) {
-                    case (fatalResult: FatalResult, _) => fatalResult
+                    case (result, _) if !result.continueVerification => result
                     case (intermediateResult, (s1, pcs, ff1)) => /* [BRANCH-PARALLELISATION] ff1 */
                       val s2 = s1.copy(invariantContexts = sLeftover.h +: s1.invariantContexts)
-                      intermediateResult && executionFlowController.locally(s2, v1)((s3, v2) => {
+                      intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => {
                         v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
                         v2.decider.assume(pcs.assumptions)
                         v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)

From eebbc61e6faaa62cb7d69c6185f566eb5f361fa9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 14 Aug 2023 13:03:42 +0200
Subject: [PATCH 11/32] Added test in silver

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

diff --git a/silver b/silver
index 9f5b214fb..f03ccf8f2 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 9f5b214fb27c7aba0f48901a02f80704915ea536
+Subproject commit f03ccf8f28f0dc733dbda162b4c17b98132952c9

From fb0f19e7e5fd64c1810b94227402b24770107115 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 14 Aug 2023 18:23:00 +0000
Subject: [PATCH 12/32] Update silver submodule

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

diff --git a/silver b/silver
index 04df2df94..501f1ecef 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 04df2df94858240769c851e2a1aba43c35976232
+Subproject commit 501f1ecefb156db539de9ec68f5673f5ca3f4817

From 2885c620b89d6e6c4eb2ea51c635931f85739a87 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 14 Aug 2023 19:42:24 +0000
Subject: [PATCH 13/32] Update silver submodule

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

diff --git a/silver b/silver
index 18e73c604..c3cf35a73 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 18e73c604d22db62261902ef8b0daa6a0bcd754f
+Subproject commit c3cf35a73a1292d0b3c9f60039ca691c5b874ca6

From 246f0193cdef2555145fa9a1dda0e5fc93e779dd Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 15 Aug 2023 00:32:10 +0200
Subject: [PATCH 14/32] Silicon frontend classes for API usage

---
 silver                       |  2 +-
 src/main/scala/Silicon.scala | 21 ++++++++++++++++++++-
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/silver b/silver
index 04df2df94..afaf4523a 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 04df2df94858240769c851e2a1aba43c35976232
+Subproject commit afaf4523a8429873c4f160713a22764162b12b21
diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala
index ebab80e34..987ae59f1 100644
--- a/src/main/scala/Silicon.scala
+++ b/src/main/scala/Silicon.scala
@@ -14,7 +14,7 @@ import ch.qos.logback.classic.{Level, Logger}
 import com.typesafe.scalalogging.LazyLogging
 import org.slf4j.LoggerFactory
 import viper.silver.ast
-import viper.silver.frontend.{DefaultStates, SilFrontend}
+import viper.silver.frontend.{DefaultStates, MinimalViperFrontendAPI, SilFrontend, ViperFrontendAPI}
 import viper.silver.reporter._
 import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier}
 import viper.silicon.interfaces.Failure
@@ -377,6 +377,25 @@ class SiliconFrontend(override val reporter: Reporter,
   }
 }
 
+/**
+  * Silicon "frontend" for use by actual Viper frontends.
+  * Performs consistency check and verification.
+  * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
+  */
+class SiliconFrontendAPI(override val reporter: Reporter,
+                         override implicit val logger: Logger = ViperStdOutLogger("SiliconFrontendAPI", "INFO").get)
+  extends SiliconFrontend(reporter, logger) with ViperFrontendAPI
+
+/**
+  * Silicon "frontend" for use by actual Viper frontends.
+  * Performs only verification (no consistency check).
+  * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
+  */
+class MinimalSiliconFrontendAPI(override val reporter: Reporter,
+                                override implicit val logger: Logger = ViperStdOutLogger("MinimalSiliconFrontendAPI", "INFO").get)
+  extends SiliconFrontend(reporter, logger) with MinimalViperFrontendAPI
+
+
 object SiliconRunner extends SiliconRunnerInstance {
   def main(args: Array[String]): Unit = {
     runMain(args)

From 184af09e0cdf8adbf5e982d58cb81bf0e65297f9 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 17 Aug 2023 13:30:37 +0200
Subject: [PATCH 15/32] Removed superfluous logger arguments

---
 src/main/scala/Silicon.scala | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala
index 987ae59f1..a9b1001cf 100644
--- a/src/main/scala/Silicon.scala
+++ b/src/main/scala/Silicon.scala
@@ -382,18 +382,16 @@ class SiliconFrontend(override val reporter: Reporter,
   * Performs consistency check and verification.
   * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
   */
-class SiliconFrontendAPI(override val reporter: Reporter,
-                         override implicit val logger: Logger = ViperStdOutLogger("SiliconFrontendAPI", "INFO").get)
-  extends SiliconFrontend(reporter, logger) with ViperFrontendAPI
+class SiliconFrontendAPI(override val reporter: Reporter)
+  extends SiliconFrontend(reporter) with ViperFrontendAPI
 
 /**
   * Silicon "frontend" for use by actual Viper frontends.
   * Performs only verification (no consistency check).
   * See [[viper.silver.frontend.ViperFrontendAPI]] for usage information.
   */
-class MinimalSiliconFrontendAPI(override val reporter: Reporter,
-                                override implicit val logger: Logger = ViperStdOutLogger("MinimalSiliconFrontendAPI", "INFO").get)
-  extends SiliconFrontend(reporter, logger) with MinimalViperFrontendAPI
+class MinimalSiliconFrontendAPI(override val reporter: Reporter)
+  extends SiliconFrontend(reporter) with MinimalViperFrontendAPI
 
 
 object SiliconRunner extends SiliconRunnerInstance {

From c2b3f1635abbb504e0fa200f594b5b4401f52789 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Thu, 17 Aug 2023 15:46:08 +0000
Subject: [PATCH 16/32] Update silver submodule

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

diff --git a/silver b/silver
index c3cf35a73..8bd26f55d 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit c3cf35a73a1292d0b3c9f60039ca691c5b874ca6
+Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4

From 8fdb9d50b91d3db58d2302ce84f64e2efb8a6e41 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 17 Aug 2023 17:48:32 +0200
Subject: [PATCH 17/32] Updating silver

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

diff --git a/silver b/silver
index afaf4523a..8bd26f55d 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit afaf4523a8429873c4f160713a22764162b12b21
+Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4

From cb319dee9508059f8c8f93f064294230ee413fce Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Thu, 17 Aug 2023 17:54:48 +0000
Subject: [PATCH 18/32] Update silver submodule

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

diff --git a/silver b/silver
index 8bd26f55d..c5ce6cd1a 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 8bd26f55d8b60e5e3a7bc09d6e52b996265a6dc4
+Subproject commit c5ce6cd1a12c778bd254c2f7d10ba44654f08378

From d4c8d849278dd2f4e96ec6d85d13a93a89bb1163 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 21 Aug 2023 15:36:49 +0000
Subject: [PATCH 19/32] Update silver submodule

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

diff --git a/silver b/silver
index c5ce6cd1a..0f16c1f02 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit c5ce6cd1a12c778bd254c2f7d10ba44654f08378
+Subproject commit 0f16c1f025a67de84f1ba7511aa19e19ae8e59eb

From da038b8232dbfdbda221d621e3eb4355cefd335e Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 21 Aug 2023 22:41:13 +0200
Subject: [PATCH 20/32] Fixing issue #744

---
 silver                                                   | 2 +-
 src/main/scala/supporters/functions/FunctionData.scala   | 9 +++++++--
 .../supporters/functions/FunctionVerificationUnit.scala  | 4 ++--
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/silver b/silver
index 0f16c1f02..c7d57c2e0 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 0f16c1f025a67de84f1ba7511aa19e19ae8e59eb
+Subproject commit c7d57c2e09eaec9279827098c93ec3a400e42702
diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
index 8629a2168..7e0b3cab2 100644
--- a/src/main/scala/supporters/functions/FunctionData.scala
+++ b/src/main/scala/supporters/functions/FunctionData.scala
@@ -266,17 +266,22 @@ class FunctionData(val programFunction: ast.Function,
       Forall(arguments, body, allTriggers)})
   }
 
-  lazy val preconditionPropagationAxiom: Seq[Term] = {
+  lazy val bodyPreconditionPropagationAxiom: Seq[Term] = {
     val pre = preconditionFunctionApplication
     val bodyPreconditions = if (programFunction.body.isDefined) optBody.map(translatedBody => {
       val body = Implies(pre, FunctionPreconditionTransformer.transform(translatedBody, program))
       Forall(arguments, body, Seq(Trigger(functionApplication)))
     }) else None
+    bodyPreconditions.toSeq
+  }
+
+  lazy val postPreconditionPropagationAxiom: Seq[Term] = {
+    val pre = preconditionFunctionApplication
     val postPreconditions = if (programFunction.posts.nonEmpty) {
       val bodyBindings: Map[Var, Term] = Map(formalResult -> limitedFunctionApplication)
       val bodies = translatedPosts.map(tPost => Let(bodyBindings, Implies(pre, FunctionPreconditionTransformer.transform(tPost, program))))
       bodies.map(b => Forall(arguments, b, Seq(Trigger(limitedFunctionApplication))))
     } else Seq()
-    bodyPreconditions.toSeq ++ postPreconditions
+    postPreconditions
   }
 }
diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
index 71a2117dd..32d15c436 100644
--- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
+++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
@@ -172,10 +172,10 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
           emitAndRecordFunctionAxioms(data.limitedAxiom)
           emitAndRecordFunctionAxioms(data.triggerAxiom)
           emitAndRecordFunctionAxioms(data.postAxiom.toSeq: _*)
+          emitAndRecordFunctionAxioms(data.postPreconditionPropagationAxiom: _*)
           this.postConditionAxioms = this.postConditionAxioms ++ data.postAxiom.toSeq
 
           if (function.body.isEmpty) {
-            emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
             result1
           } else {
             /* Phase 2: Verify the function's postcondition */
@@ -186,7 +186,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
                 data.verificationFailures = data.verificationFailures :+ fatalResult
               case _ =>
                 emitAndRecordFunctionAxioms(data.definitionalAxiom.toSeq: _*)
-                emitAndRecordFunctionAxioms(data.preconditionPropagationAxiom.toSeq: _*)
+                emitAndRecordFunctionAxioms(data.bodyPreconditionPropagationAxiom: _*)
             }
 
             result1 && result2

From 084d7178c95a0ac4e0e3d5c869dd04b09397ce5e Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 21 Aug 2023 22:18:31 +0000
Subject: [PATCH 21/32] Update silver submodule

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

diff --git a/silver b/silver
index c7d57c2e0..56b74d1ab 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit c7d57c2e09eaec9279827098c93ec3a400e42702
+Subproject commit 56b74d1abcf7cfe4f9268f8df1bf015a736fd30c

From 854b84c06cdb7e85d27540a782a849f5d880889c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Tue, 22 Aug 2023 17:35:22 +0200
Subject: [PATCH 22/32] Reset the number of errors before verifying a new
 method

---
 src/main/scala/supporters/MethodSupporter.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala
index e78253f3f..a99cbb17e 100644
--- a/src/main/scala/supporters/MethodSupporter.scala
+++ b/src/main/scala/supporters/MethodSupporter.scala
@@ -72,6 +72,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
           new java.io.File(s"${Verifier.config.tempDirectory()}/${method.name}.dot"))
       }
 
+      errorsReportedSoFar.set(0)
       val result =
         /* Combined the well-formedness check and the execution of the body, which are two separate
          * rules in Smans' paper.

From fa5810e6d30237fc1ec05e1b13dbfc3ba2d2a906 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Fri, 25 Aug 2023 15:14:08 +0000
Subject: [PATCH 23/32] Update silver submodule

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

diff --git a/silver b/silver
index 56b74d1ab..65ec3412b 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 56b74d1abcf7cfe4f9268f8df1bf015a736fd30c
+Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4

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 24/32] 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 67fc9a33c535de7184c8a9255736202e8816ba75 Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Fri, 15 Sep 2023 17:35:51 +0200
Subject: [PATCH 25/32] benchmarking mods

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

diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
index 625ca4918..0597ff5d2 100644
--- a/src/main/scala/rules/Brancher.scala
+++ b/src/main/scala/rules/Brancher.scala
@@ -56,13 +56,13 @@ object brancher extends BranchingRules {
     /* True if the then-branch is to be explored */
     val executeThenBranch = (
          skipPathFeasibilityCheck
-      || !v.decider.check(negatedCondition, Verifier.config.checkTimeout()))
+      ||{v.decider.prover.comment("branching!!!") ; !v.decider.check(negatedCondition, Verifier.config.checkTimeout())} || true)
 
     /* False if the then-branch is to be explored */
     val executeElseBranch = (
          !executeThenBranch /* Assumes that ast least one branch is feasible */
       || skipPathFeasibilityCheck
-      || !v.decider.check(condition, Verifier.config.checkTimeout()))
+      || {v.decider.prover.comment("branching!!!") ; !v.decider.check(condition, Verifier.config.checkTimeout())} || true)
 
     val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch
 

From 1982e7358a3c29e36a270a0e88db080a4516aaa0 Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Fri, 15 Sep 2023 17:38:34 +0200
Subject: [PATCH 26/32] Revert "benchmarking mods"

This reverts commit 67fc9a33c535de7184c8a9255736202e8816ba75.
---
 src/main/scala/rules/Brancher.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
index 0597ff5d2..625ca4918 100644
--- a/src/main/scala/rules/Brancher.scala
+++ b/src/main/scala/rules/Brancher.scala
@@ -56,13 +56,13 @@ object brancher extends BranchingRules {
     /* True if the then-branch is to be explored */
     val executeThenBranch = (
          skipPathFeasibilityCheck
-      ||{v.decider.prover.comment("branching!!!") ; !v.decider.check(negatedCondition, Verifier.config.checkTimeout())} || true)
+      || !v.decider.check(negatedCondition, Verifier.config.checkTimeout()))
 
     /* False if the then-branch is to be explored */
     val executeElseBranch = (
          !executeThenBranch /* Assumes that ast least one branch is feasible */
       || skipPathFeasibilityCheck
-      || {v.decider.prover.comment("branching!!!") ; !v.decider.check(condition, Verifier.config.checkTimeout())} || true)
+      || !v.decider.check(condition, Verifier.config.checkTimeout()))
 
     val parallelizeElseBranch = s.parallelizeBranches && !s.underJoin && executeThenBranch && executeElseBranch
 

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 27/32] 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 28/32] 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 29/32] 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 30/32] 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 31/32] 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 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 32/32] 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