Update expect file

boogie-org · Oct 18, 2024 · f27d1eb · f27d1eb
1 parent 160b0f7
commit f27d1eb
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 35 deletions.
diff --git 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
@@ -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
@@ -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.*