Hi, Further investigation revealed that the version of ACL2 I was using was explicitly setting the threshold to 10^9 bytes. Once I changed that, everything started working fine and my problems have been solved. Sorry to have bothered everyone for this :) Thanks, Jared