;; This triggers on positive integers of 64 bits length
;; with the most significant 33 bits being 1. We use the
;; same encoding as in the previous clause.
;; This triggers on positive integers of 64 bits length
;; with the most significant 33 bits being 1. We use the
;; same encoding as in the previous clause.