mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #6153

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-12 15:49:57 -07:00
parent 43cf053066
commit ca80d99617
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_arith_core.h
View file

@ -563,7 +563,7 @@ namespace smt {
if (!m_util.is_zero(divisor)) {
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
expr_ref eqz(m), eq(m), lower(m), upper(m), qr(m);
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_int(0);
@ -571,7 +571,8 @@ namespace smt {
abs_divisor = m_util.mk_sub(m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor), one);
s(abs_divisor);
eqz = m.mk_eq(divisor, zero);
eq = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
qr = m_util.mk_add(m_util.mk_mul(divisor, div), mod);
eq = m.mk_eq(qr, dividend);
lower = m_util.mk_ge(mod, zero);
upper = m_util.mk_le(mod, abs_divisor);
TRACE("div_axiom_bug",
@ -585,6 +586,8 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(mod));
if (m_util.is_zero(dividend)) {
mk_axiom(eqz, m.mk_eq(div, zero));
mk_axiom(eqz, m.mk_eq(mod, zero));

1
src/smt/theory_lra.cpp
View file

@ -1271,6 +1271,7 @@ public:
mk_axiom(eqz, eq);
mk_axiom(eqz, mod_ge_0);
mk_axiom(eqz, mod_lt_q);
m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
if (a.is_zero(p)) {
mk_axiom(eqz, mk_literal(m.mk_eq(div, zero)));