From cfe96fe92e1e6cbf265feb02580afb5f1c9d8154 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 31 Mar 2020 10:13:37 -0400
Subject: [PATCH] [spacer] fixedpoint.get_answer() returns ground refutation
 for SAT

---
 src/muz/spacer/spacer_context.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 5a38f723c..62075ebcb 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1016,7 +1016,10 @@ class context {
     /**
        \brief Retrieve satisfying assignment with explanation.
     */
-    expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
+    expr_ref mk_sat_answer() const {
+        proof_ref pr = get_ground_refutation();
+        return expr_ref(pr.get(), pr.get_manager());
+    }
     expr_ref mk_unsat_answer() const;
     unsigned get_cex_depth ();