From c1db5a29940e41af685ec6d5c68c73ca837161c9 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 2 Oct 2024 16:38:24 +0200
Subject: [PATCH] Update test files

---
 Source/VCGeneration/Splits/Split.cs           | 10 ++++----
 .../intro-nonblocking.bpl.expect              |  1 -
 .../regression-tests/left-mover.bpl.expect    |  1 -
 .../non-interference-1.bpl.expect             |  1 -
 .../non-interference-2.bpl.expect             |  2 --
 .../pa-noninterference-check.bpl.expect       |  1 -
 .../regression-tests/parallel1.bpl.expect     |  1 -
 .../regression-tests/parallel6.bpl.expect     |  1 -
 .../pending-async-1.bpl.expect                |  1 -
 ...ding-async-noninterference-fail.bpl.expect |  1 -
 .../regression-tests/refinement.bpl.expect    |  5 ----
 .../regression-tests/refinement2.bpl.expect   |  4 ----
 .../yield-invariant-fails.bpl.expect          |  1 -
 Test/commandline/SplitOnEveryAssert.bpl       | 24 +++++++++----------
 Test/test0/SplitOnEveryAssert.bpl             | 24 +++++++++----------
 Test/test2/Structured.bpl.expect              |  1 -
 16 files changed, 29 insertions(+), 50 deletions(-)

diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
index f9c7292e7..9930e6ecc 100644
--- a/Source/VCGeneration/Splits/Split.cs
+++ b/Source/VCGeneration/Splits/Split.cs
@@ -484,7 +484,7 @@ void ComputeBlockSetsHelper(Block b, bool allowSmall)
         }
       }
 
-      void ComputeBlockSets(bool allowSmall)
+      private void ComputeBlockSets(bool allowSmall)
       {
         protectedFromAssertToAssume.Clear();
         keepAtAll.Clear();
@@ -494,12 +494,12 @@ void ComputeBlockSets(bool allowSmall)
 
         if (assertToAssume)
         {
-          foreach (Block b in allowSmall ? Blocks : bigBlocks)
+          foreach (var block in allowSmall ? Blocks : bigBlocks)
           {
-            Contract.Assert(b != null);
-            if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock)))
+            Contract.Assert(block != null);
+            if (ComputeReachableNodes(block).Contains(cce.NonNull(splitBlock)))
             {
-              keepAtAll.Add(b);
+              keepAtAll.Add(block);
             }
           }
 
diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
index 1a747e1d9..08c401b27 100644
--- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect
+++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect
@@ -1,5 +1,4 @@
 intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed
 Execution trace:
-    (0,0): init
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect
index 44ada71cb..383a2cd10 100644
--- a/Test/civl/regression-tests/left-mover.bpl.expect
+++ b/Test/civl/regression-tests/left-mover.bpl.expect
@@ -10,6 +10,5 @@ Execution trace:
     left-mover.bpl(6,24): inline$inc$0$Return
 left-mover.bpl(26,24): Error: Cooperation check for block failed
 Execution trace:
-    (0,0): init
 
 Boogie program verifier finished with 3 verified, 3 errors
diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect
index 9ed2f19b1..be24ba16a 100644
--- a/Test/civl/regression-tests/non-interference-1.bpl.expect
+++ b/Test/civl/regression-tests/non-interference-1.bpl.expect
@@ -2,6 +2,5 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-1.bpl(7,3): anon0
     non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/civl/regression-tests/non-interference-2.bpl.expect b/Test/civl/regression-tests/non-interference-2.bpl.expect
index c1176c36d..4bbae5629 100644
--- a/Test/civl/regression-tests/non-interference-2.bpl.expect
+++ b/Test/civl/regression-tests/non-interference-2.bpl.expect
@@ -2,10 +2,8 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(7,3): anon0
     non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(34,3): anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 
 Boogie program verifier finished with 2 verified, 2 errors
diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect
index b97bf307f..55715916a 100644
--- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect
+++ b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect
@@ -1,6 +1,5 @@
 pa-noninterference-check.bpl(26,1): Error: Non-interference check failed
 Execution trace:
-    (0,0): init
     pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0
     pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return
 
diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect
index 4b52e2854..0bc33ffe1 100644
--- a/Test/civl/regression-tests/parallel1.bpl.expect
+++ b/Test/civl/regression-tests/parallel1.bpl.expect
@@ -2,6 +2,5 @@ parallel1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     parallel1.bpl(7,3): anon0
     parallel1.bpl(12,5): inline$AtomicIncr$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/civl/regression-tests/parallel6.bpl.expect b/Test/civl/regression-tests/parallel6.bpl.expect
index 0ff7beb24..9a6a6e2be 100644
--- a/Test/civl/regression-tests/parallel6.bpl.expect
+++ b/Test/civl/regression-tests/parallel6.bpl.expect
@@ -7,6 +7,5 @@ Execution trace:
     parallel6.bpl(11,5): anon0_0
     parallel6.bpl(30,7): inline$atomic_incr$2$anon0
     parallel6.bpl(30,7): inline$atomic_incr$3$anon0
