Fix program element printing in proof saver

key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java

@@ -87,6 +87,19 @@ public void print(SourceElement e) {
         l.end();
     }
 
+    /**
+     * Alternative entry method for this class. Omits the trailing semicolon in the output.
+     *
+     * @param s source element to print
+     */
+    public void printFragment(SourceElement s) {
+        l.beginRelativeC(0);
+        markStart(s);
+        s.visit(this);
+        markEnd(s);
+        l.end();
+    }
+
     /**
      * Marks the start of the first executable statement ...
      *

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

@@ -739,7 +739,7 @@ public static String escapeCharacters(String toEscape) {
 
     public static String printProgramElement(ProgramElement pe) {
         PrettyPrinter printer = PrettyPrinter.purePrinter();
-        printer.print(pe);
+        printer.printFragment(pe);
         return printer.result();
     }
 

key.core/src/test/java/de/uka/ilkd/key/pp/PrettyPrinterTest.java

@@ -0,0 +1,20 @@
+package de.uka.ilkd.key.pp;
+
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.logic.ProgramElementName;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.Test;
+
+class PrettyPrinterTest {
+    @Test
+    void printLocationVariable() {
+        // Test that the pretty printer does not add a ';' when using printFragment.
+        // This is important for saving instantiations (see #3071)
+        PrettyPrinter pp = PrettyPrinter.purePrinter();
+        ProgramElementName name = new ProgramElementName("x");
+        LocationVariable variable = new LocationVariable(name, KeYJavaType.VOID_TYPE);
+        pp.printFragment(variable);
+        Assertions.assertEquals("x", pp.result());
+    }
+}