Comparing Int with float unexpected results

[Wout4]

comparing an integer decision variable with a floating point number gives wrong results because the float gets converted to an integer

example in python:
x = Int('x')
s = Solver()
s.add(x >= 0.1)
s.add(x < 1)
print(s.check())
#sat but should be unsat
m = s.model()
print(m) #gives x = 0

I believe the issue is located in the function _coerce_exprs at line 1214 in z3.py
Because the rhs is not an expression it is typecast to the type of the lhs, in this case leading to the constraint x >= 0 instead of x >= 0.1