(n48 x) → *
Function: n48$inline
(defun n48$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 48 x) :exec (logand 281474976710655 x)))
