error bitvecs not defined

[Zibri]

$ python3 xs128p.py
BROWSER: chrome
[0.49965622623126693, 0.5106241305628436, 0.7895949638905317, 0.883588766746984, 0.5368584449767335]
Traceback (most recent call last):
  File "xs128p.py", line 207, in <module>
    main()
  File "xs128p.py", line 167, in main
    ostate0, ostate1 = BitVecs('ostate0 ostate1', 64)
NameError: name 'BitVecs' is not defined

[Xavier59]

pip install z3-solver