Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. - David Chocholatý; Vojtech Havlena; Lukás Holík; Jan Hranicka; Ondrej Lengál; Juraj Síc (TACAS (2), 2025)