You need to use sign or zero extension to fix the type error by changing the number of bits in the expression. Documentation for each is respectively:
http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-SignExt
http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-ZeroExt
For example (rise4fun link: http://rise4fun.com/Z3Py/872 ):
byte1 = BitVec('byte1', 8)
byte2 = BitVec('byte2', 8)
word = BitVec('word', 16)
s = Solver()
Pz = word == (ZeroExt(8, byte1) <<8) | (ZeroExt(8, byte2))
Ps = word == (SignExt(8, byte1) <<8) | (SignExt(8, byte2))
print Pz
print Ps
s.add(Pz)
s.add(Ps)
s.add(word == 0xffff)
print s
print s.check()
print s.model() # word is 65535, each byte is 255