Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination of first-order theories. We present the architecture and selected features of Boolector, which is an efficient SMT solver for the quantifier-free theories of bit-vectors and arrays. It uses term rewriting, bit-blasting to handle bit-vectors, and lemmas on demand for arrays. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Brummayer, R., & Biere, A. (2009). Boolector: An efficient SMT solver for bit-vectors and arrays. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5505 LNCS, pp. 174–177). https://doi.org/10.1007/978-3-642-00768-2_16
Mendeley helps you to discover research relevant for your work.