ACL2 退出代码 137 是什么意思?输出如下所示:
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