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

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-17 00:45:52 -05:00
parent d016cb1da5
commit 2174bccdba
1 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/bv_internalize.cpp
View file

@ -661,12 +661,10 @@ namespace bv {
if (lit0 == sat::null_literal) { if (lit0 == sat::null_literal) {
m_bits[v_arg][idx] = lit; m_bits[v_arg][idx] = lit;
TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
if (arg_sz > 1) { atom* a = new (get_region()) atom(lit.var());
atom* a = new (get_region()) atom(lit.var()); a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); insert_bv2a(lit.var(), a);
insert_bv2a(lit.var(), a); ctx.push(mk_atom_trail(lit.var(), *this));
ctx.push(mk_atom_trail(lit.var(), *this));
}
} }
else if (lit != lit0) { else if (lit != lit0) {
add_clause(lit0, ~lit); add_clause(lit0, ~lit);