
	/**
	 * Returns the expression-to-bitvector conversion specified by the given operator.
	 * @ensures expr.apply(op)
	 */
	public static final IntExpression cast(ExprCastOperator op, Expression expr) {
		try {
			return expr.apply(op);
		} catch (RuntimeException ex) {
			throw new ActionException(ex.getMessage(), ex); // wrap
		}
	}