SMT resources

ericpony.github.io/z3py-tutorial/guide-examples.htm
http://ericpony.github.io/z3py-tutorial/advanced-examples.htm
https://theory.stanford.edu/~nikolaj/programmingz3.html
A big tutorial: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf

Strategies/goals/tactics: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

Modelling a logic puzzle. Interesting because it uses uninterpreted functions https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle

An example of using z3 regular expressions to restrict possible strings: https://stackoverflow.com/questions/53808101/defining-constraints-in-z3-using-boolean-operators

In the 2018 talks, there’s a section on code synthesis using z3 https://cseweb.ucsd.edu/~npolikarpova/

A series of posts on using z3 to generate traces for ARM instructions https://alastairreid.github.io/tracing-smt3/

A book chapter on ways to apply z3 to program verification https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-smt-application-chapter.pdf