-    (0,0): Civl_ReturnChecker
 
 Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect
index 86c6fbf94..5e0a35e06 100644
--- a/Test/civl/regression-tests/pending-async-1.bpl.expect
+++ b/Test/civl/regression-tests/pending-async-1.bpl.expect
@@ -5,7 +5,6 @@ Execution trace:
     pending-async-1.bpl(51,3): anon0$1
     pending-async-1.bpl(11,9): inline$B$1$anon0
     pending-async-1.bpl(51,3): anon0$2
-    (0,0): Civl_ReturnChecker
 pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized
 Execution trace:
     pending-async-1.bpl(67,3): anon0
diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect
index 29a3c680e..d6951c016 100644
--- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect
+++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect
@@ -1,6 +1,5 @@
 pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed
 Execution trace:
-    (0,0): init
     pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0
     pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return
 
diff --git a/Test/civl/regression-tests/refinement.bpl.expect b/Test/civl/regression-tests/refinement.bpl.expect
index 4974958b5..7203ec2a4 100644
--- a/Test/civl/regression-tests/refinement.bpl.expect
+++ b/Test/civl/regression-tests/refinement.bpl.expect
@@ -5,13 +5,11 @@ Execution trace:
     refinement.bpl(10,3): anon0$1
     refinement.bpl(10,3): anon0_0
     refinement.bpl(58,5): inline$INCR$1$anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action
 Execution trace:
     refinement.bpl(18,3): anon0
     refinement.bpl(64,5): inline$DECR$0$anon0
     refinement.bpl(18,3): anon0$1
-    (0,0): Civl_RefinementChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
     refinement.bpl(18,3): anon0
@@ -19,11 +17,9 @@ Execution trace:
     refinement.bpl(18,3): anon0$1
     refinement.bpl(18,3): anon0_0
     refinement.bpl(58,5): inline$INCR$0$anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement.bpl(41,1): anon0
-    (0,0): Civl_ReturnChecker
 refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement.bpl(46,3): anon0
@@ -32,6 +28,5 @@ Execution trace:
     refinement.bpl(46,3): anon0_0
     refinement.bpl(48,3): anon2_LoopHead
     refinement.bpl(58,5): inline$INCR$1$anon0
-    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 3 verified, 5 errors
diff --git a/Test/civl/regression-tests/refinement2.bpl.expect b/Test/civl/regression-tests/refinement2.bpl.expect
index 3005f0993..24cb32f73 100644
--- a/Test/civl/regression-tests/refinement2.bpl.expect
+++ b/Test/civl/regression-tests/refinement2.bpl.expect
@@ -1,15 +1,11 @@
 refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement2.bpl(16,5): anon0
-    (0,0): Civl_call_refinement_4
     refinement2.bpl(27,28): inline$atomic_nop$0$Return
-    (0,0): Civl_ReturnChecker
 refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement2.bpl(16,5): anon0
-    (0,0): Civl_call_refinement_3
     refinement2.bpl(22,7): inline$atomic_incr$0$anon0
     refinement2.bpl(19,28): inline$atomic_incr$0$Return
-    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 1 verified, 2 errors
diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect
index 093836a59..8bab02145 100644
--- a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect
+++ b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect
@@ -2,6 +2,5 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed
 Execution trace:
     yield-invariant-fails.bpl(11,5): anon0
     yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0
-    (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
index 2e3878802..f65fd1203 100644
--- 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/11 .*
-// CHECK:      checking split 2/11 .*
-// CHECK:      checking split 3/11 .*
-// CHECK:      --> split #3 done,  \[.* s\] Invalid
-// CHECK:      checking split 4/11 .*
-// 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:      checking split 1/12 .*
+// CHECK:      checking split 2/12 .*
+// CHECK:      checking split 3/12 .*
+// CHECK:      checking split 4/12 .*
+// 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-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
index c883fb50c..d1313c7c9 100644
--- 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/11.*
-// CHECK:      checking split 2/11.*
-// CHECK:      checking split 3/11.*
-// CHECK:      --> split #3 done,  \[.* s\] Invalid
-// CHECK:      checking split 4/11.*
-// 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:      checking split 1/12.*
+// CHECK:      checking split 2/12.*
+// CHECK:      checking split 3/12.*
+// CHECK:      checking split 4/12.*
+// 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-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.
diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect
index a349c0d87..22c885b42 100644
--- a/Test/test2/Structured.bpl.expect
+++ b/Test/test2/Structured.bpl.expect
@@ -22,6 +22,5 @@ Execution trace:
     Structured.bpl(355,3): anon4_LoopHead
     Structured.bpl(358,7): anon4_LoopBody
     Structured.bpl(361,7): anon5_LoopBody
-    (0,0): anon3
 
 Boogie program verifier finished with 16 verified, 4 errors