[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

A question



Dear PVS users:
  Sometimes the PVS prover will prompt the following message when I invoke
some PVS decision procedures such as (grind). Did anyone know what the
message means? And how would it affect the correctness of the proof?
Many thanks.

-------------------------------------------------------------------------------
5142208 bytes have been tenured, next gc will be global.
See the documentation for variable EXCL:*GLOBAL-GC-BEHAVIOR* for more information.
-------------------------------------------------------------------------------

-- Jei-Wen Teng