From ca80d996176f26fc171b2a131d7dcf6bd112a38d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jul 2022 15:49:57 -0700 Subject: [PATCH] fix #6153 --- src/smt/theory_arith_core.h | 7 +++++-- src/smt/theory_lra.cpp | 1 + 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 1b2a7cc49fe..012ad695baa 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -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)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 794a61e76d9..75f9cb99710 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1271,6 +1271,7 @@ class theory_lra::imp { 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)));