Z3 hangs on String formula

[muchang]

Hi,
For this formula:

(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert
 (and
  (=
   (str.at
    (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (- (str.len (str.substr c 1 (- (str.len c) 1))) 1) 0))
    (- (str.len (str.substr (str.substr c 1 (- (str.len a ) 1)) 0 (- (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1) 0))) 1))
   "x"
   )
  (not (= (str.at (str.substr (str.substr c 1 (- (str.len a) 1)) 0 (- (- (str.len (str.substr a 1 (- (str.len (str.replace a b "")) 1))) 1) 0)) 0) "y"))
  (not (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr a 1 (- (str.len a) 1))) 1)) 0) "z"))
  (= (str.at (str.substr a 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "w")
  )
 )
(check-sat)     

Z3 latest version will hang on it:

$ timeout -s 9 120 z3 test.smt2
Killed

While z3-4.8.5-stable version will give sat result quickly:

$ time z3-4.8.5-x64-ubuntu-16.04/bin/z3 test.smt2 
sat

real	0m0.049s
user	0m0.038s
sys	0m0.008s

OS: Ubuntu 18.04
Revision: 6384080