Skip to content

Commit 0f8b28a

Browse files
committed
Fix inst with sort depending fn
1 parent 1e7d61b commit 0f8b28a

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
@@ -925,8 +925,8 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal,
925925
}
926926

927927
String value = s.substring(eq + 1);
928-
int colon = value.indexOf(':');
929-
if (colon != -1) {
928+
int colon = value.lastIndexOf(':');
929+
if (colon != -1 && value.charAt(colon - 1) != ':') {
930930
value = value.substring(0, colon);
931931
}
932932
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)