From 375c0ff9a9bc594bad2e14ec0c1141203600489a Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 12 Aug 2019 11:03:50 -0400
Subject: [PATCH] Implement get_proof() in bmc and spacer engines

---
 src/muz/bmc/dl_bmc_engine.cpp     | 6 +++++-
 src/muz/bmc/dl_bmc_engine.h       | 3 ++-
 src/muz/spacer/spacer_context.cpp | 5 -----
 src/muz/spacer/spacer_context.h   | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index b03a9aab1..28de7950b 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1537,10 +1537,14 @@ namespace datalog {
         // m_solver->reset_statistics();
     }
 
-    expr_ref bmc::get_answer() {
+    expr_ref bmc::get_answer()  {
         return m_answer;
     }
 
+    proof_ref bmc::get_proof() {
+        return proof_ref(to_app(m_answer), m);
+    }
+
     void bmc::get_rules_along_trace(datalog::rule_ref_vector& rules) {
         rules.append(m_rule_trace);
     }
diff --git a/src/muz/bmc/dl_bmc_engine.h b/src/muz/bmc/dl_bmc_engine.h
index 9a7424287..9eee65ad9 100644
--- a/src/muz/bmc/dl_bmc_engine.h
+++ b/src/muz/bmc/dl_bmc_engine.h
@@ -63,7 +63,8 @@ namespace datalog {
         void reset_statistics() override;
         void get_rules_along_trace(datalog::rule_ref_vector& rules) override;
 
-        expr_ref get_answer() override;
+        expr_ref get_answer()  override;
+        proof_ref get_proof() override; 
 
         // direct access to (new) non-linear compiler.
         void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level);
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 05e8eeb70..492182dbe 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2909,11 +2909,6 @@ model_ref context::get_model()
     return model;
 }
 
-proof_ref context::get_proof() const
-{
-    return proof_ref (m);
-}
-
 expr_ref context::get_answer()
 {
     switch(m_last_result) {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 76813895c..f73af2fe3 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1109,7 +1109,7 @@ public:
     expr_ref get_reachable (func_decl* p);
     void add_invariant (func_decl *pred, expr* property);
     model_ref get_model();
-    proof_ref get_proof() const;
+    proof_ref get_proof() const {return get_ground_refutation();}
 
     expr_ref get_constraints (unsigned lvl);
     void add_constraint (expr *c, unsigned lvl);