Bounded Model Checker Modulo Theories

Checking executions of TLA+ specifications up to a predefined execution length. Semantics of TLA+ operations is encoded in SMT.