Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

Abstract

The SMT-LIB language and the B language are both based on predicate logic and share the definition of several operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation from SMT-LIB to B. Using this translation, SMT-LIB can be analyzed by tools developed for the B method. We show how Atelier B can be used for automatic and interactive proof of SMT-LIB problems. Furthermore, we incorporated our translation into the model checker ProB and applied it to several benchmarks taken from the SMT-LIB repository. In contrast to most SMT solvers, ProB relies on finite domain constraint propagation, with support for infinite domains by keeping track of the exhaustiveness of domain variable enumerations. Our goal was to see whether this kind of approach is beneficial for SMT solving.