z3py time not in Optimize.statistics()

[diegochine]

Looks like z3py saves time in statistics only for Solver objects and not for Optimize ones.
Using Solver:

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 10, y == x + 2)
s.set("timeout", 1000) # not actually needed to have time in statistics
s.check()
print(s.statistics())

outputs

(:eliminated-applications 2
 :eliminated-vars         2
 :max-memory              18.93
 :memory                  18.93
 :num-allocs              8649163
 :rlimit-count            536
 :time                    0.00)

which includes time, but for Optimize the same code

x = Int('x')
y = Int('y')
s = Optimize()
s.set("timeout", 1000)
s.add(x > 10, y == x + 2)
s.minimize(x)
print(s.statistics())

outputs

(:max-memory   18.93
 :memory       16.72
 :num-allocs   11346270
 :rlimit-count 536)

This issue looks very similar to issue #4662. Is there any way to get the internal time when using the Optimize class?

[NikolajBjorner]

you also need to call s.check()

[diegochine]

Thank you!