z3py time not in solver.statistics()

[Skynet0]

I'd like to be able to access the time to solve, but can't seem to figure out how to get it from the solver:

from z3 import *
x = Int('x')
y = Int('y')
s.add(x > 10, y == x + 2)
s.check()
print(s.statistics())

outputs

(:eliminated-applications 4
 :eliminated-vars         4
 :max-memory              3.35
 :memory                  3.05
 :mk-bool-var             9
 :num-allocs              2145234
 :rlimit-count            250)

which doesn't include the time. The time is present in the verbose logs.

Yes, I could use time, but I'd like to see if there's a way to get the internal time.

[wintersteiger]

If I remember correctly, the statistics output suppresses all zeros, i.e. if it's not there, it's 0.

[Skynet0]

It's not that; I can solve a problem that takes nonzero time to solve, and time isn't present in the statistics

I don't have a short example unfortunately, but e.g. most of the examples from https://github.com/obijywk/grilops will take a while. Running the Fillomino example definitely takes several seconds real-time, but the statistics output is:

(:added-eqs                 3469923
 :arith-assert-diseq        1392077
 :arith-assert-lower        2237930
 :arith-assert-upper        1837081
 :arith-assume-eqs          1
 :arith-bound-prop          43731
 :arith-conflicts           19362
 :arith-eq-adapter          12475
 :arith-fixed-eqs           437175
 :arith-num-rows            1195
 :arith-offset-eqs          653220
 :arith-pivots              223953
 :arith-row-summations      2156199
 :arith-tableau-max-columns 2503
 :arith-tableau-max-rows    1195
 :binary-propagations       7496610
 :conflicts                 59582
 :decisions                 131817
 :del-clause                61439
 :eliminated-vars           151
 :final-checks              2
 :interface-eqs             1
 :max-memory                17.14
 :memory                    6.30
 :minimized-lits            272170
 :mk-bool-var               22815
 :mk-clause                 84975
 :num-allocs                86747651
 :num-checks                2
 :propagations              10835537
 :restarts                  329
 :rlimit-count              164700996)

[rainoftime]

It seems that z3 does not record the time if a timeout is not set?

[Skynet0]

I've also set a timeout using solver.set(timeout=timeout), which still hasn't added the time to the statistics. (It does timeout properly though.)

[Skynet0]

Thanks!