Interesting discussion of different SAT solver's in Conda's package resolution, and their performance: https://github.com/Z3Prover/z3/issues/211