See #479

Within the #:guarantee of the synthesize call, I can't even do something like (log-debug "~a" (bveq ...)). The synthesize call just crashes immediately. In the I found, this seems to happen because the top-level bitwidths obviously don't match, and so perhaps the bveq is just shortcutting?