From 5ecc59b6bc5611060b77bd76f6c632574482e956 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Aug 2020 10:13:13 -0700 Subject: [PATCH] fix #4627 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index c096c1a30..1a8648156 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -694,7 +694,7 @@ br_status arith_rewriter::mk_eq_core(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 (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)));