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