Permit verify-termination for functions with raw Lisp code.
By default, it is not permitted to
However, in some cases it may be harmless to remove this restriction. That can be done as follows. Note that an active trust tag is required: in principle you can render ACL2 unsound with this action!
(defttag t) (remove-untouchable verify-termination-on-raw-program-okp nil) ; In the following, t can be replaced by an expression that evaluates to a ; list of symbols for which it is permitted to verify termination. (assign verify-termination-on-raw-program-okp t)