diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 7431618df..3c1d1665c 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -64,7 +64,7 @@ void simple_check_sat_result::get_model_core(model_ref & m) { } proof * simple_check_sat_result::get_proof() { - return m_status == l_false ? m_proof.get() : nullptr; + return m_proof; } std::string simple_check_sat_result::reason_unknown() const {