Z3str3 String Constraint Solver

Z3str3 is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3str3 is now part of the Z3 theorem prover's main codebase, and is the primary string solver in Z3.

The Z3str3 string solver is being actively developed in close cooperation with the Z3 team at Microsoft Research. Additionally, this research is being supported by IBM, Amazon, Google, and NSERC Canada through various grants, awards, and research collaborations.

Latest Stable Release: Official Z3 repository

The benchmarks (for Z3str2) used in CAV'15 paper are available in the Github Repo.

Release history

2017-05-05 (1) Z3str3 1.0.0 released. 
(2) Support for SMT-LIB 2.5 strings draft standard added.
2015-02-09 (1) Z3str2 1.0.0 released.
(2) Regex support added.
(3) Overlapping variables detection.
(4) Bi-directional integration between string and integer theories.

2014-12-05 (1) Change version identifier to Z3-str 1.0.0.
(2) String/Integer theory integration.
(3) Fix Several bugs.
(4) Performance optimization tweaks.

2014-07-20 (1) Remove the upper bound of the length searched for free variable.
(2) Use the 256 ASCII character set as the default alphabet.
(3) Fix Several bugs.
(4) Performance optimization tweaks.

2014-01-20 (1) Return "UNKNOWN" for not well-formed inputs whose solution may be in the ignored loop-inducing cuts. 
(2) Allow setting the upper bound of length searched for free variables.
(3) Minor bugs fixed.
(4) The universe of the value of free variables changed from {'@'} to a set of alphabets
(5) Supports for operators "StartsWith" and "EndsWith" added

2013-10-03 (1) Solving procedure improved. On average, it runs ~3.5x faster than the initial release.
(2) Bugs fixed.

2013-06-02 Initial release