Rob, I'm glad that's sorted. --enable-compact32bit uses 32-bit quantities for both addresses and ints. It's necessary to use the same size for both in order to be able to compile polymorphic functions. LargeWord.word is 64-bits (i.e. two "words") to allow it to handle native values in SysWord.word.
Regards, David
On 04/04/2019 11:38, Rob Arthan wrote:
David,
Apologies! This was all down to a simple misunderstanding on my part. I hadn't appreciated that --enable-compact32bit gives you 31-bit ints. My proof search explores in excess of 2^32 blind alleys and it tries to count them.
The confusion about Mac OS versions and lldb was caused by me doing the tests with the compiler built with --enable-intinf-as-int as well as --enable-compact32bit.
Regards,
Rob.