From 3e8fbbd55879de5d258edd5e999dbc3fec8cdb6e Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 20 Jan 2025 19:37:42 +0100 Subject: [PATCH] changing one rule for final fields it was not wrong before but not confluent. Failed the case vstte10_05_Queue/AmortizedQueue_AmortizedQueue.key --- .../main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key index 10a0838873..c856eee307 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key @@ -1355,7 +1355,7 @@ EQ, java.lang.Object::) = TRUE) - \replacewith( ==> boolean::select(h, o, java.lang.Object::) = TRUE ) + \add( ==> boolean::select(h, o, java.lang.Object::) = TRUE ) \heuristics(concrete) };