==Expressive power of SMT==An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories.
== Выразительная сила SMT ==SMT-формула — это обобщение булевой формулы SAT, в которой переменные заменены предикатами из соответствующих теорий.