0
votes

Are the numbers returned by (get-info :all-statistics) accumulated across multiple calls to check-sat, and across multiple push-pop scopes? Or are they reset at each check-sat (or at push or pop)?

Phrased differently, if I get statistics at various points during a run of Z3, and if a certain statistics, e.g.quant-instantiations always has the same value, can I then conclude that no quantifier instantiation happened in between getting these statistics?

1

1 Answers

0
votes

I did a quick search and it appears that no obj::reset_statistics() is called between check-sat calls for various objs. There are a few re-initializations happening though, so no guarantee that any of this is precise enough for your purpose.