mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix relevancy test

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-27 14:49:05 -08:00
parent 35900ee8ea
commit df09cb7c95
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_bv.cpp
View file

@ -1477,9 +1477,9 @@ namespace smt {
lbool val1 = ctx.get_assignment(bit1);
lbool val2 = ctx.get_assignment(bit2);
TRACE("bv", tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";);
if (!ctx.is_relevant(bit1))
if (val1 == l_undef && !ctx.is_relevant(bit1))
ctx.mark_as_relevant(bit1);
if (!ctx.is_relevant(bit2))
if (val2 == l_undef && !ctx.is_relevant(bit2))
ctx.mark_as_relevant(bit2);
if (val1 == val2)
continue;