This patch adds support for model generation in the bitvector theory.

To generate a value for a model, a simple brute-force backtracking
search amongst all possible bitvector values is performed to find one
that is different from the values that were asserted distinct. If none
can be found (or if exactly one is found, in which case the value is
forced) the `case_split` flag is set so that we report `unsat` instead
of looping during model generation.

In the future, this should be augmented with proper support for case
splits / bit-blasting in the relational theory. Note that even if we add
support for case splits in the relational theory, having an enumeration
in model generation is useful, because we may not always want to perform
case splits on large bitvector types.

Co-authored-by: Pierrot <[email protected]>