Investigating issue #50

Current suspicion is that the number of steps reported per prover in the check_tree array denotes a different value than the ones reported in the subsequent stats objects and it seems, the one from the stats object is the proper one to use.

Example (shortened to relevant parts):

"check_tree": [
   {
      "proof_attempts": {
         "Z3": {
            "result": "Valid",
            "steps": 8989120,
            "time": 2.67000000000000E+00
         }
      },
   }
],
"stats": {
   "Z3": {
      "count": 1,
      "max_steps": 10674,
      "max_time": 2.67000007629395E+00
   }
}

As can be seen here, while the time mostly matches (so far I've seen very minor differences which can probably be attributed to different set up times or something), the steps reported in the check_tree array is close to 9 million, while the max_steps from the stats object claims only about 10 thousand steps. The relationship between these two values looks rather linear, so I am suspecting there is some scaling factor involved, probably to have a comparable number of steps independent of the actual prover's reported steps.

Hence, from the looks of it, the stats/<prover_name>/max_steps is the value that should be reported and used for comparisons etc., not the check_tree/proof_attempts/<prover_name>/steps.

Raw number examples

Prover	steps	max_steps
Z3	5 - 407010	1
Z3	602295	191
Z3	705274	320
Z3	8989120	10674
CVC4	72 - 12361	1
CVC4	25745	308
CVC4	78886	1826
CVC4	179947	4713
CVC4	196625	5190
CVC4	206823	5481
CVC4	910628	25590
CVC4	1240724	35021
CVC4	1259723	35564
CVC4	1380321	39010
CVC4	1410144	39862
CVC4	1724694	48849
CVC4	3321417	94470
CVC4	3483618	99104