Want suggestion on improving performance using sequence solver

[smoy]

The following sequence problem is pretty slow to solve. (about 4s in M2 pro)

I already set z3 encoding to ascii; otherwise, the max length 45 on a is still a very big search space.

(declare-fun r () String)
(declare-fun a () String)
(assert (let ((a!1 (str.in_re (str.substr a 6 (+ (- 6) (str.len a)))
                      (re.* (re.range "!" "~")))))
  (and (>= (str.len a) 6)
       (= (str.substr a 0 6) "s3:get")
       a!1
       (str.in_re r (re.* (re.range "!" "~"))))))
(assert (let ((a!1 (str.in_re (str.substr a 3 (+ (- 3) (str.len a)))
                      (re.* (re.range "!" "~"))))
      (a!2 (str.in_re (str.substr r 29 (+ (- 29) (str.len r)))
                      (re.* (re.range "!" "~")))))
(let ((a!3 (or (= r "arn:aws:s3:::sample-bucket-1")
               (and (>= (str.len r) 29)
                    (= (str.substr r 0 29) "arn:aws:s3:::sample-bucket-1/")
                    a!2))))
  (not (and (>= (str.len a) 3) (= (str.substr a 0 3) "s3:") a!1 a!3)))))
(assert (let ((a!1 (str.in_re r
                      (re.++ (str.to_re "arn:aws:s3:::sample-bucket-1/")
                             (re.* (re.range "!" "~"))))))
  (or (= r "arn:aws:s3:::sample-bucket-1") a!1)))
(assert (<= (str.len a) 45))

The expected answer is unsat

The formula is formed using modeling this policy:

[
        {
            "Sid": "read_everything",
            "Effect": "Allow",
            "Action": [
                "s3:Get*",
            ],
            "Resource": "*",
        },
        {
            "Sid": "deny-single-bucket",
            "Effect": "Deny",
            "Action": [
                "s3:*",
            ],
            "Resource": [
                "arn:aws:s3:::sample-bucket-1",
                "arn:aws:s3:::sample-bucket-1/*",
            ],
        },
    ]

When I test against access to resource (variable r) on "arn:aws:s3:::sample-bucket-1", i am pinning the r already, so the other variable a has to figure out the regex between s3:Get* in allow vs s3:* in deny.

Is there other optimization in can add to the formula or tuning other z3 parameters?