Abstract
Satisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-standing challenge, which has been a major bottleneck of practical application of SMT solvers in some fields. We reveal a decidable fragment of FOL involving quantifiers, which could not be solved by SMT solvers such as Z3, CVC3, etc., and show how to convert them into model checking problems.