I am new to PVS (and new to LISP, too).
Type-error in KERNEL : OBJECT-NOT-FOUND-ERROR-HANDLER
134218304 is not of type (UNSIGNED-BYTE 27)
After the error message, the checking process continues for a while until the prover generates a long warning message and takes an abnormal stop.
Briefly speaking, the warning message says pvs-undo-info is discarded since it exceeds the limit.
My best guess is that some of the recursive functions generate a mismatched-type value as a parameter to themselves.
I interpreted the message as ¡°one of the recursive calls generate 134218304 which is out-of-range for unsigned-byte¡±, out of pure guesswork.
I have been trying to locate the source of the error for a while without a success since my recursive functions do not increase parameter values.
Therefore, I would like to confirm with experts that I am digging into the right direction.
Can somebody interpret the exact meaning of this error message for me?
Can this type-error cause an abnormal stop even though the prover continues after the error occurs?
Many thanks in advance,