Fix satsub64be() to unconditionally use 64-bit integers