Cannot convert model back to bit vector after bit-blasting #7667
Description
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