This paper presents a fully SAT-based method for unbounded symbolic model checking using Craig interpolants. The method is more efficient than BDD-based symbolic model checking and performs well compared to recent SAT-based methods on positive instances. The approach uses SAT solvers to generate refutations and interpolants, which are used for finite-state reachability analysis and LTL model checking. The method is applied to verify properties of commercial microprocessor designs. The paper compares the performance of the interpolation-based method with other approaches, such as proof-based abstraction and structural methods. The results show that the interpolation method is more efficient in verifying properties, especially for large industrial circuit verification instances. The method is able to handle a large number of state variables and is not limited by the number of inputs. The paper also discusses optimizations and practical experience with the method, showing that it can successfully verify a wide range of properties in benchmark studies. The method is based on the use of interpolants derived from proofs of unsatisfiability, which are used to approximate reachable states and check for counterexamples. The paper concludes that interpolation and bounded model checking can be combined to allow unbounded model checking, which is more efficient than BDD-based methods and some recent SAT-based approaches.This paper presents a fully SAT-based method for unbounded symbolic model checking using Craig interpolants. The method is more efficient than BDD-based symbolic model checking and performs well compared to recent SAT-based methods on positive instances. The approach uses SAT solvers to generate refutations and interpolants, which are used for finite-state reachability analysis and LTL model checking. The method is applied to verify properties of commercial microprocessor designs. The paper compares the performance of the interpolation-based method with other approaches, such as proof-based abstraction and structural methods. The results show that the interpolation method is more efficient in verifying properties, especially for large industrial circuit verification instances. The method is able to handle a large number of state variables and is not limited by the number of inputs. The paper also discusses optimizations and practical experience with the method, showing that it can successfully verify a wide range of properties in benchmark studies. The method is based on the use of interpolants derived from proofs of unsatisfiability, which are used to approximate reachable states and check for counterexamples. The paper concludes that interpolation and bounded model checking can be combined to allow unbounded model checking, which is more efficient than BDD-based methods and some recent SAT-based approaches.