SMT2 bitreverse eq0 rewrite hang

(set-option :produce-models true)
(set-logic QF_BV )
(declare-fun dummy1127 () (_ BitVec 1) )
(declare-fun reservedconst_32 () (_ BitVec 64) )
(assert
 (let ( (?B1 dummy1127 ) (?B2 reservedconst_32 ) )
  (let ( (?B3 (ite  (bvugt ?B1 (_ bv0 1) ) (_ bv18446744073709551615 64) ?B2 ) ) )
   (let ( (?B4 ((_ extract 53  53)  ?B3 ) ) (?B5 ((_ extract 54  54)  ?B3 ) ) (?B6 ((_ extract 55  55)  ?B3 ) ) (?B7 ((_ extract 56  56)  ?B3 ) ) (?B8 ((_ extract 57  57)  ?B3 ) ) (?B9 ((_ extract 58  58)  ?B3 ) ) (?B10 ((_ extract 59  59)  ?B3 ) ) (?B11 ((_ extract 60  60)  ?B3 ) ) (?B12 ((_ extract 61  61)  ?B3 ) ) (?B13 ((_ extract 62  62)  ?B3 ) ) (?B14 ((_ extract 63  63)  ?B3 ) ) (?B15 ((_ extract 14  14)  ?B3 ) ) (?B16 ((_ extract 15  15)  ?B3 ) ) (?B17 ((_ extract 16  16)  ?B3 ) ) (?B18 ((_ extract 17  17)  ?B3 ) ) (?B19 ((_ extract 18  18)  ?B3 ) ) (?B20 ((_ extract 19  19)  ?B3 ) ) (?B21 ((_ extract 20  20)  ?B3 ) ) (?B22 ((_ extract 21  21)  ?B3 ) ) (?B23 ((_ extract 22  22)  ?B3 ) ) (?B24 ((_ extract 23  23)  ?B3 ) ) (?B25 ((_ extract 24  24)  ?B3 ) ) (?B26 ((_ extract 25  25)  ?B3 ) ) (?B27 ((_ extract 26  26)  ?B3 ) ) (?B28 ((_ extract 0  0)  ?B3 ) ) (?B29 ((_ extract 1  1)  ?B3 ) ) (?B30 ((_ extract 2  2)  ?B3 ) ) (?B31 ((_ extract 3  3)  ?B3 ) ) (?B32 ((_ extract 4  4)  ?B3 ) ) (?B33 ((_ extract 5  5)  ?B3 ) ) (?B34 ((_ extract 6  6)  ?B3 ) ) (?B35 ((_ extract 7  7)  ?B3 ) ) (?B36 ((_ extract 8  8)  ?B3 ) ) (?B37 ((_ extract 9  9)  ?B3 ) ) (?B38 ((_ extract 10  10)  ?B3 ) ) (?B39 ((_ extract 11  11)  ?B3 ) ) (?B40 ((_ extract 12  12)  ?B3 ) ) (?B41 ((_ extract 13  13)  ?B3 ) ) (?B42 ((_ extract 40  40)  ?B3 ) ) (?B43 ((_ extract 41  41)  ?B3 ) ) (?B44 ((_ extract 42  42)  ?B3 ) ) (?B45 ((_ extract 43  43)  ?B3 ) ) (?B46 ((_ extract 44  44)  ?B3 ) ) (?B47 ((_ extract 45  45)  ?B3 ) ) (?B48 ((_ extract 46  46)  ?B3 ) ) (?B49 ((_ extract 47  47)  ?B3 ) ) (?B50 ((_ extract 48  48)  ?B3 ) ) (?B51 ((_ extract 49  49)  ?B3 ) ) (?B52 ((_ extract 50  50)  ?B3 ) ) (?B53 ((_ extract 51  51)  ?B3 ) ) (?B54 ((_ extract 52  52)  ?B3 ) ) (?B55 ((_ extract 27  27)  ?B3 ) ) (?B56 ((_ extract 28  28)  ?B3 ) ) (?B57 ((_ extract 29  29)  ?B3 ) ) (?B58 ((_ extract 30  30)  ?B3 ) ) (?B59 ((_ extract 31  31)  ?B3 ) ) (?B60 ((_ extract 32  32)  ?B3 ) ) (?B61 ((_ extract 33  33)  ?B3 ) ) (?B62 ((_ extract 34  34)  ?B3 ) ) (?B63 ((_ extract 35  35)  ?B3 ) ) (?B64 ((_ extract 36  36)  ?B3 ) ) (?B65 ((_ extract 37  37)  ?B3 ) ) (?B66 ((_ extract 38  38)  ?B3 ) ) (?B67 ((_ extract 39  39)  ?B3 ) ) )
    (let ( (?B68 (concat  ?B28 ?B29 ) ) )
    (let ( (?B69 (concat  ?B68 ?B30 ) ) )
    (let ( (?B70 (concat  ?B69 ?B31 ) ) )
    (let ( (?B71 (concat  ?B70 ?B32 ) ) )
    (let ( (?B72 (concat  ?B71 ?B33 ) ) )
    (let ( (?B73 (concat  ?B72 ?B34 ) ) )
    (let ( (?B74 (concat  ?B73 ?B35 ) ) )
    (let ( (?B75 (concat  ?B74 ?B36 ) ) )
    (let ( (?B76 (concat  ?B75 ?B37 ) ) )
    (let ( (?B77 (concat  ?B76 ?B38 ) ) )
    (let ( (?B78 (concat  ?B77 ?B39 ) ) )
    (let ( (?B79 (concat  ?B78 ?B40 ) ) )
    (let ( (?B80 (concat  ?B79 ?B41 ) ) )
    (let ( (?B81 (concat  ?B80 ?B15 ) ) )
    (let ( (?B82 (concat  ?B81 ?B16 ) ) )
    (let ( (?B83 (concat  ?B82 ?B17 ) ) )
    (let ( (?B84 (concat  ?B83 ?B18 ) ) )
    (let ( (?B85 (concat  ?B84 ?B19 ) ) )
    (let ( (?B86 (concat  ?B85 ?B20 ) ) )
    (let ( (?B87 (concat  ?B86 ?B21 ) ) )
    (let ( (?B88 (concat  ?B87 ?B22 ) ) )
    (let ( (?B89 (concat  ?B88 ?B23 ) ) )
    (let ( (?B90 (concat  ?B89 ?B24 ) ) )
    (let ( (?B91 (concat  ?B90 ?B25 ) ) )
    (let ( (?B92 (concat  ?B91 ?B26 ) ) )
    (let ( (?B93 (concat  ?B92 ?B27 ) ) )
    (let ( (?B94 (concat  ?B93 ?B55 ) ) )
    (let ( (?B95 (concat  ?B94 ?B56 ) ) )
    (let ( (?B96 (concat  ?B95 ?B57 ) ) )
    (let ( (?B97 (concat  ?B96 ?B58 ) ) )
    (let ( (?B98 (concat  ?B97 ?B59 ) ) )
    (let ( (?B99 (concat  ?B98 ?B60 ) ) )
    (let ( (?B100 (concat  ?B99 ?B61 ) ) )
    (let ( (?B101 (concat  ?B100 ?B62 ) ) )
    (let ( (?B102 (concat  ?B101 ?B63 ) ) )
    (let ( (?B103 (concat  ?B102 ?B64 ) ) )
    (let ( (?B104 (concat  ?B103 ?B65 ) ) )
    (let ( (?B105 (concat  ?B104 ?B66 ) ) )
    (let ( (?B106 (concat  ?B105 ?B67 ) ) )
    (let ( (?B107 (concat  ?B106 ?B42 ) ) )
    (let ( (?B108 (concat  ?B107 ?B43 ) ) )
    (let ( (?B109 (concat  ?B108 ?B44 ) ) )
    (let ( (?B110 (concat  ?B109 ?B45 ) ) )
    (let ( (?B111 (concat  ?B110 ?B46 ) ) )
    (let ( (?B112 (concat  ?B111 ?B47 ) ) )
    (let ( (?B113 (concat  ?B112 ?B48 ) ) )
    (let ( (?B114 (concat  ?B113 ?B49 ) ) )
    (let ( (?B115 (concat  ?B114 ?B50 ) ) )
    (let ( (?B116 (concat  ?B115 ?B51 ) ) )
    (let ( (?B117 (concat  ?B116 ?B52 ) ) )
    (let ( (?B118 (concat  ?B117 ?B53 ) ) )
    (let ( (?B119 (concat  ?B118 ?B54 ) ) )
    (let ( (?B120 (concat  ?B119 ?B4 ) ) )
    (let ( (?B121 (concat  ?B120 ?B5 ) ) )
    (let ( (?B122 (concat  ?B121 ?B6 ) ) )
    (let ( (?B123 (concat  ?B122 ?B7 ) ) )
    (let ( (?B124 (concat  ?B123 ?B8 ) ) )
    (let ( (?B125 (concat  ?B124 ?B9 ) ) )
    (let ( (?B126 (concat  ?B125 ?B10 ) ) )
    (let ( (?B127 (concat  ?B126 ?B11 ) ) )
    (let ( (?B128 (concat  ?B127 ?B12 ) ) )
    (let ( (?B129 (concat  ?B128 ?B13 ) ) )
    (let ( (?B130 (concat  ?B129 ?B14 ) ) )
     (let ( (?B131 (=  (_ bv0 64) ?B130 ) ) )
      (let ( ) ?B131 )
     )
    )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   )
  )
 )
)
(check-sat)
(get-value (dummy1127) )
(get-value (reservedconst_32) )
(exit)