Traceback (most recent call last):
  File "z3_messing_around.py", line 6, in <module>
    map_to_index = z3.SeqMapI(
                   ^^^^^^^^^^^
  File ".venv/lib/python3.12/site-packages/z3/z3.py", line 11344, in SeqMapI
    ctx = _get_ctx(f, s)
          ^^^^^^^^^^^^^^
TypeError: _get_ctx() takes 1 positional argument but 2 were given

import z3

nums = z3.Const('nums', z3.SeqSort(z3.IntSort()))
mapped_nums = z3.Const('mapped_nums', nums.sort())

index, value = z3.Ints("index value")
map_to_index = z3.SeqMapI(
    z3.Lambda([index, value], index),
    z3.IntVal(0),
    nums,
)
s = z3.Solver()

s.add(z3.Length(nums) == 3)
s.add(map_to_index == mapped_nums)

print(s.sexpr())
print("SAT: ", s.check())
print(s.model())