Fix model issues with --bitblast=eager. (#6753)

Fix model issues with --bitblast=eager. (#6753)

For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.

If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>