(z3str3) Segmentation fault or assertion violation at ../src/smt/theory_str_regex.cpp Line: 967

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[521] % z3release smt.string_solver=z3str3 small.smt2
Segmentation fault
[522] % z3debug smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_str_regex.cpp
Line: 967
str1.length() == 1
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[523] % 
[523] % cat small.smt2
(assert (str.in.re "" (re.loop (re.range "" "") 0)))
(check-sat)
[524] %

OS: Ubuntu 18.04
Commit: fc8dfe3

[mtrberzi]

Opened #4360