Illegal ACL2 state
See set-absstobj-debug for background on invariance violations for abstract stobjs. In short, they may occur when execution does not complete for certain atomic operations.
Such violations cause the following error message to be printed.
ACL2 Error in CHK-ABSSTOBJ-INVARIANTS: Possible invariance violation for an abstract stobj! **PROCEED AT YOUR OWN RISK.** To proceed, evaluate the following form. :CONTINUE-FROM-ILLEGAL-STATE See :DOC set-absstobj-debug.
At this point, the only way to get ACL2 to evaluate further input is to
submit the form
To get a bit more information from the error message displayed above, see set-absstobj-debug.
See community-book file
Technical note. An illegal-state is entered when ACL2 sets the