i haven't done solver stuff in maybe a year, i wonder if z3 works any better than it used to? it used to have problems with problems that other solvers could solve
@notwa isn't this somewhat true of every automatic prover? The design space is so large that there is always a way to do a little bit better than the existing competitors for some category of inputs, and they each do?
@spun_off true, but z3 struggled with quantifier-free bitvector problems that SAT solvers with my unoptimized bit-blaster could solve in seconds. i worry that this kind of thing leaves a bad taste for any newcomers to solvers.
@notwa For properties that come from program verification (among other classes of problems), Z3 has the highest success rate overall. Don't worry about it leaving a bad taste, if every solver out there was as consistently good at at least one thing, people would find automatic solvers more usable.
@notwa Damien Doligez (working on Zenon) told me that Zenon was solving problems where the conclusion to prove or disprove was exactly one of the hypotheses modulo alpha-conversion better than every other provers, because it has techniques that made this trivial and other provers didn't. It's just a large design space.