mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

Gracefully handle absence of a proof

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-26 21:18:10 -04:00
parent d9100437ce
commit 176c0a97f7
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/solver/solver_pool.cpp
View file

@ -101,9 +101,11 @@ public:
proof * get_proof() override { proof * get_proof() override {
scoped_watch _t_(m_pool.m_proof_watch); scoped_watch _t_(m_pool.m_proof_watch);
if (!m_proof.get()) { if (!m_proof.get()) {
elim_aux_assertions pc(m_pred);
m_proof = m_base->get_proof(); m_proof = m_base->get_proof();
pc(m, m_proof, m_proof); if (m_proof) {
elim_aux_assertions pc(m_pred);
pc(m, m_proof, m_proof);
}
} }
return m_proof; return m_proof;
} }