From 75f26a3ae59bfdfff17f1d2c682820ca7a30628a Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Wed, 31 Jul 2024 13:44:32 +0200
Subject: [PATCH] Fixes

---
 Test/civl/samples/treiber-stack.bpl     |  2 +-
 Test/commandline/SplitOnEveryAssert.bpl | 24 ++++++++++++------------
 Test/test0/MaxKeepGoingSplits.bpl       |  2 +-
 Test/test0/MaxSplits.bpl                |  2 +-
 4 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl
index b9ae5c918..b9e426474 100644
--- a/Test/civl/samples/treiber-stack.bpl
+++ b/Test/civl/samples/treiber-stack.bpl
@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert -trace "%s" > "%t"
+// RUN: %parallel-boogie -lib:base -lib:node -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype LocPiece { Left(), Right() }
diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
index 605492ced..1751a4d99 100644
--- a/Test/commandline/SplitOnEveryAssert.bpl
+++ b/Test/commandline/SplitOnEveryAssert.bpl
@@ -3,19 +3,19 @@
 // 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/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:      checking split 12/12, .*
+// 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 12/12 .*
 // CHECK-L: SplitOnEveryAssert.bpl(32,5): Error: this assertion could not be proved
 
 procedure Ex() returns (y: int)
diff --git a/Test/test0/MaxKeepGoingSplits.bpl b/Test/test0/MaxKeepGoingSplits.bpl
index 3cc9de23e..2b9c40686 100644
--- a/Test/test0/MaxKeepGoingSplits.bpl
+++ b/Test/test0/MaxKeepGoingSplits.bpl
@@ -7,7 +7,7 @@
 // CHECK-L: checking split 3/3
 // CHECK-L: checking split 4/5
 // CHECK-L: checking split 5/5
-// CHECK-L: checking split 1/1, 0.00%, (cost:4/1 last) ...
+// CHECK-L: checking split 1/1 (line 28), 0.00%, (cost:4/1 last) ...
 // CHECK-L: Boogie program verifier finished with 1 verified, 1 error
 
 function f(i:int, j:int) returns (int)
diff --git a/Test/test0/MaxSplits.bpl b/Test/test0/MaxSplits.bpl
index 46bf55b98..da35c7bc7 100644
--- a/Test/test0/MaxSplits.bpl
+++ b/Test/test0/MaxSplits.bpl
@@ -1,6 +1,6 @@
 // RUN: %parallel-boogie /trace /vcsMaxSplits:2 /vcsMaxCost:0 "%s" > %t.log
 // RUN: %OutputCheck --file-to-check "%t.log" "%s"
-// CHECK-L: checking split 1/2, 0.00%, (cost:17/2)
+// CHECK-L: checking split 1/2, 0.00%
 
 procedure SumFour(a: int, b: int, c: int, d: int) returns (e: int)
   ensures e == a + b + c + d;