What does ACL2 exit code 137 mean?

What does ACL2 exit code 137 mean? The output reads like this:

Form:  ( INCLUDE-BOOK "centaur/ubdds/param" ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT
Note: not introducing any A4VEC field bindings for A, since none of
its fields appear to be used.
Note: not introducing any MODSCOPE field bindings for SCOPE, since
none of its fields appear to be used.


;;; Starting full GC,  10,736,500,736 bytes allocated.
Exit code from ACL2 is 137
top.cert seems to be missing

Solution

Looks like "Linux OOM killer" killed your program.

Exit status 137 means program was terminated with singal 9 (SIGKILL) (See here):

When a command terminates on a fatal signal whose number is N, Bash uses the value 128+N as the exit status.

128+9=137

This message from the log tells us that your ACL2 proof consumed 10Gb of memory:

;;; Starting full GC, 10,736,500,736 bytes allocated.

Linux has a feature where it kills an offending process when the system is very low on memory. It is called OOM Killer: https://www.kernel.org/doc/gorman/html/understand/understand016.html

Such events are logged by kernel. You can immediately see them just to make sure:

$ dmesg |grep -i "killed process"
Mar  7 02:43:11 myhost kernel: Killed process 3841 (acl2) total-vm:128024kB, anon-rss:0kB, file-rss:0kB

There are two ACL2 calls : set-max-mem and maybe-wash-memory which you can use to control memory consumtion.

(include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag
(value-triple (set-max-mem (* 4 (expt 2 30))))           ;; 4 GB

Unfortunately these two calls do not guarantee that memory will be freed. Consider using a more powerful computer for your proof.