Summary: We describe the open-source tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. dReal implements the framework of \(\delta \)-complete decision procedures: It returns either unsat or \(\delta \)-sat on input formulas, where \(\delta \) is a numerical error bound specified by the user. dReal also produces certificates of correctness for both \(\delta \)-sat (a solution) and unsat answers (a proof of unsatisfiability).
For the entire collection see [Zbl 1264.68002].