Replaces the per-byte `store(store(...))` chain in modelMemcpyLikeCall
with a single `z3::lambda(i, ite(in_range, src_byte, orig_byte))`.
Drops the `!arg_values[2].is_numeral()` bail so symbolic copy_bytes
now reaches the solver instead of being silently skipped.
Concrete cap (kMaxModeledCopyBytes=4096) is kept to prevent
pathological bit-blast explosion on giant memcpy()s. strcpy is
unchanged -- literal bytes are short + concrete and the lambda
form doesn't help there.
z3 simplifies the lambda away at concrete-index selects so QF_BV
stays viable; no logic-change cascade. Full unit suite stays
57/57 green.
