Z3str4: A Multi-armed String Solver

We present Z3str4, a new high-performance string SMT solver for a rich quantifier-free first-order theory of strings and length constraints. These kinds of constraints have found widespread application in analysis of string-intensive programs in general, and web applications in particular. Three key contributions underpin our solver: first, a novel length-abstraction algorithm that performs various string-length based abstractions and refinements along with a bit-vector backend; second, an arrangement-based solver with a bit-vector backend; third, an algorithm selection and constraint-sharing architecture which leverages the above-mentioned solvers along with the Z3 sequence (Z3seq) solver. We perform extensive empirical evaluation over 20 different industrial and randomly-generated benchmarks with over 120,000+ instances, and show that Z3str4 outperforms the previous best solvers, namely, CVC4, Z3seq, and Z3str3 in both total solved instances and total runtime.