saving proofs for sequent problems (#3496)

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

@@ -209,7 +209,13 @@ public void save(OutputStream out) throws IOException {
                 }
                 final Sequent problemSeq = proof.root().sequent();
                 ps.println("\\problem {");
-                printer.printSemisequent(problemSeq.succedent());
+                if (problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) {
+                    // Problem statement is a single formula ...
+                    printer.printSemisequent(problemSeq.succedent());
+                } else {
+                    // Problem statement is a proper sequent ...
+                    printer.printSequent(problemSeq);
+                }
                 ps.println(printer.result());
                 ps.println("}\n");
             }

key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java

@@ -0,0 +1,54 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.proof.io;
+
+import java.io.File;
+import java.io.IOException;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.nparser.KeyIO;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.init.AbstractProfile;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.rule.TacletForTests;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class ProofSaverTest {
+
+    void testSaveProblemToFile(String content) throws IOException {
+        Services services = TacletForTests.services();
+        KeyIO io = new KeyIO(services);
+        KeyIO.Loader loader = io.load(content);
+        Sequent seq = loader.parseFile().loadProblem().getProblem();
+        final InitConfig initConfig =
+            new InitConfig(new Services(AbstractProfile.getDefaultProfile()));
+        Proof proof = new Proof("test", seq, "", initConfig, null);
+        File file = File.createTempFile("proofSaveTest", ".key");
+        file.deleteOnExit();
+        String status = new ProofSaver(proof, file).save();
+        assertNull(status);
+
+        KeyIO io2 = new KeyIO(services);
+        KeyIO.Loader loader2 = io2.load(content);
+        Sequent seq2 = loader2.parseFile().loadProblem().getProblem();
+
+        assertEquals(seq, seq2);
+    }
+
+    @Test
+    void saveTermProblemToFile() throws IOException {
+        String content = "\\problem { true }";
+        testSaveProblemToFile(content);
+    }
+
+    @Test
+    void saveSequentProblemToFile() throws IOException {
+        String content = "\\problem { true, false ==> false, false }";
+        testSaveProblemToFile(content);
+    }
+}