After off-list interaction, it turned out that the problem was due to Zenon producing a multi-megabyte proof that exceeded the fixed limit on the size of OCaml strings on a 32-bit architecture. We plan to provide a 64-bit version also for Windows with the next release.
Stephan
On Wednesday, February 1, 2017 at 4:45:05 PM UTC+1, Stephan Merz wrote:
Dear Amira,
I would suspect that the problem is due to certain operators that appear in your proof obligation. Would it be possible for you to send me the problematic spec (possibly by private email)?
Thanks,
Stephan