From fc4c162e31a0898c87cb603a60adf1f0d40c81bb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 May 2019 15:59:28 -0700
Subject: [PATCH] add clause proof module, small improvements to bapa

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/solver2tactic.cpp | 9 ++++-----
 src/solver/tactic2solver.cpp | 2 ++
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 3c4f291a5..2bd5f59c7 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -110,7 +110,11 @@ public:
         extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
         ref<solver> local_solver = m_solver->translate(m, m_params);
         local_solver->assert_expr(clauses);
+        TRACE("solver2tactic", tout << "clauses asserted\n";);
         lbool r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr()); 
+        TRACE("solver2tactic", tout << "check sat result " << r << "\n";);
+        proof* pr = local_solver->get_proof();
+        if (pr) in->set(proof2proof_converter(m, pr));
         switch (r) {
         case l_true: 
             if (in->models_enabled()) {
@@ -128,11 +132,6 @@ public:
         case l_false: {
             in->reset();
             expr_dependency_ref lcore(m);
-            proof* pr = nullptr;
-            if (in->proofs_enabled()) {
-                pr = local_solver->get_proof();
-                in->set(proof2proof_converter(m, pr));
-            }
             if (in->unsat_core_enabled()) {
                 expr_ref_vector core(m);
                 local_solver->get_unsat_core(core);
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index c62e920e7..06cdac71a 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -196,12 +196,14 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
     }
     catch (z3_error & ex) {
         TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
+        m_result->m_proof = pr;
         throw ex;
     }
     catch (z3_exception & ex) {
         TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
         m_result->set_status(l_undef);
         m_result->m_unknown = ex.msg();
+        m_result->m_proof = pr;
     }
     m_tactic->collect_statistics(m_result->m_stats);
     m_tactic->collect_statistics(m_stats);