Applying bit blasting to quantified variables results in type error

[tneele]

Take the following SMT2 file, stored in test.smt2:

(assert
  (exists ((x1 (_ BitVec 2)) (x2 (_ BitVec 2)) )
    (= ((_ extract 0 0) (ite (bvugt x1 x2) #b01 #b01)) (_ bv1 1))
  ))
(check-sat)
(apply (using-params bit-blast :blast_quant true))

Running Z3 yields:

$ z3 test.smt2 
sat
(error "line 6 column 49: Sort mismatch at argument #1 for function (declare-fun mkbv (Bool Bool) (_ BitVec 2)) supplied sort is (_ BitVec 2)")

Thus, parsing and type checking is fine and the satisfiability result is as expected. However, after applying bit blasting to the two quantified variables, an unexpected type error pops up.

platform: Ubuntu 23.10, GCC 13.2.0
Z3 version: both 4.12.4 and a fresh build from master have this issue.