AttributeError Z3 'Solver'

[chapeyfor]

Hi there.

First of all thanks for all your work, it really helps me, and I am sure lots of people :-).

I am opening an issue ticket regarding an AttributeError following the use of raid_solver.py.

I have installed Python on my computer, then in Windows cmd, launched the following:
1/ py -m pip install z3
2/ py raid.py

Then I have entered the value of the Pokemon find in den, value as follow: (first Pokemon of the rare den 69, Linoone)

• EC: 0x12d60415
• PID: 0x134071ce
• IVs(x.x.x.x.x.x): 27.14.28.31.29.31

As a result, I have the following:
Traceback (most recent call last):
File "raid.py.py", line 179, in
if main() == False:
File "raid.py.py", line 174, in main
return searchInput()
File "raid.py.py", line 170, in searchInput
return search(ec, pid, ivs)
File "raid.py.py", line 137, in search
seeds = find_seeds(ec, pid)
File "raid.py.py", line 89, in find_seeds
solver = z3.Solver()
AttributeError: module 'z3' has no attribute 'Solver'

Did I, or am I doing something wrong there?

Please note that this is the first time for me to use Python, as such I'm not familiar with the tool. If I did something wrong, could you please tell me step by step what I have to do?

Thanks in advance for your support.

[Admiral-Fish]

The package name to install with pip is z3-solver, not z3.