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

#5777

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-16 14:01:49 -08:00
parent ea93345b75
commit a48d3fdbb1
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_solver.cpp
View file

@ -158,7 +158,7 @@ namespace bv {
SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
m_stats.m_num_diseq_static++;
expr_ref eq = mk_var_eq(v1, v2);
expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
add_unit(~ctx.internalize(eq, false, false, m_is_redundant));
}
@ -740,6 +740,7 @@ namespace bv {
void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_expr_id() << " v" << v2 << " #" << var2enode(v2)->get_expr_id() << "\n";);
if (!merge_zero_one_bits(r1, r2)) {
TRACE("bv", tout << "conflict detected\n";);
return; // conflict was detected