Z3 extension solves cyclic string constraints more effectively
Taming Cyclic Dependencies in Stabilization-Based String Constraint Solving
Logic in Computer Science
Summary
Solving puzzles involving strings and equations can get stuck when variables depend on each other in loops. The paper’s authors improved a solver named Z3-Noodler by adding special techniques that recognize and handle these loops directly. Their new tool, Z3-Noodler-C, avoids endless guesswork and finds solutions faster and more reliably. Tests show it solves many tough problems that previous tools could not.
What this means in practice
- •For software verification teams: Analyze programs with complex string operations involving cyclic dependencies more effectively using improved string constraint solving.
- •For security testing engineers: Enhance detection of bugs and vulnerabilities in software that uses string manipulation by solving cyclic string constraints accurately.
Authors
Siyi Wu, Bican Xia
Abstract
Word equations with cyclic variable dependencies pose a challenge to SMT string solvers. In stabilization-based procedures, such dependencies can trigger repeated refinement of regular-language assignments without reaching stability. We present Z3-Noodler-C, an extension of Z3-Noodler, combining equality-aware stabilization with dedicated loop reasoning. We introduce equality predicates to retain relevant equations as single stability obligations, and extend stabilization with equality-aware substitution and adapted concatenation-eliminating refinement to expose cyclic dependencies as overlapping variable bindings. Dedicated loop reasoning rules then exploit the periodic structure of these bindings, avoiding certain infinite derivations. We evaluate Z3-Noodler-C against Z3-Noodler, cvc5 and OSTRICH2. On 64 systematically generated, syntactically simple instances involving cyclic dependencies and regular constraints, our solver solves all instances, compared with only 20 solved for the best baseline. On equation-oriented instances from SMT-LIB'25, Z3-Noodler-C achieves the highest coverage, solving 20 more instances than Z3-Noodler while maintaining competitive aggregate CPU time.