Use constant folding for evaluating BV eager atom (#6494)

Use constant folding for evaluating BV eager atom (#6494)

This is work towards unifying top-level substitutions with model substitutions.

Currently, for model evaluation, BV eager atom preprocessing pass adds mappings (BV_EAGER_ATOM X) -> X to say how (BV_EAGER_ATOM X) should be evaluated in the model. This is not necessary since a rewrite rule (BV_EAGER_ATOM c) -> c for constant c would suffice.

This eliminates the call to addModelSubstitution in that preprocessing pass.

It also makes it so that we don't make true/false themselves into eager atoms.