Skip to content

Investigating issue #50

Vinzent "Jellix" Saranen edited this page Jul 8, 2020 · 8 revisions

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 ones from the stats objects are the proper ones 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 be attributed to different rounding or similar), 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.

It is unclear why there is this difference, but 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.