From 129c27e2338e8179a237e1aa71eb2b53fb161a8a Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 25 Jul 2026 10:00:39 +0200 Subject: [PATCH] Relax restrictions for two taclets --- .../resources/de/uka/ilkd/key/proof/rules/booleanRules.key | 2 ++ .../test/resources/de/uka/ilkd/key/nparser/taclets.old.txt | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/booleanRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/booleanRules.key index d2c5a6005da..26db07f1644 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/booleanRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/booleanRules.key @@ -97,6 +97,7 @@ \schemaVar \term [rigid] boolean br; \assumes( ==> br = TRUE) \find(br) + \ignoreUpdateLevel // safe as only rigid terms are matched \replacewith(FALSE) \heuristics(apply_equations) \displayname "apply_eq_boolean" @@ -106,6 +107,7 @@ \schemaVar \term [rigid] boolean br; \assumes( ==> br = FALSE) \find(br) + \ignoreUpdateLevel // safe as only rigid terms are matched \replacewith(TRUE) \heuristics(apply_equations) \displayname "apply_eq_boolean" diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 0d24751f3d0..cc8e69dd6ee 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Wed Jul 22 17:10:12 CEST 2026 +# Date: Sat Jul 25 10:22:38 CEST 2026 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -1006,7 +1006,7 @@ Choices: true} apply_eq_boolean_rigid { \assumes ([]==>[equals(br,TRUE)]) \find(br) -\sameUpdateLevel\replacewith(FALSE) +\replacewith(FALSE) \heuristics(apply_equations) Choices: true} ----------------------------------------------------- @@ -1014,7 +1014,7 @@ Choices: true} apply_eq_boolean_rigid_2 { \assumes ([]==>[equals(br,FALSE)]) \find(br) -\sameUpdateLevel\replacewith(TRUE) +\replacewith(TRUE) \heuristics(apply_equations) Choices: true} -----------------------------------------------------