(abort!) = nil. But imagine that it is
defined in such a way that it causes a stack overflow or other
resource exhaustion when called.
Major Section: MISCELLANEOUS
When (abort!) is evaluated inside of ACL2's command loop, the
current computation is aborted and control returns to the top of
the command loop, exactly as though the user had interrupted
and aborted the current computation.
Logically speaking, (abort!) = nil. But imagine that it is
defined in such a way that it causes a stack overflow or other
resource exhaustion when called.