Hi,
For this formula:
(set-option :smt.arith.solver 1)
(declare-fun a () String)
(assert (str.in.re a (re.* (str.to.re "a"))))
(check-sat)
Z3 throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/smt/theory_diff_logic_def.h
Line: 977
(asgn == l_true) == a->is_true()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
OS: Ubuntu 18.04
Commit: 1c760b0