mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

fix unsound merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 17:47:20 -08:00
parent aed48e9f9b
commit 3f369ae962
3 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_bv_plugin.cpp
View file

@ -171,7 +171,7 @@ namespace euf {
if (is_extract(p, lo, hi)) { if (is_extract(p, lo, hi)) {
auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1); auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
push_merge(p, mk_value(val_p, width(p))); push_merge(bv.mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p)));
} }
} }

2
src/sat/smt/polysat/viable.cpp
View file

@ -804,7 +804,7 @@ namespace polysat {
return find_t::multiple; return find_t::multiple;
} }
else { else {
IF_VERBOSE(0, display_one(verbose_stream() << "full: ", v, ne) << "\n"); // IF_VERBOSE(0, display_one(verbose_stream() << "full: ", v, ne) << "\n");
SASSERT(hi < lo); SASSERT(hi < lo);
ne->interval = eval_interval::full(); ne->interval = eval_interval::full();
ne->coeff = 1; ne->coeff = 1;

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

@ -515,7 +515,6 @@ namespace polysat {
pdd b = expr2pdd(y); pdd b = expr2pdd(y);
auto& m = a.manager(); auto& m = a.manager();
unsigned sz = m.power_of_2(); unsigned sz = m.power_of_2();
verbose_stream() << "quot-rem " << a << " " << b << "\n";
if (b.is_zero()) { if (b.is_zero()) {
// By SMT-LIB specification, b = 0 ==> q = -1, r = a. // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
internalize_set(quot, m.mk_val(m.max_value())); internalize_set(quot, m.mk_val(m.max_value()));