mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 10:41:35 +00:00
Code Activity

fixup proof logging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-27 14:46:26 -08:00
parent 4cf24fb5fc
commit 6450ad82f4
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/sat/smt/bv_solver.cpp
View file

@ -410,15 +410,23 @@ namespace bv {
expr_ref eq1(m), eq2(m); expr_ref eq1(m), eq2(m);
expr* a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr; expr* a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr;
if (c.m_kind == bv_justification::kind_t::bv2int) { switch (c.m_kind) {
case bv_justification::kind_t::bv2int:
a1 = c.a->get_expr(); a1 = c.a->get_expr();
a2 = c.b->get_expr(); a2 = c.b->get_expr();
b1 = c.a->get_expr(); b1 = c.a->get_expr();
b2 = c.c->get_expr(); b2 = c.c->get_expr();
} break;
else if (c.m_kind != bv_justification::kind_t::bit2ne) { case bv_justification::kind_t::ne2bit:
case bv_justification::kind_t::eq2bit:
case bv_justification::kind_t::bit2eq:
a1 = var2expr(c.m_v1); a1 = var2expr(c.m_v1);
a2 = var2expr(c.m_v2); a2 = var2expr(c.m_v2);
break;
case bv_justification::kind_t::bit2ne:
case bv_justification::kind_t::bvext:
default:
break;
} }
if (a1) { if (a1) {