(Also, my figure of halving in performance was bogus; I was looking at user time, not wallclock time. 7 seconds versus 43 seconds is more like what I'm seeing.)
(Also, my figure of halving in performance was bogus; I was looking at user time, not wallclock time. 7 seconds versus 43 seconds is more like what I'm seeing.)