(Z3Py) BitVec type conversion, "sort mismatch" error

Question

I'm trying to connect two 8-bit bytes and one 16-word:

from z3 import *

byte1 = BitVec('byte1', 8)
byte2 = BitVec('byte2', 8)
word = BitVec('word', 16)
s = Solver()
s.add(word==(byte1<<8) | byte2)

But I'm getting error:

WARNING: invalid function application, sort mismatch on argument at position 2
WARNING: (define = (bv 16) (bv 16) Bool) applied to:
word of sort (bv 16)
(bvor (bvshl byte1 bv[8:8]) byte2) of sort (bv 8)
...
z3types.Z3Exception: 'type error'

What is correct way to do this?

Answer 1

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