CVC4（http://cvc4.cs.nyu.edu）是一款支持丰富理论域的SMT约束求解器，目前由NYU和U Iowa联合开发和维护。