Add bitwise refinement mode for IAND (#5328)

Add bitwise refinement mode for IAND (#5328)

Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.

For example, with a 1-bit granularity, you might learn a lemma like:

((_ iand 4) x y), value = 1
  actual (2, 3) = 2
  bv-value = #b0001
  bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
         (and (and true
                  (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
                  (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
        ; BITWISE_REFINE

which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.