Solving String Split Constraints via Structural Relaxation

Abstract

String operations are integral to program analysis, yet reasoning about the ubiquitous split operation remains a challenge. SMT solvers have difficulty with split because it transforms a string into a variable-length sequence, creating a structural mismatch that leads to uninterpreted abstractions or unsound bounded approximations. In this paper, we bridge this gap with a precise, SMT-LIB-compliant encoding. Our key insight is structural relaxation: exploiting the sparsity of real-world constraints, we decouple the split structure from strict length requirements, materializing segments only on demand. We further introduce position-aware constraints to handle complex regex-based delimiters without overlaps. We evaluated our framework on 580 benchmarks using four leading string solvers. Our encoding enables off-the-shelf solvers to handle split constraints, solving 157 out of 168 real-world benchmarks and outperforming current baselines. Notably, our framework involves complex string operations, revealing 12 previously unknown implementation bugs in mainstream solvers.