We propose an Instability Track for SMT-COMP to address the critical issue of solver instability in program verification. SMT solvers often exhibit significant performance variations when solving semantically equivalent queries, creating challenges for industrial adoption of SMT-based verification. We describe Mariposa, our tool that measures solver instability by creating semantics-preserving mutants of SMT queries and performing statistical analysis. The proposed track would evaluate solvers both on their ability to solve verification queries quickly and their stability across query variations. We discuss benchmark sources from Dafny, F⋆, and Verus verification projects, and propose concrete scoring rubrics for evaluating solver stability.
SMT competition [
Scoring Metrics. We discuss several potential scoring metrics for an instability track. We start with some definitions. If we run Mariposa on a query , it tells us that the query is solvable, unstable, or unsolvable. We define as the set of solvable queries, as the set of unstable queries, and as the set of unsolvable queries. We use for the timeout and for each query , we define as the time taken to solve . We define a very simple scoring metric:
A. Solved Score: The solver with the greatest || “wins.” This rewards solvers that can stably solve more queries. However it has two potential issues: 1. This metric does not consider the amount of time on each solvable query. For instance, we may want to reward solvers that solve queries quickly. 2. A solver is punished equally for failing to solve a query and for being unstable on a query.
However, since this is the instability track, we may want to punish unstable queries more. For each of these issues we propose a fix:
B. PAR-2I Score: Inspired by the PAR-2 score used in the SAT and SMT competitions, we propose the PAR-2I score. The PAR-2I score is the sum of the time taken to solve each solvable query plus two times the timeout for each unstable or unsolvable query. Specifically, the score is ∑︀∈ + 2 · · | ∪ |. The solver with the lowest such score “wins.” C. Instability Score: The instability score is similar to the solved score, but “punishes” unstable queries more than unsolvable queries. Specifically the score is || − | | and the solver with the highest such score “wins.”
The PAR-2I score is a fix for issue 1 and the instability score is a fix for issue 2. We could also consider a hybrid approach that combine these two methods. The exact scoring mechanism will be finalized based on community feedback.
Other Features. There are two interesting eccentricities of these SMT queries that could be incorporated into the track.
• Goal-Axiom Divide. Program verification tools like Dafny, F ⋆, and Verus have a clear divide between the goal assertion and the axiom assertions. The goal captures the property we want to prove. For instance, this could be an assertion, ensures clause, or loop invariant at the source level. The axioms correspond to ambient facts at the source level from other functions, user-created lemmas, or language-level definitions.
This can be recognized by the SMT track by having queries annotate the goal assertion. • Fast Unknowns vs. Timeouts. Mariposa deems a query unstable for a solver if it cannot solve some of the semantically equivalent queries produced. However, there are two types of unstable queries: fast unknowns are when the solver quickly returns unknown and timeouts are when the solver uses its entire time budget without finding a solution. We believe that this corresponds to diferent issues inside the SMT solver: the former is when quantified axioms are underinstantiated, while the latter are when quantified axioms are overinstantiated. Figure 1 shows the distribution of failure modes in unstable queries, showing a clear divide between fast unknowns and timeouts. This can be recognized in SMT track by noting the number of fast unknowns and timeout failures for each solver. This would allow solvers to be scored on both of these metrics.
Mariposa-bench Verus-bench 43.5% 14.0% 44.9%
21.9%
20.0%
0.1 1.0 10.0
Time Until Failure Log Scale (seconds)
60.0
Solutions. There has been some work trying to fix instability. Shake automatically prunes the
solver’s context by removing redundant axioms in a pre-processing step [
All of this work improves stability, but does not address key underlying issues, and instability is still prevalent when we apply these fixes. More work is required. We believe that much of this work can be done at the SMT-solver level and thus a stability track at the SMT competition could be immensely helpful for encouraging solver developers to improve stability.
Drawbacks. Many program verification tools are built with Z3 in mind, so other solvers may perform worse initially. However, we hope that introducing an instability track can incentivize all solvers to perform better on verification queries and encourage verification tools to use diferent solvers.
Another drawback is that measuring instability requires running many diferent mutants of a query, which could be computationally expensive. However, this is mitigated since program verification tools require much shorter timeouts (usually 60 seconds or less) compared to many other SMT queries. Conclusions. In conclusion, we argue that instability is a critical issue for SMT-based program verification. We believe this is a problem that could be addressed at the solver level. We hope that an instability track at the SMT competition could be a step in this direction. Acknowledgements We would like to thank the anonymous reviewers for their helpful feedback. We further acknowledge Dominic Winterer and the organizers of the SMT-COMP for the suggestion to present this at the SMT workshop. We thank all of the contributors to the Mariposa project and the Dafny, F⋆, and Verus developers for contributions to the benchmark suite.
This work was supported in part by the National Science Foundation (NSF) under grant 2224279, funding from AFRL and DARPA under Agreement FA8750-24-9-1000, and the Future Enterprise Security initiative at Carnegie Mellon CyLab (FutureEnterprise@CyLab).
Declaration on Generative AI. The authors have not employed any Generative AI tools.