Understanding string solver performance in z3

[smoy]

I turn a support policy (see attachment) with string variable a, r. when i add the constraint of s3: prefix of variable a. it takes really slow to compute sat. Is there some way to formula the constraints to something more efficient for sat checking?

support_policy.txt

[smoy]

I notice by switching the constraint from PrefixOf (9.21 sec) to substring (SubString(a, 0, 3) == "s3:" ) checking (2.59 sec) is faster.