(z3str3) Segmentation fault on QF_S formula with str.++, str.to.re

[muchang]

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

[511] % z3 small.smt2
sat
[512] % z3 smt.string_solver=z3str3 small.smt2
Segmentation fault
[513] % 
[513] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(assert (= c (str.++ a b)))
(assert (= d "b"))
(assert (= f (str.++ c d)))
(assert (distinct "c"))
(assert (= g (str.++ f e)))
(assert (distinct h "ab"))
(assert (= i (str.++ g h)))
(assert (str.in.re i (str.to.re "abc")))
(check-sat)
[514] %

OS: Ubuntu 18.04 Commit: f2d3160

[mtrberzi]

Opened #4413