Z3 soundness bug, rewriter.flat=false correct, z3str crashes #4275
Description
[705] % z3-4.8.5 small.smt2
sat
[706] % z3-4.8.6 small.smt2
sat
[707] % z3-4.8.7 small.smt2
unknown
[708] % z3release small.smt2
unsat
[709] % z3release rewriter.flat=false small.smt2
sat
[710] % z3release smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_str_regex.cpp
Line: 1158
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[711] %
[711] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () Int)
(declare-fun m () Bool)
(declare-fun n () Int)
(assert (distinct "" k))
(assert (= m (distinct c (- 1))))
(assert
(ite m
(and (= c b) (= k g) (= b (str.len e)) (= g "abcd")
(not (str.in.re j (re.inter (str.to.re "") (str.to.re "a")))))
(distinct d 1)))
(assert (= l (+ c 8) n l))
(assert (= a (div d n)))
(assert (>= d n))
(assert (= a (str.len f)))
(assert (= k (str.++ h f i)))
(check-sat)
[712] %
OS: Ubuntu 18.04
Commit: 9c97252