Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.
Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.)
---
[1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers"
[2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B...
[3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...
* Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-pro...
* Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-cont...
* Synthetic Minds (that is us): https://synthetic-minds.com/
You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.
Its facilities for program construction over the integers, sets, bitvectors, and reals make it an ideal candidate for this, especially when leveraging nu-Z3 for optimization over these.
With Z3, we’re able to construct optimized routes for robots extremely fast (especially with extensions over the techniques described in [1]), and as a direct result, derive value for our customers as execution time is important when dealing with expensive equipment.
A couple of my friends over at trail of bits do the work that saurabh does at synthetic minds, and their code is open source so you can take a look at it. [2]
It’s a decently active field of research, with solvers trading blows in the annual SMT-COMP [3]. check out their instances to see how people really use them.
[1] https://papers.nips.cc/paper/8233-learning-to-solve-smt-form...
[2] https://www.trailofbits.com/services/blockchain-security/