From d7ecaa2ebbb790cbe19bb8d57d2b0358e5ba7532 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 10 Nov 2018 09:56:19 -0800
Subject: [PATCH] add stub for certificate #1926

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

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 9a9043f2f..308b07d1a 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2366,6 +2366,10 @@ void context::updt_params() {
     }
 }
 
+void context::display_certificate(std::ostream& out) const {
+    proof_ref pr = get_proof();
+    out << pr;
+}
 
 void context::reset()
 {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 0d8b2daf6..8dd13cf63 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1092,7 +1092,7 @@ public:
     void reset();
 
     std::ostream& display(std::ostream& out) const;
-    void display_certificate(std::ostream& out) const {NOT_IMPLEMENTED_YET();}
+    void display_certificate(std::ostream& out) const;
 
     pob& get_root() const {return m_pob_queue.get_root();}
     void set_query(func_decl* q) {m_query_pred = q;}