From 4d0835b9ddb4ff1b2dabaa4df293700fddc8db14 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 15:20:07 +0100 Subject: [PATCH] Fix slicing test (changed loop rules add two more rules, resulting in more slices) --- .../firstTouch/05-ReverseArray/reverseArray.proof | 2 ++ .../java/org/key_project/slicing/EndToEndTests.java | 10 +++++----- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof b/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof index b772b95f7a1..a07ede2b6c4 100644 --- a/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof +++ b/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof @@ -359,6 +359,7 @@ (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")) @@ -366,6 +367,7 @@ (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 index da4981d9aea..d930d1821e3 100644 --- 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 iteration1 = sliceProofFullFilename( new File(testCaseDirectory, "../../../../../key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof"), - 6535, 4234, true, true, true); + 6537, 4236, true, true, true); Pair iteration2 = - sliceProofFullFilename(iteration1.second, 4234, 4227, true, true, true); + sliceProofFullFilename(iteration1.second, 4236, 4229, true, true, true); Pair iteration3 = - sliceProofFullFilename(iteration2.second, 4227, 4218, true, true, true); + sliceProofFullFilename(iteration2.second, 4229, 4220, true, true, true); Pair iteration4 = - sliceProofFullFilename(iteration3.second, 4218, 4207, true, true, true); + sliceProofFullFilename(iteration3.second, 4220, 4209, true, true, true); Pair 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();