Mathias Preiner is a Research Scientist at Stanford University in the Centaur lab. He is one of the main developers of the SMT solver Boolector (since June 2012) and Bitwuzla -- which is what he joined us to discuss today. This was a good talk, but an excellent Q&A, and we really enjoyed it. Thanks Mathias for joining us today, and to the awesome audience for showing up with such deep and technical questions!