Taming Cyclic Dependencies in Stabilization-Based String Constraint Solving

Overview & Synopsis

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.