As discussed in #176, the final liveness check is single threaded. At the time this was implemented, the liveness checks users wanted to use were simple enough that this wasn't a problem. However, this is no longer the case. E.g. 10f7a122b938d0d41f91bcdbe412c828c00519aa reported that one of their models takes ~5x as long to run the final liveness check as the rest of the entire checking run. We still don't have an efficient algorithm for liveness checking, but we should at least be able to ameliorate the problem by going multithreaded.
As discussed in #176, the final liveness check is single threaded. At the time this was implemented, the liveness checks users wanted to use were simple enough that this wasn't a problem. However, this is no longer the case. E.g. 10f7a122b938d0d41f91bcdbe412c828c00519aa reported that one of their models takes ~5x as long to run the final liveness check as the rest of the entire checking run. We still don't have an efficient algorithm for liveness checking, but we should at least be able to ameliorate the problem by going multithreaded.