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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-30 19:15:03 -08:00
parent 4daba290b1
commit 3b4f976118
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_user_propagator.cpp
View file

@ -53,7 +53,7 @@ void theory_user_propagator::propagate_cb(
unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs,
expr* conseq) { expr* conseq) {
CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true, CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true,
tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"); ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"));
if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true)
return; return;
m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));