Name of the function (defined in a separate file) to call the ACL2 rewriter.
Definition: *solve-call-acl2-rewriter*
(defconst *solve-call-acl2-rewriter* 'solve-call-acl2-rewriter)