...

It seems like using --enable-optimize-space gives a faster build *and* faster execution. So maybe I will probably make this the default if I observe the same thing on other benchmarks.

Just as a side note, when I was fiddling with Visual C++ compiler options on Windows, I noticed the exact same behavior where optimizing for speed versus optimizing for space gave only a marginal speed advantage and at a large compilation time premium. Guillaume