let rec mk_unsigned = 
  let unsigned = mk_app (Bvarith(Unsigned)) in
    function
      | App(Bv(Const(b)), []) ->
          Arith.mk_num (Q.of_int (unsigned_interp_of b))
      | App(Bv(Conc(n, m)), [x; y]) ->
          let ux = mk_unsigned x 
          and uy = mk_unsigned y in
          let two_expt_m = Q.of_z (Z.expt (Z.of_int 2) m) in
            Arith.mk_add (Arith.mk_multq two_expt_m ux) uy
      | a -> 
          unsigned [a]

and unsigned_interp_of b =
  Bitv.fold_right 
    (fun x acc -> 
       if x then 2 * acc + 1 else 2 * acc) 
    b 0