from z3 import * key = BitVec('key', 64) solve((key * key * key * key * key * key * key) == 0x90de757572b51cd3)
[key = 16721472531635646971] 0xE80E9AAC619831FB