A QF_S test case make z3 unable to return results

[drogonFan]

For this test case, I can get the result "unsat" quickly by using cvc4, but z3 can't get the result for a long time.

(set-logic QF_S)
(declare-fun var0 () Int)
(declare-fun var4 () String)
(assert (>= (str.len "s[""PBv%Ut'\r'f") (str.to.int (str.at var4 14))))
(assert (>= (str.to.int var4) (str.len "Ne0X4g0-yOl<")))
(assert (<= (str.len var4) (str.len (str.at var4 var0))))
(assert (<= 10 34))
(assert (>= (str.len (str.at "OCV>}8Py" var0)) (str.len (str.at "'\x0c'dja0voh" 14))))
(assert (<= 5 22))
(check-sat)

I'm not sure if it is a syntax error in this test cast. Is this a potential bug?

Ps： This is my running screenshot

[mtrberzi]

It doesn't look like a syntax error to me. It is most likely a performance issue with the way Z3str3 handles the operators you've used. I'll take a look and see if there is anything simple that can be done.