Our FAQ section could discuss what solvers are more appropriate to use in each case. Our team has some insight into this which could be valuable for many other users. In addition, there are certain options that we routinely use for speeding up harnesses like --no-memory-safety-checks. This is often appropriate if there is no usage of unsafe code, so we should mention it.