From 441d38855ad1b1a8d7beba85ac623320bacd4e85 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@posteo.de>
Date: Fri, 11 Apr 2025 22:08:40 +0200
Subject: [PATCH] Enable SMT focus goals (unsat cores) for CVC5

---
 .../java/de/uka/ilkd/key/smt/communication/CVC5Socket.java   | 1 +
 .../uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java   | 5 +----
 .../resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props     | 1 +
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java
index 6d7c47cf2d3..fe50d3cf0d5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java
@@ -48,6 +48,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
             if (msg.contains("unsat")) {
                 sc.setFinalResult(SMTSolverResult.createValidResult(getName()));
                 sc.setState(FINISH);
+                pipe.sendMessage("(get-unsat-core)");
                 pipe.sendMessage("(exit)");
                 // pipe.close();
             } else if (msg.contains("sat")) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java
index fc459866dd8..1b3115d8c43 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java
@@ -44,10 +44,7 @@ public class ModularSMTLib2Translator implements SMTTranslator {
      * Handler option. If provided, the translator will label translations of sequent formulas such
      * that {@link de.uka.ilkd.key.smt.SMTFocusResults} can interpret the unsat core.
      * <p>
-     * This option is currently only enabled for Z3.
-     * Currently, this option only works with a CVC5 dev build.
-     * Once <a href="https://github.com/cvc5/cvc5/pull/9353">the fix</a> is included in a release,
-     * add this handler option to the .props file.
+     * This option is currently only enabled for Z3 and CVC5 (needs 1.0.4+).
      * </p>
      * Make sure to also send (get-unsat-core) in the respective socket class when adding this
      * option.
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props
index 3e057ccb853..e247c7763e4 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props
+++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props
@@ -20,3 +20,4 @@ de.uka.ilkd.key.smt.newsmt2.FloatHandler,\
 de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\
 de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\
 de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler
+handlerOptions=getUnsatCore