How do I convert the key to bytes and pass it to sha256 before checking for satisfiability.
Note the script is a bigger than this but my problem is here:
from hashlib import sha256
from z3 import *
key = BitVec('k', 8)
# key = [BitVec(f'key_{i}', 8) for i in range(6)]
h = sha256(key).digest()
print(h.hex())
I don't want to check for satisfiability first because the constraints has to presented in the key generation.
You can't. sha256 as implemented by hashlib is not an algorithm that can work on symbolic key values. If you want it to work on symbolic values, you'll have to write your own version that knows how to deal with z3's symbolic values.
Depending on the algorithm you're coding, this might be a fairly difficult task. To get a feel of how to program with symbolic values, you can start by reading through https://theory.stanford.edu/~nikolaj/programmingz3.html
I should add that if your goal is to find the "input" that produces a certain concrete output value, then you'll be disappointed. No SMT solver can "reverse-engineer" an algorithm like SHA256, an algorithm designed for being a one-way function. (You can solve it if your input is really really small; essentially by enumerating; but for any reasonable input size, the problem is practically intractable.)