From f27d1ebd940c438990b9aa59e5507138d460ed7e Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 18 Oct 2024 16:49:02 +0200
Subject: [PATCH] Update expect file

---
 Test/commandline/SplitOnEveryAssert.bpl       |  2 +-
 .../isolateJump/isolateJump.bpl.expect        | 66 +++++++++----------
 Test/test0/SplitOnEveryAssert.bpl             |  2 +-
 3 files changed, 35 insertions(+), 35 deletions(-)

diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl
index 50425d6e9..2e3878802 100644
--- a/Test/commandline/SplitOnEveryAssert.bpl
+++ b/Test/commandline/SplitOnEveryAssert.bpl
@@ -6,8 +6,8 @@
 // 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:      --> split #4 done,  \[.* s\] Invalid
 // CHECK:      checking split 5/11 .*
 // CHECK:      checking split 6/11 .*
 // CHECK:      checking split 7/11 .*
diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
index 3c47dc663..9c32be2a1 100644
--- a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
+++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect
@@ -1,3 +1,33 @@
+implementation IsolateReturn(x: int, y: int) returns (r: int)
+{
+
+  anon0:
+    goto anon6_Then, anon6_Else;
+
+  anon6_Then:
+    assume {:partition} x > 0;
+    assume r#AT#0 == 0 + 1;
+    assume r#AT#2 == r#AT#0;
+    goto anon7_Else;
+
+  anon6_Else:
+    assume {:partition} 0 >= x;
+    assume r#AT#1 == 0 + 2;
+    assume r#AT#2 == r#AT#1;
+    goto anon7_Else;
+
+  anon7_Else:
+    assume {:partition} 0 >= y;
+    assume r#AT#4 == r#AT#2 + 4;
+    assume r#AT#5 == r#AT#4;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assert r#AT#5 > 4;
+    return;
+}
+
+
 implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
 {
 
@@ -28,7 +58,9 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int)
 }
 
 
-implementation IsolateReturn(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(x: int, y: int) returns (r: int)
 {
 
   anon0:
@@ -58,8 +90,6 @@ implementation IsolateReturn(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/assert@34[27](x: int, y: int) returns (r: int)
 {
 
@@ -90,36 +120,6 @@ implementation IsolateReturnPaths/assert@34[29](x: int, y: int) returns (r: int)
 }
 
 
-implementation IsolateReturnPaths(x: int, y: int) returns (r: int)
-{
-
-  anon0:
-    goto anon6_Then, anon6_Else;
-
-  anon6_Then:
-    assume {:partition} x > 0;
-    assume r#AT#0 == 0 + 1;
-    assume r#AT#2 == r#AT#0;
-    goto anon7_Else;
-
-  anon6_Else:
-    assume {:partition} 0 >= x;
-    assume r#AT#1 == 0 + 2;
-    assume r#AT#2 == r#AT#1;
-    goto anon7_Else;
-
-  anon7_Else:
-    assume {:partition} 0 >= y;
-    assume r#AT#4 == r#AT#2 + 4;
-    assume r#AT#5 == r#AT#4;
-    goto GeneratedUnifiedExit;
-
-  GeneratedUnifiedExit:
-    assert r#AT#5 > 4;
-    return;
-}
-
-
 isolateJump.bpl(34,29): Error: a postcondition could not be proved on this return path
 isolateJump.bpl(23,3): Related location: this is the postcondition that could not be proved
 
diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl
index e459892fd..c883fb50c 100644
--- a/Test/test0/SplitOnEveryAssert.bpl
+++ b/Test/test0/SplitOnEveryAssert.bpl
@@ -6,8 +6,8 @@
 // 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:      --> split #4 done,  \[.* s\] Invalid
 // CHECK:      checking split 5/11.*
 // CHECK:      checking split 6/11.*
 // CHECK:      checking split 7/11.*