(declare-fun a () String)
(declare-fun z () String)
(declare-fun c () String)
(declare-fun aa () String)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun b () Bool)
(declare-fun f () Bool)
(declare-fun GohuV_new () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun ac () String)
(declare-fun j () Int)
(declare-fun k () String)
(declare-fun m () String)
(declare-fun n () String)
(declare-fun l () String)
(declare-fun p () Bool)
(declare-fun s () Bool)
(declare-fun o () Bool)
(declare-fun t () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun u () String)
(declare-fun v () Bool)
(declare-fun w () Bool)
(declare-fun af () String)
(assert (= (= d (not (= e s))) (= "" (str.substr ac 21 (str.len u)))))
(assert (= (= "-" (str.substr ac 25 (str.len u))) o s))
(assert (= f (and (= GohuV_new q))))
(assert
 (=
  (not (= j 43))
  (or (= (str.substr z 21 (str.len m)) "__utma=16886264.")
   (or
    (str.in.re
     (str.substr c 30 (str.len n))
     (re.++
      (str.to.re "")
      (re.++
       (str.to.re "")
       (re.++
        (str.to.re "")
        (re.++
         (str.to.re "t")
         (re.++
          (str.to.re "")
          (re.++
           (str.to.re "a")
           (re.++
            (str.to.re "=")
            (re.++
             (str.to.re "1")
             (re.++
              (str.to.re "6")
              (re.++
               (str.to.re "8")
               (re.++
                (str.to.re "8")
                (re.++
                 (str.to.re "6")
                 (re.++
                  (str.to.re "2")
                  (re.++
                   (str.to.re "")
                   (re.++
                    (str.to.re "")
                    (str.to.re ".")))))))))))))))))))
  (or (= j 0) (= g (not (= h r))))
  (= "" (str.substr ac 0 (str.len u)))
  (or (= h v))))
(assert (not (= i v)))
(assert
 (=
  (or f t)
  (not (= d p))
  (and
   (=
    ""
    (str.substr
     a
     (str.len k)
     (str.len
      (str.substr
       z
       (str.len m)
       (str.len
        (str.substr
         aa
         (str.len l)
         (str.len
          (str.substr ac (str.len u) (str.len af))))))))))))
(assert (not (= b o)))
(assert (= a (str.++ k af) z (str.++ m af)))
(assert (= c aa (str.++ l af)))
(assert (= d (not (= p w))))
(assert (= e (or (= s w)) b f (and (= r v))))
(check-sat)

% z3 small.smt2
sat
% z3 model_validate=true small.smt2
sat
% z3 smt.string_solver=z3str3 small.smt2
sat
% z3 smt.string_solver=seq model_validate=true small.smt2
sat
% z3 smt.string_solver=z3str3 model_validate=true small.smt2
unsat