Fixes

boogie-org · Jul 31, 2024 · 75f26a3 · 75f26a3
1 parent ce88ee2
commit 75f26a3
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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;