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

remove debug out

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-23 16:42:36 +07:00
parent 9a2693bb72
commit 0a28bacd0f
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -1346,7 +1346,6 @@ namespace smt {
TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v));); TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v)););
if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) { if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
literal n_eq = literal(l.var(), true); literal n_eq = literal(l.var(), true);
IF_VERBOSE(0, verbose_stream() << "eq-conflict @" << m_scope_lvl << "\n");
set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq); set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq);
} }
} }