Major Section: ACL2-BUILT-INS
The form (mbe1 exec logic) is equivalent to the forms (mbe :logic logic :exec exec) and (must-be-equal logic exec). See mbe.
(mbe1 exec logic)
(mbe :logic logic :exec exec)
(must-be-equal logic exec)
