  We present a novel length-aware solving algorithm for the quantifier-free
first-order theory over regex membership predicate and linear arithmetic over
string length. We implement and evaluate this algorithm and related heuristics
in the Z3 theorem prover. A crucial insight that underpins our algorithm is
that real-world instances contain a wealth of information about upper and lower
bounds on lengths of strings under constraints, and such information can be
used very effectively to simplify operations on automata representing regular
expressions. Additionally, we present a number of novel general heuristics,
such as the prefix/suffix method, that can be used in conjunction with a
variety of regex solving algorithms, making them more efficient. We showcase
the power of our algorithm and heuristics via an extensive empirical evaluation
over a large and diverse benchmark of 57256 regex-heavy instances, almost 75%
of which are derived from industrial applications or contributed by other
solver developers. Our solver outperforms five other state-of-the-art string
solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this
benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over
Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup
over OSTRICH.
