How to get statistics in Z3 3.2?

Question

With Z3 2.x I used the SMTLib2 command

(get-info statistics)

to get statistics of a Z3 run. Using Z3 3.2 I get

(error "line _ column _: invalid command argument, keyword expected")

for the above, and to

(get-info :statistics)

Z3 replies with

unsupported

What's the new way of getting statistics (other than the /st command-line option)?

And while we're at it: The INI options page lists

(set-option :STATISTICS true)

as a valid option, but Z3 3.2 again replies with

unsupported

pad · Accepted Answer · 2012-01-09T10:07:58.587

2

(get-info :all-statistics)

should do the trick.

edited Jan 09 '12 at 10:07

answered Jan 09 '12 at 10:01

pad

It indeed does, thanks! Is it mentioned somewhere in the docs? – Malte Schwerhoff Jan 09 '12 at 10:06
I saw it when browsing through Z3's examples at http://rise4fun.com/samples (see my update). – pad Jan 09 '12 at 10:09
Is there maybe even a way of getting a specific statistic, e.g. "conflicts" or "quant-instantiations"? – Malte Schwerhoff Jan 09 '12 at 10:13
I don't think so. Z3 team wants to keep the core as small as possible. – pad Jan 09 '12 at 10:18

1 Answers1