Optimizer returns empty model for unsatisfiable constraints

[humnrdble]

If the difference between Solver and Optimize is intended, please add documentation for this.

from z3 import *
s = Optimize()
x = Bool("x")
s.add(x)
s.add(Not(x))
s.check() #unsat
s.model()

Output:

[]

Solver:

from z3 import *
s = Solver()
x = Bool("x")
s.add(x)
s.add(Not(x))
s.check() #unsat
s.model()

Output:

Z3Exception: model is not available

z3py Versions 4.14.1.0, 4.15.4.0

[humnrdble]

Or even simpler:

s = Optimize()
s.model()

Output:

[]