1 Theorem prover. Uses Nelson-Oppen approach. A part of Extended Static Checking project (ESC). 2 Input: first-order formula, including quantifiers. Theories: equality, linear rational arithmetic, linear integer arithmetic. To check the validity of a conjecture G, Simplify tests the satisfiability of ¬G. Uses backtracking search.

3 Theory of equality: =. Theory of arithmetic: +, —, ×, >, <, ≥, ≤.

Sergey Vartanov, 2007–2020