diff --git a/src/params/solver_params.pyg b/src/params/solver_params.pyg
index 9ff13864d..1c2be3213 100644
--- a/src/params/solver_params.pyg
+++ b/src/params/solver_params.pyg
@@ -8,6 +8,7 @@ def_module_params('solver',
                           ('lemmas2console', BOOL, False, 'print lemmas during search'),
                           ('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'),
                           ('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'),
+                          ('proof.log', SYMBOL, '', 'log clause proof trail into a file'),
                           ('proof.check', BOOL, True, 'check proof logs'),
                           ('proof.save', BOOL, False, 'save proof log into a proof object that can be extracted using (get-proof)'),
                           ('proof.trim', BOOL, False, 'trim and save proof into a proof object that an be extracted using (get-proof)'),			  
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 4ca223be6..eb2d0071d 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -197,7 +197,6 @@ namespace sat {
         m_drat_check_unsat  = p.drat_check_unsat();
         m_drat_check_sat  = p.drat_check_sat();
         m_drat_file       = p.drat_file();
-        m_smt_proof       = p.smt_proof();
         m_smt_proof_check = p.smt_proof_check();
         m_smt_proof_check_rup = p.smt_proof_check_rup();
         m_drat_disable = p.drat_disable();
@@ -206,7 +205,7 @@ namespace sat {
             (sp.lemmas2console() ||
              m_drat_check_unsat ||
              m_drat_file.is_non_empty_string() ||
-             m_smt_proof.is_non_empty_string() ||
+             sp.proof_log().is_non_empty_string() ||
              m_smt_proof_check ||
              m_drat_check_sat);
         m_drat_binary     = p.drat_binary();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index ae19c63ea..8adfc13ed 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -178,7 +178,6 @@ namespace sat {
         bool               m_drat_disable;
         bool               m_drat_binary;
         symbol             m_drat_file;
-        symbol             m_smt_proof;
         bool               m_smt_proof_check;
         bool               m_smt_proof_check_rup;
         bool               m_drat_check_unsat;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 7466a1126..20a415441 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -47,7 +47,6 @@ def_module_params('sat',
                           ('threads', UINT, 1, 'number of parallel threads to use'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
                           ('drat.disable', BOOL, False, 'override anything that enables DRAT'),
-                          ('smt.proof', SYMBOL, '', 'add SMT proof log to file'),
                           ('smt.proof.check', BOOL, False, 'check SMT proof while it is created'),
                           ('smt.proof.check_rup', BOOL, True, 'apply forward RUP proof checking'),
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),