SMT Solving
SMT stands for Satisfiability Modulo Theories. It is a decision problem for logical formulas with respect to combinations of background theories.
Bit-Vectors, Floating Points, etc.
See bvfp_solver.py
Linear Arithmetic
See lira_solver.py
Strings
TBD