Set a global time limit for CCG-based termination proofs.

Examples: (set-ccg-time-limit 120) ; limits termination proofs to 120 seconds. (set-ccg-time-limit 53/2) ; limits termination proofs to 53/2 seconds. (set-ccg-time-limit nil) ; removes any time limit for termination proofs.

Introduced by the CCG analysis book, this macro sets a global time limit for the completion of the CCG analysis. The time limit is given as a rational number, signifying the number of seconds to which the CCG analysis should be limited, or nil, signifying that there should be no such time limit. If CCG has not completed its attempt to prove termination in the number of seconds specified, it will immediately throw an error and the definition attempt will fail. Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form: (set-ccg-time-limit tl)

where

To see what the current time limit is, see `get-ccg-time-limit`.