A timeout test case for z3str3

[drogonFan]

(set-logic QF_S)
(declare-fun var3 () Int)
(declare-fun var0 () String)
(declare-fun var2 () String)
(assert (> (str.indexof "+]YAPKJ8b8" var2 var3) (str.to.int var0)))
(check-sat)

This test case triggers a timeout problem. It seems cause z3str3 to loop endlessly at some point in the code.

For example, in ast.cpp(using gcov):

Whether this could be a performance issue?