<div dir="ltr"><div>Unfortunately, I have not been able to produce a small test case, but there is a large-ish one (12MB compressed) available here:<br><a href="https://hol-theorem-prover.org/overflow.tar.gz">https://hol-theorem-prover.org/overflow.tar.gz</a>.<br></div><br>It contains three files, hol4-words.thy, hol4-words-unint.art, and <a href="http://hol4.int">hol4.int</a>.<br><br>To produce the error, edit the paths in hol4-words.thy to point to the other two files, then try this:<br>opentheory info --theory hol4-words.thy<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 21 April 2016 at 02:28, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It means that an integer overflow is occurring somewhere in the<br>
processing, which shouldn't happen. If you give me a test case where<br>
this occurs (the smaller the better) I can look into it.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div class="h5"><br>
On Tue, Apr 19, 2016 at 6:12 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> Hello,<br>
><br>
> I keep running into this problem:<br>
><br>
> FATAL ERROR: opentheory exception:<br>
> Overflow<br>
><br>
> What does it mean?<br>
><br>
> Thanks,<br>
> Ramana<br>
><br>
</div></div>> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>