Without the flag, functions applied to ground arguments are treated the
same way as every other one: by unrolling their body. This is
suboptimal, as we can instead pass to Z3 the equality f(a0, a1) = v,
instead of letting it "discover" it by itself.

Note that this hasn't been shown to bring any major performance
improvement; ground applications hardly show up in verification, for
instance. But think about it, you'll agree using evaluation there is
"The right thing to do.™".

Note that testing --evalground currently highlights some bugs.