We currently use MathSAT5 as the default SMT solver for everything related SMT. Due to the newly released JavaSMT 6.0.0 and its many updates and updated solvers, we should take a close look at available solvers and their performance, to evaluate the best possible default solver for CPAchecker as a whole, and possibly even more fine grained (e.g. per analysis/specification/config). We should also analyze whether distinct solvers can yield distinct results and possibly extend our portfolios with more solvers for existing configurations. Is blocked by !503.