Apologies if I'm posing this question in the wrong place -- please let me know if there is a better place to ask.

We're using the theory of bitvectors. We're trying to extract a slice/subvector of a vector b, where the length l of the slice is constant but the offset o may be symbolic. In Python notation:

b[o:o+l]

If o is a constant, using the Python API, we can use Extract and do z3.Extract(o + l - 1, o, b).
If o is symbolic, Extract will throw an error because it disallows symbolic indices, but we figured out the following workaround using RotateRight, which does allow symbolic rotation:

z3.Extract(l - 1, 0, z3.RotateRight(b, o))

However, empirically we're observing poor performance using this encoding when o is indeed symbolic.

I am wondering if this is expected and if there are any known approaches to address this issue, e.g. more clever encodings?
I am also curious how RotateRight works in the first place when the rotation is symbolic...does this just translate down to a # bit-wise case split or something more clever?

cc @qobilidop @jonathan-dilorenzo @kheradmandG