Key points are not available for this paper at this time.
Satisfiability Modulo Theories (SMT) is a decision problem for logical formulas over one or more first-order theories. In this paper, we study the problem of finding all solutions of an SMT problem with respect to a set of Boolean variables, henceforth All-SMT. First, we show how an All-SMT solver can benefit various domains of application: Bounded Model Checking, Automated Test Generation, Reliability analysis, and Quantitative Information Flow. Secondly, we then propose algorithms to design an All-SMT solver on top of an existing SMT solver, and implement it into a prototype tool, called aZ3. Thirdly, we create a set of benchmarks for All-SMT in the theory of linear integer arithmetic QFLIA and the theory of bit vectors with arrays and uninterpreted functions QFAUFBV. We compare aZ3 against Math SAT, the only existing All-SMT solver, on our benchmarks. Experimental results show that aZ3 is more precise than Math SAT.
Phan et al. (Sat,) studied this question.