Search code examples
acl2

ACL2's GL clock ran out

What does it mean when I receive the following error message? I have GL loaded.

| ACL2 Error in ( DEFTHM SOME-THEOREM-THAT-USES-GL ...):  The clock
| ran out.~%
Solution

  • It's most likely that while you have GL loaded, you haven't yet defined a clause-processor that includes all of the necessary symbolic counterparts. This can occur even if you've already defined a GL clause processor -- you have likely included some other books since defining the GL clause processor.

    To solve it, simply define yet another GL clause processor:

    (def-gl-clause-processor yet-another-gl-clause-processor)