diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 00b607fbc9b..634350a620e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3070,9 +3070,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { } else if (m_util.str.is_is_digit(e)) { + } + else if (m_util.str.is_foldl(e) || m_util.str.is_foldli(e)) { + } else { TRACE("seq", tout << mk_pp(e, m) << "\n";); + IF_VERBOSE(0, verbose_stream() << mk_pp(e, m) << "\n"); UNREACHABLE(); } }