Update expect files

boogie-org · Jan 22, 2025 · e529af5 · e529af5
1 parent ccd5110
commit e529af5
Show file tree

Hide file tree

Showing 7 changed files with 31 additions and 31 deletions.
diff --git a/Test/implementationDivision/focus/focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect
@@ -1,4 +1,4 @@
-implementation Ex() returns (y: int)
+implementation Ex-0() returns (y: int)
 {
 
   anon0:
@@ -13,7 +13,7 @@ implementation Ex() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
+implementation Ex-1/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,-20,+25]() returns (y: int)
+implementation Ex-2/focus[+16,-20,+25]() returns (y: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation Ex/focus[+16,-20,+25]() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,+20,-25]() returns (y: int)
+implementation Ex-3/focus[+16,+20,-25]() returns (y: int)
 {
 
   anon0:
@@ -76,7 +76,7 @@ implementation Ex/focus[+16,+20,-25]() returns (y: int)
 }
 
 
-implementation Ex/focus[+16,+20,+25]() returns (y: int)
+implementation Ex-4/focus[+16,+20,+25]() returns (y: int)
 {
 
   anon0:
@@ -102,7 +102,7 @@ implementation Ex/focus[+16,+20,+25]() returns (y: int)
 
 
 focus.bpl(15,5): Error: this assertion could not be proved
-implementation focusInconsistency/focus[+38](x: int) returns (y: int)
+implementation focusInconsistency--1/focus[+38](x: int) returns (y: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect
@@ -81,7 +81,7 @@ implementation IsolateAssertion(x: int, y: int)
 
 isolateAssertion.bpl(20,3): Error: this assertion could not be proved
 isolateAssertion.bpl(21,3): Error: this assertion could not be proved
-implementation IsolatePathsAssertion/assert@50/path[29,45](x: int, y: int)
+implementation IsolatePathsAssertion-0/assert@50/path[29,45](x: int, y: int)
 {
 
   anon0:
@@ -112,7 +112,7 @@ implementation IsolatePathsAssertion/assert@50/path[29,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[29,47](x: int, y: int)
+implementation IsolatePathsAssertion-1/assert@50/path[29,47](x: int, y: int)
 {
 
   anon0:
@@ -143,7 +143,7 @@ implementation IsolatePathsAssertion/assert@50/path[29,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,32,45](x: int, y: int)
+implementation IsolatePathsAssertion-2/assert@50/path[31,32,45](x: int, y: int)
 {
 
   anon0:
@@ -175,7 +175,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,32,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,32,47](x: int, y: int)
+implementation IsolatePathsAssertion-3/assert@50/path[31,32,47](x: int, y: int)
 {
 
   anon0:
@@ -207,7 +207,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,32,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,35,45](x: int, y: int)
+implementation IsolatePathsAssertion-4/assert@50/path[31,35,45](x: int, y: int)
 {
 
   anon0:
@@ -239,7 +239,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,35,45](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion/assert@50/path[31,35,47](x: int, y: int)
+implementation IsolatePathsAssertion-5/assert@50/path[31,35,47](x: int, y: int)
 {
 
   anon0:
@@ -271,7 +271,7 @@ implementation IsolatePathsAssertion/assert@50/path[31,35,47](x: int, y: int)
 }
 
 
-implementation IsolatePathsAssertion(x: int, y: int)
+implementation IsolatePathsAssertion-6(x: int, y: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect
@@ -1,4 +1,4 @@
-implementation IsolateContinue/remainingAssertions(x: int) returns (r: int)
+implementation IsolateContinue-0/remainingAssertions(x: int) returns (r: int)
 {
 
   anon0:
@@ -26,7 +26,7 @@ implementation IsolateContinue/remainingAssertions(x: int) returns (r: int)
 }
 
 
-implementation IsolateContinue/goto@17(x: int) returns (r: int)
+implementation IsolateContinue-1/goto@17(x: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
@@ -98,7 +98,7 @@ implementation IsolateReturnPaths/remainingAssertions(x: int, y: int) returns (r
 }
 
 
-implementation IsolateReturnPaths/return@44/path[27](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-0/return@44/path[27](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -125,7 +125,7 @@ implementation IsolateReturnPaths/return@44/path[27](x: int, y: int) returns (r:
 }
 
 
-implementation IsolateReturnPaths/return@44/path[29,30](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-1/return@44/path[29,30](x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -153,7 +153,7 @@ implementation IsolateReturnPaths/return@44/path[29,30](x: int, y: int) returns
 }
 
 
-implementation IsolateReturnPaths/return@44/path[29,33](x: int, y: int) returns (r: int)
+implementation IsolateReturnPaths-2/return@44/path[29,33](x: int, y: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect
@@ -1,4 +1,4 @@
-implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MergeAtEnd--1/assert@5(x: int) returns (r: int)
 {
 
   anon0:
@@ -22,7 +22,7 @@ implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns
 
 isolateJumpAndSplitOnEveryAssert.bpl(9,3): Error: a postcondition could not be proved on this return path
 isolateJumpAndSplitOnEveryAssert.bpl(5,3): Related location: this is the postcondition that could not be proved
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-0/return@25/assert@16(x: int) returns (r: int)
 {
 
   anon0:
@@ -33,7 +33,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-1/return@25/assert@17(x: int) returns (r: int)
 {
 
   anon0:
@@ -45,7 +45,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-2/return@21/assert@16(x: int) returns (r: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(
 }
 
 
-implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@17(x: int) returns (r: int)
+implementation {:vcs_split_on_every_assert} MultipleEnsures-3/return@21/assert@17(x: int) returns (r: int)
 {
 
   anon0:

diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo/untilFirstSplit()
+implementation Foo-0/untilFirstSplit()
 {
 
   anon3_Then:
@@ -8,7 +8,7 @@ implementation Foo/untilFirstSplit()
 }
 
 
-implementation Foo/afterSplit@11()
+implementation Foo-1/afterSplit@11()
 {
 
   anon3_Else:
@@ -20,7 +20,7 @@ implementation Foo/afterSplit@11()
 }
 
 
-implementation Foo/afterSplit@12()
+implementation Foo-2/afterSplit@12()
 {
 
   anon3_Else:

diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect
@@ -1,4 +1,4 @@
-implementation Foo/untilFirstSplit() returns (y: int)
+implementation Foo-0/untilFirstSplit() returns (y: int)
 {
 
   anon0:
@@ -13,7 +13,7 @@ implementation Foo/untilFirstSplit() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@15() returns (y: int)
+implementation Foo-1/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Foo/afterSplit@15() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@22() returns (y: int)
+implementation Foo-2/afterSplit@22() returns (y: int)
 {
 
   anon0:
@@ -51,7 +51,7 @@ implementation Foo/afterSplit@22() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@25() returns (y: int)
+implementation Foo-3/afterSplit@25() returns (y: int)
 {
 
   anon0:
@@ -86,7 +86,7 @@ implementation Foo/afterSplit@25() returns (y: int)
 }
 
 
-implementation Foo/afterSplit@19() returns (y: int)
+implementation Foo-4/afterSplit@19() returns (y: int)
 {
 
   anon0: