From 2195b5e57a4033bd3117aa752be6f897353d131a Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Mon, 3 Jul 2023 16:47:59 +0200
Subject: [PATCH] Solve UNSAT queries again with proof production enabled

---
 libsmtutil/CHCSmtLib2Interface.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index c82057a1c..b3b23a7f9 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -194,7 +194,16 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
 	}();
 	auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);
 	if (result.success)
+	{
+		if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat")) {
+			solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false";
+			string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)";
+			auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery);
+			if (secondResult.success)
+				return secondResult.responseOrErrorMessage;
+		}
 		return result.responseOrErrorMessage;
+	}
 
 	m_unhandledQueries.push_back(_input);
 	return "unknown\n";