Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael
This paper describes a method for combining "off-the-shelf" SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning don't care to as...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.