Method sext

smt/expr.cpp:1827–1840

}

expr expr::sext(unsigned amount) const {
  C();
  if (amount == 0)
    return *this;

  expr e;
  if (isSignExt(e))
    return e.sext((bits() - e.bits()) + amount);

  if (isNegative().isFalse())
    return zext(amount);

  return simplify_const(Z3_mk_sign_ext(ctx(), amount, ast()), *this);
}

expr expr::zext(unsigned amount) const {
  if (amount == 0)