Factor code a bit between known and unknown prover versions.

In particular, unknown versions are now also recorded for use in automatic strategies.

This fixes part of issue #667 (closed).