mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #4930

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-08 12:15:02 -08:00
parent e902e1ef13
commit 3d39f37e63
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_conflict_resolution.cpp
View file

@ -839,8 +839,7 @@ namespace smt {
unsigned num_args; unsigned num_args;
switch (js.get_kind()) { switch (js.get_kind()) {
case eq_justification::AXIOM: case eq_justification::AXIOM:
UNREACHABLE(); return m.mk_hypothesis(m.mk_eq(n1->get_expr(), n2->get_expr()));
return nullptr;
case eq_justification::EQUATION: case eq_justification::EQUATION:
TRACE("proof_gen_bug", tout << js.get_literal() << "\n"; m_ctx.display_literal_info(tout, js.get_literal());); TRACE("proof_gen_bug", tout << js.get_literal() << "\n"; m_ctx.display_literal_info(tout, js.get_literal()););
return norm_eq_proof(n1, n2, get_proof(js.get_literal())); return norm_eq_proof(n1, n2, get_proof(js.get_literal()));
@ -1138,7 +1137,6 @@ namespace smt {
eq_justification js = lhs->m_trans.m_justification; eq_justification js = lhs->m_trans.m_justification;
switch (js.get_kind()) { switch (js.get_kind()) {
case eq_justification::AXIOM: case eq_justification::AXIOM:
UNREACHABLE();
break; break;
case eq_justification::EQUATION: case eq_justification::EQUATION:
if (get_proof(js.get_literal()) == nullptr) if (get_proof(js.get_literal()) == nullptr)