Verify-termination-on-raw-program-okp
Permit verify-termination for functions with raw Lisp code.
By default, it is not permitted to verify termination for functions with raw Lisp
code. This restriction is important in general for preserving soundness; see
program-only. 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)
