All-Solution Satisfiability Modulo Theories: Applications, Algorithms and Benchmarks

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 QF_LIA and the theory of bit vectors with arrays and uninterpreted functions QF_AUFBV. 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.