Skip to content

Commit 5f9de0a

Browse files
Drodtwadoon
authored andcommitted
Fix inst with sort depending fn
1 parent 7c0fb9d commit 5f9de0a

2 files changed

Lines changed: 3 additions & 3 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -924,8 +924,8 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal,
924924
}
925925

926926
String value = s.substring(eq + 1);
927-
int colon = value.indexOf(':');
928-
if (colon != -1) {
927+
int colon = value.lastIndexOf(':');
928+
if (colon != -1 && value.charAt(colon - 1) != ':') {
929929
value = value.substring(0, colon);
930930
}
931931
app = parseSV2(app, sv, value, currGoal);

key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ public class ProveRulesTest {
5656
public void loadTacletProof(String tacletName, Taclet taclet, @Nullable Path proofFile)
5757
throws Exception {
5858
assertNotNull(proofFile,
59-
"Taclet " + tacletName + " was annoted with \\lemma but no taclet proof was found.");
59+
"Taclet " + tacletName + " was annotated with \\lemma but no taclet proof was found.");
6060
assertNotNull(taclet, "Proof file " + proofFile
6161
+ " claims that it contains a proof for taclet " + tacletName
6262
+ " but corresponding taclet seems to be unavailable (maybe it is not annotated with \\lemma?).");

0 commit comments

Comments
 (0)