Abstract:

Satisfiability modulo theories solver is a decision procedure for the satisfiabilily of formulas of the firstorder logics. It is the verification engine for many formalization methods. Theory solvers solve problems with different theoretical backgrounds; however, the problems in the realworld applications often are supported by multiple theories. This paper mainly introduces the methods of theory combination, summarizes the status quo of the SMT solvers. Besides，it analyzes several major techniques on the theoretical combination for SMT solvers. Testing with the industrial cases, we finally evaluate methods of combination theory with experimental results, and compare the  performances of several popular SMT solvers which  support theoretical combination techniques.

Key words: satisfiability modulo theories;SMT solver;combination theory