Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

veriT : everyone said generating proofs from a compact and competitive solver was impossible, veriT proves (ha ha) they are wrong.

Yices : ever thought of a great idea, implemented it and then found you still couldn't beat another solver because they thought of it first? It was Yices that thought of it first.

Z3 : the most famous and widely used solver because of it's robust performance and speedy support.

All gratuitously my opinion, YMMV, hope that helps.

Thanks so much! I've looked at SMTCOMP results before but still been a bit lost. Good advice on sticking to smtlib format - I was lazy and the Python interface was tempting. But I've seen most of my workload turn to bitvector stuff so CVC4, Boolector and Yices seem worth trying.

... honestly, at this stage, the best solver is nice, but community and documentation are important. I'm having a lot of trouble with the gap between "hi noob, want to solve Sudoku or find a De Bruijin sequence?" and scientific papers that assume I'm already a SMT researcher.

As I've said before, I feel like one of those apes in 2001 poking the monolith with a stick whenever I use an SMT solver. Building a better mental model of how it works - preferably without having to ingest enough theory to become an SMT researcher in the process - would be nice.

There isn't too much written between the two I'm afraid. Performance optimisation is a black art TBH. That said I hope the research community is not too inaccessible.