Update expect files

boogie-org · Jan 23, 2025 · c70a308 · c70a308
1 parent e529af5
commit c70a308
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateAssertion/assert@20(x: int, y: int)
+implementation IsolateAssertion-0/assert@20(x: int, y: int)
 {
 
   anon0:
@@ -38,7 +38,7 @@ implementation IsolateAssertion/assert@20(x: int, y: int)
 }
 
 
-implementation IsolateAssertion(x: int, y: int)
+implementation IsolateAssertion-1(x: int, y: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateReturn/remainingAssertions(x: int, y: int) returns (r: int)
+implementation IsolateReturn-0/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -25,7 +25,7 @@ implementation IsolateReturn/remainingAssertions(x: int, y: int) returns (r: int
 }
 
 
-implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
+implementation IsolateReturn-1/return@16(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -54,7 +54,7 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
 
 isolateJump.bpl(16,21): Error: a postcondition could not be proved on this return path
 isolateJump.bpl(5,3): Related location: this is the postcondition that could not be proved
-implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-0/remainingAssertions(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -98,7 +98,7 @@ implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r
 }
 
 
-implementation IsolateReturnPaths-0/return@44/path[27](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-1/return@44/path[27](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -125,7 +125,7 @@ implementation IsolateReturnPaths-0/return@44/path[27](x: int, y: int) returns (
 }
 
 
-implementation IsolateReturnPaths-1/return@44/path[29,30](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-2/return@44/path[29,30](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -153,7 +153,7 @@ implementation IsolateReturnPaths-1/return@44/path[29,30](x: int, y: int) return
 }
 
 
-implementation IsolateReturnPaths-2/return@44/path[29,33](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-3/return@44/path[29,33](x: int, y: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl
@@ -1,5 +1,5 @@
 // RUN: %parallel-boogie /prune:1 /errorTrace:0 /printSplit:"%t" /printSplitDeclarations "%s" > "%t"
-// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.spl"
+// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit--1.spl"
 
 // The following checks are a bit simplistic, but this is
 // on purpose to reduce brittleness. We assume there would now be two uses clauses