I am using PVS in writing specifications. But I have observed that, when we try to prove lemmas of complicated specifications using 'grind', PVS hangs giving message
Error:16777216 is invalid size for make-string
[condition type: SIMPLE-ERROR]
Restart actions(Select using :continue):
0: Return to Top Level ( an "abort" restart)
1: Abort # <PROCESS Initial Lisp Listener>
 PVS (24)
What can be reason behind this type of error?
Is there any way now, to continue with my proof process?