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

fix #2869 fix #2878

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-23 10:59:26 -06:00
parent 876d7c92fb
commit 6321dabe93
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -518,6 +518,7 @@ namespace smt {
enode * r1 = n1->get_root(); enode * r1 = n1->get_root();
enode * r2 = n2->get_root(); enode * r2 = n2->get_root();
if (r1 == r2) { if (r1 == r2) {
TRACE("add_eq", tout << "redundant constraint.\n";); TRACE("add_eq", tout << "redundant constraint.\n";);
return; return;

8
src/smt/theory_bv.cpp
View file

@ -1134,6 +1134,9 @@ namespace smt {
void theory_bv::apply_sort_cnstr(enode * n, sort * s) { void theory_bv::apply_sort_cnstr(enode * n, sort * s) {
if (!is_attached_to_var(n) && !approximate_term(n->get_owner())) { if (!is_attached_to_var(n) && !approximate_term(n->get_owner())) {
mk_bits(mk_var(n)); mk_bits(mk_var(n));
if (get_context().is_relevant(n)) {
relevant_eh(n->get_owner());
}
} }
} }
@ -1773,7 +1776,6 @@ namespace smt {
st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic); st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
} }
#ifdef Z3DEBUG
bool theory_bv::check_assignment(theory_var v) { bool theory_bv::check_assignment(theory_var v) {
context & ctx = get_context(); context & ctx = get_context();
if (!is_root(v)) if (!is_root(v))
@ -1798,9 +1800,10 @@ namespace smt {
tout << "equivalence class is inconsistent, i: " << i << "\n"; tout << "equivalence class is inconsistent, i: " << i << "\n";
display_var(tout, v1); display_var(tout, v1);
display_var(tout, v2); display_var(tout, v2);
tout << "relevant: " << ctx.is_relevant(bit1) << " " << ctx.is_relevant(bit2) << "\n";
tout << "val1: " << val1 << " lvl: " << ctx.get_assign_level(bit1.var()) << " bit " << bit1 << "\n"; tout << "val1: " << val1 << " lvl: " << ctx.get_assign_level(bit1.var()) << " bit " << bit1 << "\n";
tout << "val2: " << val2 << " lvl: " << ctx.get_assign_level(bit2.var()) << " bit " << bit2 << "\n";); tout << "val2: " << val2 << " lvl: " << ctx.get_assign_level(bit2.var()) << " bit " << bit2 << "\n";);
SASSERT(val1 == val2); VERIFY(val1 == val2);
} }
SASSERT(ctx.is_relevant(get_enode(v1))); SASSERT(ctx.is_relevant(get_enode(v1)));
v1 = next(v1); v1 = next(v1);
@ -1865,6 +1868,5 @@ namespace smt {
return true; return true;
} }
#endif
}; };

3
src/smt/theory_bv.h
View file

@ -273,12 +273,9 @@ namespace smt {
bool get_fixed_value(app* x, numeral & result) const; bool get_fixed_value(app* x, numeral & result) const;
#ifdef Z3DEBUG
bool check_assignment(theory_var v); bool check_assignment(theory_var v);
bool check_invariant(); bool check_invariant();
bool check_zero_one_bits(theory_var v); bool check_zero_one_bits(theory_var v);
#endif
}; };
}; };