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

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-03 12:33:04 -07:00
parent 87f5b9282f
commit a566c7307d
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -244,8 +244,9 @@ namespace bv {
expr_ref b2b(bv.mk_bit2bool(e, i), m); expr_ref b2b(bv.mk_bit2bool(e, i), m);
m_bits[v].push_back(sat::null_literal); m_bits[v].push_back(sat::null_literal);
sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant); sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant);
(void)lit;
TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
if (m_bits[v].back() == sat::null_literal)
m_bits[v].back() = lit;
SASSERT(m_bits[v].back() == lit); SASSERT(m_bits[v].back() == lit);
} }
} }