Does Z3 use Z3str4?

[heroinedd]

Hi all,

Does anyone know whether Z3str4 (Z3str4: A Multi-armed String Solver) is integrated in Z3? If so, is it enabled by default?

Thanks!

[smoy]

@heroinedd apparently not:

z3/src/params/smt_params.cpp

Line 192 in 30830aa

if (s == "z3str3" || s == "seq" || s == "empty" || s == "auto" || s == "none")

You can configure z3 to use one of two backends for solving strings. The default backend is called the seq solver. It solves constraints over both sequences and strings. The other backend is [z3str3](https://z3string.github.io/), which applies to strings and regular expressions over strings. Extensions to sequences operations are not supported in z3str3.

https://microsoft.github.io/z3guide/docs/theories/Strings/#introduction

[NikolajBjorner]

z3str4 was not integrated in the z3prover repository.
given that z3str3 is not being maintained I am also planning to remove it.