Metamorphic testing reveals floating-point slowdowns in SMT solvers
Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers
Programming Languages
Summary
SMT solvers are programs used to solve complex math problems that arise in software verification and creation. This work shows that simplifying certain floating-point math problems can surprisingly make these solvers run much slower. The researchers used a testing method that modifies problems without changing their meaning to find these slowdowns in popular solvers. They also found that random test problems are less effective at revealing these performance issues than real-world examples.
What this means in practice
- •For software verification teams: Identify and fix cases where simplifying floating-point formulas unexpectedly slows down SMT solvers during verification tasks.
- •For formal methods engineers: Use metamorphic testing with real-world floating-point queries to evaluate and improve solver efficiency.
Authors
Rosa Abbasi, Eva Darulova
Abstract
SMT solvers are essential in various domains, including program verification and synthesis. Although their correctness and performance have been extensively studied, performance testing for the floating-point theory remains limited, particularly for real-world queries. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values and peep-hole optimizations, to uncover meaningful performance issues in SMT solvers' handling of floating-point formulas. Using real-world test inputs, our approach is able to identify for every solver tested SMT queries for which solving time increases when the queries are simplified; we see slowdowns of up to 33.4x for Z3, 5.6x for MathSAT, 4.5x for cvc5, and 1.8x for Bitwuzla. We further observe that the approach is less successful when using input files that were randomly generated from a grammar.