Dynamic array such as bytes are used to pass calldata. These are the source of a large number of exploits, where the data passed is not properly sanitized, yet fuzzers have a lot of trouble to produce reasonable values for them. In hevm, the current dynamic array make them intractable. Halmos instead, concertizes the size of the dynamic array up to a certain number selected by the user, and that's usually good enough.