Conjecture on SMT Solver Instability Causes

This document is a research article that investigates the instability issues faced by SMT (Satisfiability Modulo Theories) solvers, particularly in the context of automated verification. It presents a conjecture that the instability is primarily due to fixable engineering problems rather than fundamental theoretical limitations. The authors conducted case studies on 11 unstable queries from verification projects and identified root causes such as solver bugs, misconfiguration, and misaligned user expectations. The analysis suggests that existing metrics for instability are inadequate and proposes the need for better tools and methods for debugging instability. The article discusses the architecture of the Z3 solver and highlights the challenges posed by instability, including performance variations from minor input changes. The authors call for improved debugging tools, better instability metrics, and controlled randomness in SMT solvers to enhance usability and reliability in formal verification processes.