From 5374142e3e1b0edee4d5ace5cdf2ba1d3ab82738 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Nov 2022 07:59:32 +0700
Subject: [PATCH] continue updates for adding proof-log to smt core

---
 src/smt/params/smt_params.cpp | 2 ++
 src/smt/params/smt_params.h   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 4e9afaa8d5b..8143bc31b21 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -64,6 +64,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_axioms2files = sp.axioms2files();
     m_lemmas2console = sp.lemmas2console();
     m_instantiations2console = sp.instantiations2console();
+    m_proof_log = sp.proof_log();
 }
 
 void smt_params::updt_params(params_ref const & p) {
@@ -126,6 +127,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_ematching);
     DISPLAY_PARAM(m_induction);
     DISPLAY_PARAM(m_clause_proof);
+    DISPLAY_PARAM(m_proof_log);
 
     DISPLAY_PARAM(m_case_split_strategy);
     DISPLAY_PARAM(m_rel_case_split_order);
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 62e1ec8437a..73f556eb889 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -112,6 +112,7 @@ struct smt_params : public preprocessor_params,
     bool             m_ematching = true;
     bool             m_induction = false;
     bool             m_clause_proof = false;
+    symbol           m_proof_log;
 
     // -----------------------------------
     //