AFAIK, the AccountId sort is not needed, instead when we have an undefined account we can just use #undef_account or .Account in the Account sort instead.
Reasoning by extending the builtin sorts will definitely blow up.
Similarly, the newest version uses -1 as a "signal" value for undefined accounts. This will definitely make symbolic reasoning very difficult. It's better to not touch the builtin reasoning sorts (eg. Int or Id) at all.