JavaSMT: A Unified Interface for SMT Solvers in Java

Satisfiability Modulo Theory (SMT) solvers received a lot of attention in the research community in the last decade, and consequently their expressiveness and performance have significantly improved. In the areas of program analysis and model checking, many of the newly developed tools rely on SMT solving. The SMT-LIB initiative defines a common format for communication with an SMT solver. However, tool developers often prefer to use the solver API instead, because many features offered by SMT solvers such as interpolation, optimization, and formula introspection are not supported by SMT-LIB directly. Additionally, using SMT-LIB for communication incurs a performance overhead, because all the queries to the solver have to be serialized to strings. Yet using the API directly creates the problem of a solver lock-in, which makes evaluating a tool with different solvers very difficult. We present JavaSMT, a library that exposes a solver-independent API layer for SMT solving. Our library aims to close the gap between API-based and SMT-LIB-based communication, by offering a large set of features with minimal performance overhead. JavaSMT has been used internally in CPACHECKER since inception, and has been heavily tested in different verification algorithms.