3 ms·
Btw, python-z3 supports the % operator from z3 import Int, solve x = Int('x') solve([x % 611939 == 145767, x % 598463 == 109572]) [x = 243085550] Als
by Recursing 6y ago
Btw, python-z3 supports the % operator
from z3 import Int, solve
x = Int('x')
solve([x % 611939 == 145767, x % 598463 == 109572])
[x = 243085550]
Also: please use python3, it's 2020 :(
And a simpler conversion to base128 would be:
print(''.join(chr((x // 128**i) % 128) for i in range(3, -1, -1)))