[OxO4]

Out of curiosity, what made you choose Z3 over other SMT solvers? Also, if you have benchmarks that you can publish, it would be really great if you could submit them to SMT-LIB/SMT-COMP [0] such that they can be used to improve SMT solvers.

[0] https://smt-comp.github.io/news/2019-01-24.html

[saurabh20n]

About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances.

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...