mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dc110f10a4
commit
7b4f1ed530
|
@ -2637,6 +2637,10 @@ namespace pb {
|
|||
* add ~root(~l) to c, k <- k + 1
|
||||
*/
|
||||
void solver::unit_strengthen() {
|
||||
return;
|
||||
|
||||
// TODO - this is unsound exposed by 4_21_21_-1.txt
|
||||
|
||||
sat::big big(s().m_rand);
|
||||
big.init(s(), true);
|
||||
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i)
|
||||
|
@ -2646,7 +2650,8 @@ namespace pb {
|
|||
}
|
||||
|
||||
void solver::unit_strengthen(sat::big& big, constraint& p) {
|
||||
if (p.lit() != sat::null_literal) return;
|
||||
if (p.lit() != sat::null_literal)
|
||||
return;
|
||||
unsigned sz = p.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal u = p.get_lit(i);
|
||||
|
@ -2694,8 +2699,8 @@ namespace pb {
|
|||
}
|
||||
}
|
||||
++m_stats.m_num_big_strengthenings;
|
||||
constraint* c = add_pb_ge(sat::null_literal, wlits, b, p.learned());
|
||||
p.set_removed();
|
||||
add_pb_ge(sat::null_literal, wlits, b, p.learned());
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -211,6 +211,7 @@ namespace smt {
|
|||
new_ctx->m_is_auxiliary = true;
|
||||
new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
|
||||
copy_plugins(*this, *new_ctx);
|
||||
new_ctx->copy_user_propagator(*this);
|
||||
return new_ctx;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue