GC$

invoke the garbage collector 
Major Section:  MISCELLANEOUS

This function is provided so that the user can call the garbage collector of the underlying Lisp from inside the ACL2 loop. Specifically, a call of gc$ is translated into a call of a function below on the same arguments. 

Allegro CL:            excl:gc
GCL                    si::gbc
CLISP                  ext:gc
CMU Common Lisp        system::gc
Macintosh Common Lisp  ccl::gc
The arguments, if any, are as documented in the underlying Common Lisp.

This function always returns nil.