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.
See :DOC set-absstobj-debug.
At this point, the only way to get ACL2 to evaluate further input is to
submit the form :CONTINUE-FROM-ILLEGAL-STATE, as noted above — or
more generally, the form it actually represents,
(CONTINUE-FROM-ILLEGAL-STATE), which may need to be written as
(ACL2::CONTINUE-FROM-ILLEGAL-STATE) if the current-package is
other than "ACL2". There is actually one exception: :q is
accepted, to pop out of the current call of ld.
To get a bit more information from the error message displayed above, see
See community-book file
Examples 3 and 4, for relevant examples.
Technical note. An illegal-state is entered when ACL2 sets the ld
special, ld-pre-eval-print, to the value :illegal-state.