Fix #3156

key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationParserException.java

@@ -1,5 +1,7 @@
 package de.uka.ilkd.key.proof;
 
+import java.util.Optional;
+
 import de.uka.ilkd.key.java.Position;
 
 public class SVInstantiationParserException extends SVInstantiationExceptionWithPosition {
@@ -18,27 +20,31 @@ public SVInstantiationParserException(String instantiation, Position position, S
         this.detail = (detail == null) ? "" : detail;
     }
 
-    private String space(int i) {
-        StringBuilder res = new StringBuilder();
-        for (int j = 0; j < i; j++) {
-            res.append(" ");
+    private Optional<String> getInstantiationRow() {
+        if (getPosition().column() <= 0) {
+            return Optional.empty();
+        }
+        String[] rows = instantiation.split("\n");
+        var line = getPosition().line() - 1;
+        if (!(line < rows.length)) {
+            return Optional.empty();
         }
-        return res.toString();
+        return Optional.of(rows[line]);
     }
 
     public String getMessage() {
         int column = getPosition().column();
 
         String msg = super.getMessage();
         // needs non-prop font: msg +="\n"+inst;
-        if (column > 0) {
+        Optional<String> row = getInstantiationRow();
+        if (row.isPresent()) {
             // needs non-prop font: msg +="\n"+space(column-1)+"^";
-            String[] rows = instantiation.split("\n");
-            StringBuilder sb = new StringBuilder(rows[getPosition().line() - 1]);
+            var sb = new StringBuilder(row.get());
             sb.insert(column - 1, " ~~> ");
             msg += "\noccurred at: " + sb;
         } else {
-            msg += "\noccurred in:" + instantiation;
+            msg += "\noccurred in: " + instantiation;
         }
 
         msg += "\nDetail:\n" + detail;

key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java

@@ -439,7 +439,8 @@ public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services
 
         if (newMC == null) {
             throw new IllegalInstantiationException(
-                "Instantiation " + term + " of " + sv + "does not satisfy the variable conditions");
+                "Instantiation " + term + " of " + sv
+                    + " does not satisfy the variable conditions");
         }
 
         SVInstantiations svInst = newMC.getInstantiations();