Windows Sysinternals

https://technet.microsoft.com/en-us/sysinternals/bb842062

The Sysinternals Troubleshooting Utilities have been rolled up into a single Suite of tools. Extremely useful in the command line environment.

The Z3 SMT solver

Z3 is a Satisfiability Modulo Theories (SMT) solver. It is an automated satisfiability checker for many-typed first-order logic with built-in theories, including support for quantifiers. The currently supported theories are:

• equality over free (aka uninterpreted) function and predicate symbols
• real and integer arithmetic
• bit-vectors and arrays
• tuple/records/enumeration types and algebraic (recursive) data-types.

Z3 checks whether a set of formulas is satisfiable in the built-in theories. When the set of formulas is existential then Z3 is a decision procedure: it is always guaranteed to return a correct answer.

• If a set of formulas F is satisfiable, Z3 can produce a model for F.
• If a set of formulas contains universal quantifiers, then the model produced by Z3 should be viewed as a potential model, since Z3 is incomplete in this case.