stp.RotateLeft

stp.RotateLeft(a, b)

z3py order: the term first; an int amount is the indexed kind, a term amount is taken modulo the size, as an int amount is: (a << r) | LShR(a, size - r) with r = URem(b, size).