mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
8ae42b5ae1
commit
377dbad3b9
|
@ -665,11 +665,12 @@ proof * asserted_formulas::get_inconsistency_proof() const {
|
|||
return nullptr;
|
||||
if (!m.proofs_enabled())
|
||||
return nullptr;
|
||||
if (!m.inc())
|
||||
return nullptr;
|
||||
for (justified_expr const& j : m_formulas) {
|
||||
if (m.is_false(j.get_fml()))
|
||||
return j.get_proof();
|
||||
}
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue