Method operator+

smt/expr.cpp:719–729

                    z3app)

expr expr::operator+(const expr &rhs) const {
  expr a, b;
  // (concat x const) + rhs -> (concat const+rhs) if no overflow happens
  if (rhs.isConst() && isConcat(a, b) && b.isConst()) {
    auto rhs2 = rhs.trunc(b.bits());
    if (rhs2.zextOrTrunc(rhs.bits()).eq(rhs) &&
        b.add_no_uoverflow(rhs2).isTrue())
      return a.concat(b + rhs2);
  }
  return binopc(Z3_mk_bvadd, operator+, Z3_OP_BADD, isZero, alwaysFalse);
}

expr expr::operator-(const expr &rhs) const {
  C();