fix: Skip empty splits (#965)

boogie-org · Oct 14, 2024 · ff43b61 · ff43b61
1 parent 398413d
commit ff43b61
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 24 deletions.
diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -100,7 +100,7 @@ procedure Procedure(y: int)
 
     // The implicit return at the end gets a separate VC.
     // first split is empty. Maybe it can be optimized away
-    Assert.AreEqual(5, tasks.Count);
+    Assert.AreEqual(4, tasks.Count);
 
     var outcomes = new List<SolverOutcome> { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
     for (var index = 0; index < outcomes.Count; index++)

diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs
@@ -21,7 +21,8 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
         IsolateAttributeOnAssertsHandler.GetParts(options, withoutIsolatedJumps, createPart);
     
       var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions);
-      return isolatedJumps.Concat(isolatedAssertions).Concat(splitParts);
+      var splits = isolatedJumps.Concat(isolatedAssertions).Concat(splitParts).Where(s => s.Asserts.Any()).ToList();
+      return splits.Any() ? splits : new List<ManualSplit> { focussedPart };
     });
     return result;
   }

diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
@@ -3,18 +3,18 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying Ex ...
-// CHECK:      checking split 1/12 .*
-// CHECK:      checking split 2/12 .*
-// CHECK:      checking split 3/12 .*
-// CHECK:      checking split 4/12 .*
+// CHECK:      checking split 1/11 .*
+// CHECK:      checking split 2/11 .*
+// CHECK:      checking split 3/11 .*
+// CHECK:      checking split 4/11 .*
 // CHECK:      --> split #4 done,  \[.* s\] Invalid
-// CHECK:      checking split 5/12 .*
-// CHECK:      checking split 6/12 .*
-// CHECK:      checking split 7/12 .*
-// CHECK:      checking split 8/12 .*
-// CHECK:      checking split 9/12 .*
-// CHECK:      checking split 10/12 .*
-// CHECK:      checking split 11/12 .*
+// CHECK:      checking split 5/11 .*
+// CHECK:      checking split 6/11 .*
+// CHECK:      checking split 7/11 .*
+// CHECK:      checking split 8/11 .*
+// CHECK:      checking split 9/11 .*
+// CHECK:      checking split 10/11 .*
+// CHECK:      checking split 11/11 .*
 // CHECK-L: SplitOnEveryAssert.bpl(31,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)

diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl
@@ -3,18 +3,18 @@
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 
 // CHECK: Verifying DoTheSplitting ...
-// CHECK:      checking split 1/12.*
-// CHECK:      checking split 2/12.*
-// CHECK:      checking split 3/12.*
-// CHECK:      checking split 4/12.*
+// CHECK:      checking split 1/11.*
+// CHECK:      checking split 2/11.*
+// CHECK:      checking split 3/11.*
+// CHECK:      checking split 4/11.*
 // CHECK:      --> split #4 done,  \[.* s\] Invalid
-// CHECK:      checking split 5/12.*
-// CHECK:      checking split 6/12.*
-// CHECK:      checking split 7/12.*
-// CHECK:      checking split 8/12.*
-// CHECK:      checking split 9/12.*
-// CHECK:      checking split 10/12.*
-// CHECK:      checking split 11/12.*
+// CHECK:      checking split 5/11.*
+// CHECK:      checking split 6/11.*
+// CHECK:      checking split 7/11.*
+// CHECK:      checking split 8/11.*
+// CHECK:      checking split 9/11.*
+// CHECK:      checking split 10/11.*
+// CHECK:      checking split 11/11.*
 // CHECK-L: SplitOnEveryAssert.bpl(36,5): Error: this assertion could not be proved
 
 // Verify the second procedure is NOT split. .* is necessary to match the blank line in-between.