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

fix #5771

Browse source 
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
This commit is contained in:
Nikolaj Bjorner 2022-01-14 15:46:40 -08:00
parent d5cc162fa7
commit d09abdf58e
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/pb_solver.cpp
View file

@ -1458,7 +1458,6 @@ namespace pb {
for (auto const [w, l] : wlits) for (auto const [w, l] : wlits)
weight += w; weight += w;
if (weight < k) { if (weight < k) {
std::cout << "weight " << weight << " " << k << "\n";
if (lit == sat::null_literal) if (lit == sat::null_literal)
s().add_clause(0, nullptr, sat::status::th(false, get_id())); s().add_clause(0, nullptr, sat::status::th(false, get_id()));
else else

5
src/smt/theory_recfun.cpp
View file

@ -55,7 +55,7 @@ namespace smt {
ctx.internalize(arg, false); ctx.internalize(arg, false);
} }
if (!ctx.e_internalized(atom)) { if (!ctx.e_internalized(atom)) {
ctx.mk_enode(atom, false, true, false); ctx.mk_enode(atom, false, true, true);
} }
if (!ctx.b_internalized(atom)) { if (!ctx.b_internalized(atom)) {
bool_var v = ctx.mk_bool_var(atom); bool_var v = ctx.mk_bool_var(atom);
@ -214,7 +214,7 @@ namespace smt {
void theory_recfun::assign_eh(bool_var v, bool is_true) { void theory_recfun::assign_eh(bool_var v, bool is_true) {
expr* e = ctx.bool_var2expr(v); expr* e = ctx.bool_var2expr(v);
if (is_true && u().is_case_pred(e)) { if (is_true && u().is_case_pred(e)) {
TRACEFN("assign_case_pred_true " << mk_pp(e, m)); TRACEFN("assign_case_pred_true " << v << " " << mk_pp(e, m));
// body-expand // body-expand
push_body_expand(e); push_body_expand(e);
} }
@ -343,6 +343,7 @@ namespace smt {
activate_guard(pred_applied, guards); activate_guard(pred_applied, guards);
} }
TRACEFN("assert core " << preds);
// the disjunction of branches is asserted // the disjunction of branches is asserted
// to close the available cases. // to close the available cases.