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 @@ - 3.1.1 + 3.1.2 net6.0 false Boogie 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 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 blocks) + public static void ResetPredecessors(List blocks) { Contract.Requires(blocks != null); foreach (Block b in blocks)