Z3 - a hundred bit equalities is MUCH faster than a length-100 bitvector equality?

Question

I have a pretty simple QF_BV SMT query for Z3:

(set-logic QF_BV)

(declare-const orig_hand (_ BitVec 136))
(assert (= orig_hand #x0001121000000011100000011100000000))

(declare-const wildcard (_ BitVec 136))
(assert (or
  (= wildcard #x1000000000000000000000000000000000)
  (= wildcard #x0100000000000000000000000000000000)
  (= wildcard #x0010000000000000000000000000000000)
  (= wildcard #x0001000000000000000000000000000000)
  (= wildcard #x0000100000000000000000000000000000)
  (= wildcard #x0000010000000000000000000000000000)
  (= wildcard #x0000001000000000000000000000000000)
  (= wildcard #x0000000100000000000000000000000000)
  (= wildcard #x0000000010000000000000000000000000)
  (= wildcard #x0000000001000000000000000000000000)
  (= wildcard #x0000000000100000000000000000000000)
  (= wildcard #x0000000000010000000000000000000000)
  (= wildcard #x0000000000001000000000000000000000)
  (= wildcard #x0000000000000100000000000000000000)
  (= wildcard #x0000000000000010000000000000000000)
  (= wildcard #x0000000000000001000000000000000000)
  (= wildcard #x0000000000000000100000000000000000)
  (= wildcard #x0000000000000000010000000000000000)
  (= wildcard #x0000000000000000001000000000000000)
  (= wildcard #x0000000000000000000100000000000000)
  (= wildcard #x0000000000000000000010000000000000)
  (= wildcard #x0000000000000000000001000000000000)
  (= wildcard #x0000000000000000000000100000000000)
  (= wildcard #x0000000000000000000000010000000000)
  (= wildcard #x0000000000000000000000001000000000)
  (= wildcard #x0000000000000000000000000100000000)
  (= wildcard #x0000000000000000000000000010000000)
  (= wildcard #x0000000000000000000000000001000000)
  (= wildcard #x0000000000000000000000000000100000)
  (= wildcard #x0000000000000000000000000000010000)
  (= wildcard #x0000000000000000000000000000001000)
  (= wildcard #x0000000000000000000000000000000100)
  (= wildcard #x0000000000000000000000000000000010)
  (= wildcard #x0000000000000000000000000000000001)))

(declare-const hand (_ BitVec 136))
(assert (= hand (bvadd orig_hand wildcard)))

(declare-const digits (_ BitVec 136))

; add all the hex digits of `digits` together and make sure it's equal to 4 mod 16
(declare-const digits_2 (_ BitVec 136))
(assert (= digits_2 (bvand #x00000000000000000FFFFFFFFFFFFFFFFF (bvadd digits (bvlshr digits (_ bv68 136))))))
(declare-const digits_4 (_ BitVec 136))
(assert (= digits_4 (bvand #x0000000000000000000000000FFFFFFFFF (bvadd digits_2 (bvlshr digits_2 (_ bv36 136))))))
(declare-const digits_8 (_ BitVec 136))
(assert (= digits_8 (bvand #x00000000000000000000000000000FFFFF (bvadd digits_4 (bvlshr digits_4 (_ bv20 136))))))
(declare-const digits_16 (_ BitVec 136))
(assert (= digits_16 (bvand #x0000000000000000000000000000000FFF (bvadd digits_8 (bvlshr digits_8 (_ bv12 136))))))
(declare-const digits_32 (_ BitVec 136))
(assert (= digits_32 (bvand #x00000000000000000000000000000000FF (bvadd digits_16 (bvlshr digits_16 (_ bv8 136))))))
(declare-const digits_sum (_ BitVec 136))
(assert (= digits_sum (bvand #x000000000000000000000000000000000F (bvadd digits_32 (bvlshr digits_32 (_ bv4 136))))))
(assert (= (_ bv4 4) ((_ extract 3 0) digits_sum)))

(declare-const required (_ BitVec 136))
(assert (= required (bvadd digits (bvlshr digits (_ bv4 136)) (bvlshr digits (_ bv8 136)))))

Essentially I have a hand that can contain a wildcard I'm solving for, subject to the constraint that there exists some bitvector digits from which I derive a bitvector required that is equal to hand. I don't think the details are that important because of what's coming next. There are two ways to do the equality, compare the bitvectors:

(assert (= hand required))
(check-sat)

or compare each bit:

(assert (= ((_ extract 0 0) hand) ((_ extract 0 0) required)))
(assert (= ((_ extract 1 1) hand) ((_ extract 1 1) required)))
(assert (= ((_ extract 2 2) hand) ((_ extract 2 2) required)))
(assert (= ((_ extract 3 3) hand) ((_ extract 3 3) required)))
...
(assert (= ((_ extract 134 134) hand) ((_ extract 134 134) required)))
(assert (= ((_ extract 135 135) hand) ((_ extract 135 135) required)))
(check-sat)

The first obvious method runs in about 0.55s on my machine. The second clunky method, however, consistently runs in 0.08s, which is much faster.

Shouldn't the two methods express the exact same constraint? Why the huge discrepancy in runtime? Should I never use = with long bitvectors?