dReal(http://dreal.github.io)是一款实数域上的SMT约束求解器。