Some small demo scripts for SMTLIB and Z3 basics. Originally used as quick demonstrations during an internal talk on bitvector logic and SAT/SMT Solvers based on the 2016 edition of Decision Procedures [1] by Kroening & Strichman. The accompanying slides (which are directly derived from material in the book) can be found at [2].

[1] http://www.decision-procedures.org/

[2] https://goo.gl/a1W1b9