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] 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)")