JavaSMT 3: Interacting with SMT Solvers in Java

Satisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different implementations have different strengths, it is often desirable to be able to substitute one solver by another. Unfortunately, the solvers have vastly different APIs and it is not easy to switch to a different solver (lock-in effect). To tackle this problem, we developed JAVASMT, which is a solver-independent framework that unifies the API for using a set of SMT solvers. This paper describes version 3 of JAVASMT, which now supports eight SMT solvers and offers a simpler build and update process. Our feature comparisons and experiments show that different SMT solvers significantly differ in terms of feature support and performance characteristics. A unifying Java API for SMT solvers is important to make the SMT technology accessible for software developers. Similar APIs exist for other programming languages.

Automated summary

SMT technology has many applications, but different solvers have different APIs, making it difficult to switch between them. JAVASMT is a unified API framework that supports multiple SMT solvers.