nlsat assertion violation at ../src/nlsat/tactic/goal2nlsat.cpp Line: 208

[muchang]

Hi,
For this formula:

(declare-fun a () String)
(assert (ite true (str.in.re a (str.to.re "")) false))
(check-sat-using nlsat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/nlsat/tactic/goal2nlsat.cpp
Line: 208
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

While Z3 does not throw out assertion violation on this equivalent formula:

declare-fun a () String)
(assert (str.in.re a (str.to.re "")))
(check-sat-using nlsat)

OS: Ubuntu 18.04
Commit: aaf2c3b