With the rapid increase in size and complexity of software, more and more attention is paid to thesoftware’s trust. Verifying whether programs satisfy the properties described by assertions is a common method toguarantee trust of the software. Since path sensitive program verification cannot traverse all paths, it needs mergethe path information, which causes a loss of precision. The study proposes a program verification method usingSMT solvers, which can reduce the path search space and improve the precision at the same time. The method’smain sprit is impacting the cycle path by using maximal strongly connected component and slicing the CFGaccording to the aim assertion. The study abstracts the path space using Boolean formulas and verifies the path bycombining abstract interpretation and symbolic execution. The study has conducted experiments based on the F-Softprogram verification platform and SMT solver Z3, and results show that this method performs well based onprecision and effect.