SMT Solving
======================
SMT stands for Satisfiability Modulo Theories. It is a decision problem for logical formulas with respect to combinations of background theories.

This page gives the theory-level entry points. Specialized solver workflows,
including parallel CDCL(T), are grouped alongside it in :doc:`index`.

Bit-Vectors, Floating Points, etc.
-----

See ``bvfp_solver.py``


Linear Arithmetic
-----

See ``lira_solver.py``

Strings
-----

TBD