let sym_d_bv_conc = function Bv(Conc(n, m)) -> (n, m) | _ -> assert false