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

for Arie

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-10 18:07:54 -07:00
parent 994dab8eb6
commit 9cd339841a
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/arith_rewriter.cpp
View file

@ -729,7 +729,9 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
expr_ref arith_rewriter::neg_monomial(expr* e) const {
expr_ref_vector args(m());
rational a1;
if (is_app(e) && m_util.is_mul(e)) {
if (m_util.is_numeral(e, a1))
args.push_back(m_util.mk_numeral(-a1, e->get_sort()));
else if (is_app(e) && m_util.is_mul(e)) {
if (is_numeral(to_app(e)->get_arg(0), a1)) {
if (!a1.is_minus_one()) {
args.push_back(m_util.mk_numeral(-a1, m_util.is_int(e)));