		Search-engine friendly clone of the ACL2 documentation.

Verify-termination

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. (Technical note: With sufficient effort this restriction could perhaps be lifted, but that would involve significant modification to the ACL2 sources, in particular to handle properly code generation for executable-counterparts (see evaluation) in such cases in source function oneify-cltl-code.)

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)