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>
boogie-org · Mar 7, 2024 · 11660fd · 11660fd
1 parent 9b83c3a
commit 11660fd
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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)