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

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.

It's not terribly inaccessible, but the learning curve is v. steep especially if you're not sure of what's at the top of it nor which bit to scale first. Obviously if you want to do SMT research it is worth scaling, but as a practitioner it is a big ask to come up to speed.

Fond hopes: more understanding of what that line is between "Oh, cool, this is trivially solvable and worked just like I expected" and "Hmmn, I wonder if my solver is ever coming back".