Z3 seems cool and I want to try but I must admit I fail to see how to use it for a real world project. Do you have a blog post talking about your Z3 use for your project?
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/
* 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.