mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

map and fold cannot be treated as variables

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-10 16:03:24 -07:00
parent 4a652a4c0c
commit 8311525472
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_eq_solver.cpp
View file

@ -438,6 +438,10 @@ namespace seq {
!seq.str.is_unit(a) && !seq.str.is_unit(a) &&
!seq.str.is_itos(a) && !seq.str.is_itos(a) &&
!seq.str.is_nth_i(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); !m.is_ite(a);
} }