diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index ca96512f0..6d8734bc9 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -438,6 +438,10 @@ namespace seq { !seq.str.is_unit(a) && !seq.str.is_itos(a) && !seq.str.is_nth_i(a) && + !seq.str.is_map(a) && + !seq.str.is_mapi(a) && + !seq.str.is_foldl(a) && + !seq.str.is_foldli(a) && !m.is_ite(a); }