Improving Stability of SMT Solvers via Context-Driven Normalization

Abstract

Abstract Satisfiability Modulo Theories (SMT) solvers are widely used in formal verification. In program analysis, users often encounter queries that differ only by simple syntactic mutations and are logically equivalent. These mutations typically include assertion reordering, symbol renaming, anti-symmetric relation inversion, and commutative operand reordering. However, such minor changes can cause runtimes to vary by orders of magnitude. This variability reduces the predictability required for industrial-scale verification and remains a critical challenge. This paper presents SMTStabilizer, a tool that improves the stability of SMT solvers via context-driven normalization. Since complete input normalization is as hard as the graph isomorphism problem, SMTStabilizer adopts an approximate normalization strategy to avoid the high cost of exact normalization. The framework converts formulas into a structured representation and propagates structural information across nodes, enabling each node to capture its surrounding context. Using this context information, SMTStabilizer derives a consistent ordering over subformulas. This process yields a nearly canonical form that remains consistent across isomorphic inputs. SMTStabilizer also leverages pruning techniques that exploit the syntactic structure of SMT formulas to reduce normalization time. Evaluation on millions of queries using Z3 and cvc5 shows that SMTStabilizer improves solver stability to over $$98\%$$ 98 % under 10 random mutations.