I was doing some performance comparisons and found what looks like a bug in Poly/ML when compiled with ?enable-compact32bit. The problem is that ML code that runs to completion when compiled to use native 64 bit addresses, raises Overflow when compiled to 32 bit addressing. The code is a lengthy proof search that explores in excess of 4,000,000,000 blind alleys. It takes about 10 to 20 minutes to find the proof when using 64 bit addressing and it takes 2 or 3 minutes before it raises Overflow when using 32 bit addressing.
I don?t really know where to start with narrowing the problem down. I?ve attached a tarball containing cutdown source that demonstrates the problem, but the mailing list software will likely strip it off, hence CC to David.
Regards,
Rob.