Print stats about solver performance costs that don't vary by run, such as backjump count.

[grayjay]

See #4562 (comment).

[grayjay]

One option is to print the total number of nodes that the solver explores. I think that would correlate more closely with run time than the backjump count, because the solver can traverse any number of levels during one backjump.

[hvr]

The backjump count is still interesting though, as that value corresponds to a parameter the user can configure. Currently, we have no good way to figure out which backjump limit to set manually (without having to use an infinite upper limit), when the default one doesn't suffice to find a solution.