Cannot convert model back to bit vector after bit-blasting

[JoshuaB47]

Here's a (fairly minimal) example in Python with Z3 version: 4.15.0:

from z3 import *
pre_processor = Tactic("bit-blast")
solver = Solver()

x = BitVec('x', 8)
pre_processed = pre_processor(x == 5)
solver.add(pre_processed[0]) # add the sole assertion

if solver.check() == sat:
    print(solver.model())
    model = pre_processed[0].convert_model(solver.model())
    print(model)
    print(model[x].as_long())

Which outputs:

[]
[x = 0]
0

I would instead expect it to output:

some representation of 5 in binary
[x = 5]
5

[NikolajBjorner]

This works as I expect: pre-processing introduces internal Boolean variables. They will not show up in models.