Z3 incorrect ignore model in solver

Z3_incorrect_ignore_model.py

from z3 import *

inp_length = 2

vec = ''
for i in range(0,inp_length):
    vec += f"inp[{i}] " # inp[0] inp[1]
inp = BitVecs(vec, 8)

solver = Solver()
for i in range(0,2):
  solver.add(inp[i] & 0b111111110 == 0) # Allow only first bit to be one

while solver.check() == z3.sat:
  model = solver.model()
  # solver.add([i != model[i] for i in inp])  # <-- Incorrect
  solver.add(Or(  # <-- Correct
    [inp[i] != model[inp[i]] for i in range(0,inp_length)]
  ))
  print(model)



## Output with correct line uncommented:
##   [inp[1] = 0, inp[0] = 0]
##   [inp[0] = 1, inp[1] = 1]
##   [inp[0] = 1, inp[1] = 0]
##   [inp[0] = 0, inp[1] = 1]

## Output with incorrect line uncommented:
##   [inp[1] = 0, inp[0] = 0]
##   [inp[0] = 1, inp[1] = 1]

See also: https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models