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

#6288

Browse source 
floating points may also track bit-literals.
Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track.
This commit is contained in:
Nikolaj Bjorner 2022-08-21 15:47:19 -07:00
parent 4092302590
commit a38308792e
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_bv.cpp
View file

@ -294,8 +294,7 @@ namespace smt {
m_trail_stack.push(add_var_pos_trail(b)); m_trail_stack.push(add_var_pos_trail(b));
b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs); b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
} }
else { else if (th_id == null_theory_id) {
SASSERT(th_id == null_theory_id);
ctx.set_var_theory(l.var(), get_id()); ctx.set_var_theory(l.var(), get_id());
SASSERT(ctx.get_var_theory(l.var()) == get_id()); SASSERT(ctx.get_var_theory(l.var()) == get_id());
bit_atom * b = new (get_region()) bit_atom(); bit_atom * b = new (get_region()) bit_atom();