Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. In this repository, I will learn Z3, an efficient SMT Solver from Microsoft Research, to apply it in software verification, software testting, constraint solving, analysis of hybrid systems, security, biology and analysis applications.

In this Jupyter Notebook, I've followed these tutorials. https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ece.uwaterloo.ca/~agurfink/stqam/assets/pdf/W04-UsingZ3.pdf