In the z3 tutorial, str.indexof and seq.indexof are mentioned separately. However, in the Z3 C API, there is only one relevant function, Z3_mk_seq_index. Does that function do special-case handling for the case of sequences of 8-bit BitVecs? Meaning, if my sequences are all strings, will Z3_mk_seq_index still use the z3str3 codebase? Or will it fall back on z3's sequence solver?
There's no difference between a sequence of 8-bit values and a string in z3. In fact, all strings are treated as sequences of 8-bit values.
The only difference between seq.indexof and str.indexof is their type. The latter is simply a specialization of the former.
To switch between the regular string solver and z3str3, simply use the appropriate command line switch smt.string_solver. Valid options are seq, z3str3, and auto.