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.

My best advice is to rewrite your query in every different way you can think to issue it, observe the often initially counter-intuitive performance differences, and A/B test your way to acceptable performance. I rewrote some 2KLOC queries 10+ times. Not ideal but builds intuition

Some theory helps, too. E.g., the equality theory is one of the simpler ones. Try replacing every possible part of your query with an equality predicate of some sort. You might be shocked at the results... I was.

Aggressively eliminate the more complex theories whenever possible. Using the array theory? Maybe you can get away with just the bitvector theory if you pose the query differently somehow.