dReal: An SMT Solver for Nonlinear Theories of the Reals