1. A computer-implemented method, for modeling and verifying false paths in integrated circuit (IC) design, comprising: receiving a constraints file that includes at least one definition of a false path; for each false path in the constraints file, identifying re-convergence points in an input netlist of the IC design; modeling the false path together with the re-convergence points to produce a satisfiability formula; verifying the satisfiability formula using a Boolean satisfiability solver; storing a verification result of the verifying step in the memory of the computer; and providing a verification output based on the verification result; wherein a re-convergence point is a point in the false path that starts from a starting point and does not pass through at least one preceding through point.