mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 17:50:23 +00:00
Code Activity

#5546

Browse source 
try dampening
This commit is contained in:
Nikolaj Bjorner 2021-09-14 10:32:53 +02:00
parent f13ccf8969
commit 9aad331699
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/user_propagator.cpp
View file

@ -52,6 +52,8 @@ void user_propagator::propagate_cb(
unsigned num_fixed, unsigned const* fixed_ids, unsigned num_fixed, unsigned const* fixed_ids,
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) {
if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true)
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)));
} }