Fix slicing test (changed loop rules add two more rules, resulting in…

… more slices)
KeYProject · Oct 31, 2024 · 4d0835b · 4d0835b
1 parent 8fc8c29
commit 4d0835b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof b/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof
@@ -359,13 +359,15 @@
        (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_1") (userinteraction))
         (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_2") (userinteraction))
         (rule "variableDeclaration" (formula "9") (term "1") (newnames "x_1") (userinteraction))
+        (rule "variableDeclaration" (formula "9") (term "1") (newnames "i_before") (userinteraction))
         (rule "emptyModality" (formula "9") (term "1") (userinteraction))
          (rule "false_to_not_true" (formula "9") (term "0,1,0,1,1,1,1"))
          (rule "concrete_and_3" (formula "9") (term "0,1,1,1"))
          (rule "expandInInt" (formula "9") (term "1,0,0,1,0,0,0,0,1,1,1"))
          (rule "concrete_and_3" (formula "9") (term "0,0,1,0,0,0,0,1,1,1"))
          (rule "expandInInt" (formula "9") (term "1,0,0,0,0,0,0,0,1,1,1"))
          (rule "concrete_and_3" (formula "9") (term "0,0,0,0,0,0,0,1,1,1"))
+         (rule "simplifyUpdate2" (formula "9") (term "1,0,1,1,0,1,1,1,1") (userinteraction))
          (rule "elementOfAllFields" (formula "9") (term "0,0,0,0,1,0,1,1,0,1,1,1,1"))
          (rule "expandInInt" (formula "9") (term "1,0,0,1,0,0,0,0,0,1,1,0,1,1,1,1"))
          (rule "concrete_and_3" (formula "9") (term "0,0,1,0,0,0,0,0,1,1,0,1,1,1,1"))

diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java b/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java
@@ -78,15 +78,15 @@ void sliceMultipleIterations() throws Exception {
         Pair<Proof, File> iteration1 = sliceProofFullFilename(
             new File(testCaseDirectory,
                 "../../../../../key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof"),
-            6535, 4234, true, true, true);
+            6537, 4236, true, true, true);
         Pair<Proof, File> iteration2 =
-            sliceProofFullFilename(iteration1.second, 4234, 4227, true, true, true);
+            sliceProofFullFilename(iteration1.second, 4236, 4229, true, true, true);
         Pair<Proof, File> iteration3 =
-            sliceProofFullFilename(iteration2.second, 4227, 4218, true, true, true);
+            sliceProofFullFilename(iteration2.second, 4229, 4220, true, true, true);
         Pair<Proof, File> iteration4 =
-            sliceProofFullFilename(iteration3.second, 4218, 4207, true, true, true);
+            sliceProofFullFilename(iteration3.second, 4220, 4209, true, true, true);
         Pair<Proof, File> iteration5 =
-            sliceProofFullFilename(iteration4.second, 4207, 4195, true, true, true);
+            sliceProofFullFilename(iteration4.second, 4209, 4197, true, true, true);
         iteration5.first.dispose();
         iteration4.first.dispose();
         iteration3.first.dispose();