From 831152547211a4d21d5c1bc3dff2a5a991e26bb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Sep 2022 16:03:24 -0700 Subject: [PATCH] map and fold cannot be treated as variables --- src/ast/rewriter/seq_eq_solver.cpp | 4 ++++ 1 file changed, 4 insertions(+) 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); }