Bug: one & is missing. It is very likely a typo.

[ustchcs-bugfinder]

z3/src/ast/rewriter/arith_rewriter.cpp

Line 697 in 7fc4653

if (is_app(e) & m_util.is_mul(e)) {

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)) {                                                 // Should be &&  ?
        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)));
            }
            args.append(to_app(e)->get_num_args() - 1, to_app(e)->get_args() + 1);
        }
        else {
            args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e)));
            args.push_back(e);
        }
    }
...

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-5.2: Bit-wise operators should not be used where logical operators should be used.)