crypto - 200 - Quite an EC task - fail

from z3 import *


s = Solver()

M = Int('M')
M = 93556643250795678718734474880013829509320385402690660619699653921022012489089

A = Int('A')
A = 66001598144012865876674115570268990806314506711104521036747533612798434904785

B = Int('B')

Px = Int('Px')
Px = 56027910981442853390816693056740903416379421186644480759538594137486160388926

Pxr = Int('Pxr')
Pxrm = (Px ** 3 + A * Px) % M

Py = Int('Py')
Py = 65533262933617146434438829354623658858649726233622196512439589744498050226926

Pym = Int('Pym')
Pym = (Py ** 2) % M

Qx = Int('Qx')
Qx = 61124499720410964164289905006830679547191538609778446060514645905829507254103

Qxr = Int('Qxr')
Qxrm = (Qx ** 3 + A * Qx) % M

Qy = Int('Qy')
Qy = 2595146854028317060979753545310334521407008629091560515441729386088057610440

Qym = Int('Qym')
Qym = (Qy ** 2) % M

print 'Pym:  ', Pym
print 'Pxrm: ', Pxrm
print 'Qym:  ', Qym
print 'Qxrm: ', Qxrm

s.add(Pym == (Pxrm + B) % M)
s.add(Qym == (Qxrm + B) % M)

print s.check()
print s.model()

# Much simpler solution without z3
B = (Py ** 2 - Px ** 3 - Px * A) % M
print B # B = 25255205054024371783896605039267101837972419055969636393425590261926131199030