(smt.threads=8) Nondeterministic crash on QF_S formula

[muchang]

Z3 crashes on this formula in both release and debug builds.

[515] % for i in $(seq 1 10); do timeout -s 9 4 z3release small.smt2; done
unsat
unsat
unsat
unsat
unsat
Segmentation fault
unsat
unsat
Segmentation fault
unsat
[516] % for i in $(seq 1 10); do timeout -s 9 4 z3debug small.smt2; done
unsat
ASSERTION VIOLATION
File: ../src/smt/watch_list.h
Line: 45
m_data
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
unsat
ASSERTION VIOLATION
File: ../src/smt/watch_list.h
Line: 45
m_data
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
unsat
Killed
unsat
unsat
unsat
Killed
unsat
ASSERTION VIOLATION
File: ../src/smt/watch_list.h
Line: 45
m_data
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
Killed
[517] % 
[517] % cat small.smt2
(set-option :smt.threads 8)
(declare-fun num1 () String)
(declare-fun a () String)
(assert (>= (+ (- (- (- (- 1) 1) 1) 1) (str.len a)) 0))
(assert (ite (str.prefixof "-" a) (and (> (str.len a) 1)) (ite (= 0
  (str.to_int a)) false true)))
(assert (> (str.len (str.++ (str.++ (str.++ (str.from_int (- (+ (+
  (ite (str.prefixof "-" (str.at num1 (+ (str.len num1)))) 0
  (str.to_int (str.at num1 0))) (ite (str.prefixof "-" (str.at a (+
  (str.len a) (- 3)))) 0 (str.to_int (str.at a 0))))) 10)))
  (str.from_int (- (+ (+ (ite (str.prefixof "-" (str.at num1 0)) 0
  (str.to_int (str.at num1 (+ (str.len num1) (- 2))))))))))
  (str.from_int (+ 0)))) (str.len a)))
(check-sat)
[518] %

Commit: 4d55f83