mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #6464

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-23 17:21:51 +07:00
parent 0a28bacd0f
commit 0a671f2f44
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_bv.cpp
View file

@ -1318,7 +1318,7 @@ namespace smt {
SASSERT(consequent.var() != antecedent.var()); SASSERT(consequent.var() != antecedent.var());
TRACE("bv_bit_prop", tout << "assigning: " << consequent << " @ " << ctx.get_scope_level(); TRACE("bv_bit_prop", tout << "assigning: " << consequent << " @ " << ctx.get_scope_level();
tout << " using "; ctx.display_literal(tout, antecedent); tout << " using "; ctx.display_literal(tout, antecedent);
tout << " #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << " idx: " << idx << "\n"; tout << " " << enode_pp(get_enode(v1), ctx) << " " << enode_pp(get_enode(v2), ctx) << " idx: " << idx << "\n";
tout << "propagate_eqc: " << propagate_eqc << "\n";); tout << "propagate_eqc: " << propagate_eqc << "\n";);
if (consequent == false_literal) { if (consequent == false_literal) {
m_stats.m_num_conflicts++; m_stats.m_num_conflicts++;
@ -1358,6 +1358,9 @@ namespace smt {
// So, we need to propagate the assignment to other bits. // So, we need to propagate the assignment to other bits.
bool_var bv = consequent.var(); bool_var bv = consequent.var();
atom * a = get_bv2a(bv); atom * a = get_bv2a(bv);
CTRACE("bv", !a, tout << ctx.literal2expr(literal(bv, false)) << "\n");
if (!a)
return;
SASSERT(a->is_bit()); SASSERT(a->is_bit());
bit_atom * b = static_cast<bit_atom*>(a); bit_atom * b = static_cast<bit_atom*>(a);
var_pos_occ * curr = b->m_occs; var_pos_occ * curr = b->m_occs;