let sym_is_bv_sub = function Bv(Sub _) -> true | _ -> false