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 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.

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.

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