From 11660fdc55b762036b743e4eec0535a640680487 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 7 Mar 2024 14:20:02 -0800
Subject: [PATCH] Reset predecessors before focusing (#856)

There are two calls to `FocusAndSplit` in Boogie. Before one, there was
already a call to `ResetPredecessors`, but not before the other. Now
they both work on an implementation where the `Predecessors` attributes
has been reset.

---------

Co-authored-by: Remy Willems <rwillems@amazon.com>
---
 Source/Directory.Build.props               | 2 +-
 Source/ExecutionEngine/ExecutionEngine.cs  | 1 +
 Source/VCGeneration/ConditionGeneration.cs | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
index f1aee22ed..6ca40334e 100644
--- a/Source/Directory.Build.props
+++ b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.1.1</Version>
+    <Version>3.1.2</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 18202b600..33840642c 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -724,6 +724,7 @@ public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program) {
           out var gotoCmdOrigins,
           out var modelViewInfo);
 
+        VerificationConditionGenerator.ResetPredecessors(run.Implementation.Blocks);
         var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList();
         for (var index = 0; index < splits.Count; index++) {
           var split = splits[index];
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index c79c6f1d8..a4ac161a4 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -578,7 +578,7 @@ protected Block GenerateUnifiedExit(Implementation impl, Dictionary<TransferCmd,
       #endregion
     }
 
-    internal static void ResetPredecessors(List<Block> blocks)
+    public static void ResetPredecessors(List<Block> blocks)
     {
       Contract.Requires(blocks != null);
       foreach (Block b in blocks)