DiverFPS: Generating Diverse Solutions for Floating-Point SMT Formulas

Satisfiability Modulo Theories (SMT) is a fundamental technique underpinning a wide range of applications in software engineering and testing. Among various SMT theories, the theory of floating-point plays a crucial role in practical software systems, yet reasoning about floating-point constraints remains challenging. Although existing SMT solvers are capable of producing single solutions, many applications, particularly in software testing and verification, require diverse sets of solutions to adequately exercise program behaviors. While achieving high diversity is essential for exploring system behaviors, it is also important to limit the number of generated solutions, as overly large solution sets can considerably increase testing time and resource consumption, thereby diminishing efficiency. In this work, we propose DiverFPS , a novel floating-point SMT sampler designed to generate small solution sets that achieve high target abstract syntax tree (AST)-coverage, which is commonly regarded as the standard metric for assessing solution diversity in the SMT sampling domain. DiverFPS operates in two stages: an exploration stage that aims to achieve the target AST-coverage as fully as possible, and a pruning stage that prunes redundant solutions while preserving the target AST-coverage. We further introduce three novel techniques, namely solution-driven restart strategy, context-aware encoding technology, and coverage-driven pruning strategy, which enhance the performance of DiverFPS . Extensive experiments on publicly available SMT-LIB benchmarks for QF_FP and QF_BVFP logics demonstrate that DiverFPS outperforms state-of-the-art SMT samplers. It successfully achieves the target AST-coverage on a larger number of benchmarks, which existing samplers fail to reach, while producing solution sets that are up to 92.9These results demonstrate that DiverFPS is a high-performing sampler for floating-point SMT sampling.