• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • How-to-contribute
        • Common-lisp
          • Defun-mode-caveat
          • Generalized-booleans
          • Raw-lisp-error
            • Live-stobj-in-proof
          • Escape-to-common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Mailing-lists
    • Interfacing-tools
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Raw-lisp-error

Live-stobj-in-proof

Error messages about “live” stobjs during proofs

It is possible to see an error like the following. (This error is probably very rare, and perhaps can only occur during a proof.)

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  A live stobj (for stobj ST) was unexpectedly encountered
        when evaluating a call of the function, ST-INIT.
        See :DOC live-stobj-in-proof.
***********************************************

The solution is generally to disable the executable-counterpart of the offending function, as suggested by the example below (essentially provided by Sol Swords). As of this writing (in July, 2025), the only way to get an unexpected “live” stobj is by the use of swap-stobjs, as illustrated below.

First introduce a pair of congruent stobjs.

(defstobj st (fld))
(defstobj st1 (fld1) :congruent-to st)

Now define a function that “initializes” the stobj st by creating a new stobj st1 and swapping the two (see swap-stobjs).

(defun st-init (st)
  (declare (xargs :stobjs (st)))
  (with-local-stobj st1
    (mv-let (st1 st)
      (swap-stobjs st1 st)
      st)))

The following proof attempt causes the error message displayed above.

(thm (not (equal (st-init '(1)) '(nil))))

In fact, that formula is not a theorem! Through Version 8.6, ACL2 mistakenly proved this theorem by evaluating the indicated call of st-init to obtain an actual Lisp array, because of how ACL2 handles stobjs in Lisp. But now ACL2 produces the error displayed above.

The error is avoided if we disable the executable-counterpart of the offending function mentioned in the error message, st-init. Indeed, the following theorem, which contradicts the false claim above and disables the offending executable-counterpart, shows that the logical value of (st-init '(1)) is indeed '(nil).

(thm (equal (st-init '(1)) '(nil))
     :hints(("Goal" :in-theory (disable (:e st-init)))))