diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index c4005f9857..166f12096a 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -515,6 +515,8 @@ namespace smt { prefix.push_back(v), tl = tl1; + VERIFY(!(str().is_concat(tl, hd, tl1) && str().is_unit(hd))); + if (prefix.empty()) return false;