Compilation across the CI run
28 stage records · 7 measured workloads · 18 CI jobs
Commit 70bf5bdd156aedf31952f441e1ce51a8af9c5330 · Run 43763876593 · Generated 2026-11-15T22:25:22.530Z
These are static compilation events, not runtime execution frequencies. Proof queries can revisit the same fact. Planned substitutions and emitted substitutions are separate. Byte counters describe pass input/output, not marginal savings attributable to one rule.
Absent records are missing coverage, not zero usage. Cached builds are excluded from current-run totals; failed stages may contribute partial counters. Collection covers instrumented compiler passes in native application builds and self-compilation; host/browser test status does not imply every test compilation was measured.
Use counts alongside application size and performance measurements. An uncommon rule may still be valuable for typed code or a particular application.
CI jobs
| Job | Result | Duration |
|---|---|---|
| Build shared runtime and standalone pages | success | 406 s |
| Host compilation / sbcl-bin / ubuntu-latest | success | 55 s |
| Host compilation / sbcl-bin / macos-latest | success | 72 s |
| Host compilation / ccl-bin/1.13 / ubuntu-latest | success | 74 s |
| Host compilation / ecl/26.5.5 / ubuntu-latest | success | 327 s |
| Host compilation / sbcl-bin / windows-latest | success | 156 s |
| Application / acl2 | success | 2,492 s |
| ANSI / interpreter | success | 556 s |
| Core checks beyond ANSI | success | 20 s |
| ANSI / compiler | success | 570 s |
| Application / fricas | success | 2,412 s |
| Application / mcclim | success | 1,064 s |
| Application / game-of-life | success | 649 s |
| Application / maxima | success | 1,133 s |
| Application / coalton | success | 1,862 s |
| Collect ANSI reports | success | 6 s |
| Assemble browser examples and size report | success | 456 s |
| Collect compiler and prover report | success | 15 s |
Compilation stages and raw sizes
| Workload / stage | Coverage | Time | Runtime bytes | Input bytes | Output bytes | CI job |
|---|---|---|---|---|---|---|
| acl2compact dynamic environment | Collected | 13,671 mscollection enabled | — | — | — | application-acl2 |
| acl2compile native code | Collected | 890,902 mscollection enabled | — | — | — | application-acl2 |
| acl2loader | Collected | 3,031 mscollection enabled | — | — | — | application-acl2 |
| acl2native output | Measurement | — | 1,000,584 | 30,776,013 | 18,157,407 | application-acl2 |
| coaltoncompiler: compaction | Collected | 5,479 mscollection enabled | — | — | — | application-coalton |
| coaltoncompiler: load compacted compiler | Collected | 5,923 mscollection enabled | — | — | — | application-coalton |
| coaltoncompiler: native bundle | Collected | 251,037 mscollection enabled | — | — | — | application-coalton |
| coaltoncompiler: native output | Measurement | — | 1,000,584 | 7,706,538 | 3,404,626 | application-coalton |
| coaltoncompiler: release portable input | Collected | 5 mscollection enabled | — | — | — | application-coalton |
| coaltonfull: compaction | Collected | 17,746 mscollection enabled | — | — | — | application-coalton |
| coaltonfull: load bootstrap | Collected | 3,102 mscollection enabled | — | — | — | application-coalton |
| coaltonfull: native bundle | Collected | 620,070 mscollection enabled | — | — | — | application-coalton |
| coaltonfull: native output | Measurement | — | 1,000,584 | 23,574,801 | 10,406,359 | application-coalton |
| coaltonfull: release portable input | Collected | 4 mscollection enabled | — | — | — | application-coalton |
| compiler-bootstrapbootstrap native functions | Collected | 159,553 mscollection enabled | — | — | — | runtime |
| compiler-bootstrapsealed compiler module | Collected | 27,790 mscollection enabled | — | — | — | runtime |
| fricascompact portable input | Collected | 9,042 mscollection enabled | — | — | — | application-fricas |
| fricascompile native code | Collected | 266,994 mscollection enabled | — | — | — | application-fricas |
| fricasload build environment | Collected | 4,769 mscollection enabled | — | — | — | application-fricas |
| fricasnative output | Measurement | — | 1,000,584 | 9,923,717 | 3,860,756 | application-fricas |
| game-of-lifeapplication output | Measurement | — | 988,874 | — | 2,423,530 | application-game-of-life |
| game-of-lifemiricl-compiler:optimize-system | partial: partial or missing coverageCounter collection: Unhandled condition. | 437,201 mscollection enabled | — | — | — | application-game-of-life |
| maximacompact portable input | Collected | 20,974 mscollection enabled | — | — | — | application-maxima |
| maximacompile native code | Collected | 584,462 mscollection enabled | — | — | — | application-maxima |
| maximaload build environment | Collected | 13,275 mscollection enabled | — | — | — | application-maxima |
| maximanative output | Measurement | — | 1,000,584 | 22,318,657 | 8,303,752 | application-maxima |
| mcclimnative bundle | Collected | 615,397 mscollection enabled | — | — | — | application-mcclim |
| mcclimnative output | Measurement | — | 1,000,584 | 15,925,869 | 6,215,376 | application-mcclim |
| Rule / detail | Observed total | acl2 | coalton | compiler-bootstrap | fricas | game-of-lifepartial / cached | maxima | mcclim |
|---|---|---|---|---|---|---|---|---|
| inference/declared-argumentall | 80 | 0 | 0 | 80 | 0 | — | 0 | 0 |
| lowering/function-controldispatcher | 326 | 11 | 45 | 10 | 0 | — | 58 | 202 |
| lowering/function-controlforward | 278,920 | 65,333 | 82,648 | 695 | 19,948 | — | 38,981 | 71,315 |
| lowering/function-controlstructured | 8,676 | 1,221 | 1,363 | 488 | 2,158 | — | 1,730 | 1,716 |
| lowering/ordinary-call0 | 6,802 | 1,122 | 1,325 | 162 | 1,715 | — | 886 | 1,592 |
| lowering/ordinary-call1 | 415,548 | 109,317 | 112,280 | 6,363 | 31,967 | — | 73,454 | 82,167 |
| lowering/ordinary-call2 | 601,390 | 248,377 | 99,807 | 5,220 | 34,383 | — | 106,663 | 106,940 |
| lowering/ordinary-call3 | 75,563 | 34,154 | 6,365 | 1,470 | 4,281 | — | 8,919 | 20,374 |
| lowering/ordinary-call4 | 32,279 | 9,666 | 4,020 | 408 | 1,347 | — | 3,054 | 13,784 |
| lowering/wasm-input-bytesall · bytes | 133,820,179 | 43,375,183 | 35,251,893 | 1,289,715 | 9,458,851 | — | 19,439,076 | 25,005,461 |
| lowering/wasm-output-bytesall · bytes | 90,857,705 | 29,012,434 | 23,207,784 | 873,530 | 6,314,042 | — | 12,990,582 | 18,459,333 |
| optimization/cell-foldingall | 87,825 | 12,894 | 15,186 | 1,098 | 11,929 | — | 20,396 | 26,322 |
| optimization/generic-dispatch0 | 682 | 0 | 532 | 0 | 0 | — | 0 | 150 |
| optimization/generic-dispatch1 | 2 | 0 | 1 | 0 | 0 | — | 1 | 0 |
| optimization/generic-dispatch12 | 4 | 0 | 4 | 0 | 0 | — | 0 | 0 |
| optimization/generic-dispatch2 | 60 | 0 | 57 | 0 | 0 | — | 0 | 3 |
| optimization/generic-dispatch3 | 7 | 0 | 2 | 0 | 0 | — | 4 | 1 |
| optimization/generic-dispatch4 | 11 | 0 | 10 | 0 | 0 | — | 0 | 1 |
| optimization/generic-dispatch6 | 3 | 0 | 0 | 0 | 0 | — | 3 | 0 |
| optimization/hir-constantall | 1,661 | 76 | 4 | 1,424 | 2 | — | 155 | 0 |
| optimization/hir-constant-branchall | 635 | 104 | 8 | 453 | 0 | — | 70 | 0 |
| optimization/hir-copycell-read | 39,395 | 1,765 | 2,653 | 33,151 | 56 | — | 548 | 1,222 |
| optimization/hir-copycell-write | 1,746 | 30 | 12 | 1,700 | 2 | — | 2 | 0 |
| optimization/immediate-integer-boxall | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-primitive124 | 143 | 0 | 0 | 143 | 0 | — | 0 | 0 |
| optimization/inline-primitive125 | 111 | 0 | 0 | 111 | 0 | — | 0 | 0 |
| optimization/inline-primitive126 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitive131 | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| optimization/inline-primitive132 | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| optimization/inline-primitive133 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| optimization/inline-primitive134 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-primitive135 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitive80 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitive81 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitive82 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-primitive83 | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| optimization/inline-primitive85 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-primitive87 | 6 | 0 | 0 | 6 | 0 | — | 0 | 0 |
| optimization/inline-primitive89 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitiveash-general | 66 | 0 | 0 | 66 | 0 | — | 0 | 0 |
| optimization/inline-primitivecar | 65 | 0 | 0 | 65 | 0 | — | 0 | 0 |
| optimization/inline-primitivecar-cons | 1,294 | 0 | 0 | 1,294 | 0 | — | 0 | 0 |
| optimization/inline-primitivecdr | 323 | 0 | 0 | 323 | 0 | — | 0 | 0 |
| optimization/inline-primitivecdr-cons | 664 | 0 | 0 | 664 | 0 | — | 0 | 0 |
| optimization/inline-primitivechecked-car | 2,185 | 0 | 0 | 2,185 | 0 | — | 0 | 0 |
| optimization/inline-primitivechecked-cdr | 1,575 | 0 | 0 | 1,575 | 0 | — | 0 | 0 |
| optimization/inline-primitivecode-character | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| optimization/inline-primitivecons | 944 | 0 | 0 | 944 | 0 | — | 0 | 0 |
| optimization/inline-primitiveconsp | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-primitiveeq | 692 | 0 | 0 | 692 | 0 | — | 0 | 0 |
| optimization/inline-primitiveeql | 70 | 0 | 0 | 70 | 0 | — | 0 | 0 |
| optimization/inline-primitivegethash | 694 | 0 | 0 | 694 | 0 | — | 0 | 0 |
| optimization/inline-primitivegreater-real | 94 | 0 | 0 | 94 | 0 | — | 0 | 0 |
| optimization/inline-primitiveinteger-length | 18 | 0 | 0 | 18 | 0 | — | 0 | 0 |
| optimization/inline-primitivelength | 709 | 0 | 2 | 703 | 0 | — | 0 | 4 |
| optimization/inline-primitiveless-real | 286 | 0 | 0 | 286 | 0 | — | 0 | 0 |
| optimization/inline-primitivelist | 1,142 | 0 | 0 | 1,142 | 0 | — | 0 | 0 |
| optimization/inline-primitivelogand-general | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| optimization/inline-primitivenot-greater-real | 142 | 0 | 0 | 142 | 0 | — | 0 | 0 |
| optimization/inline-primitivenot-less-real | 308 | 0 | 0 | 308 | 0 | — | 0 | 0 |
| optimization/inline-primitivenull | 418 | 0 | 0 | 418 | 0 | — | 0 | 0 |
| optimization/inline-primitiveputhash | 298 | 0 | 0 | 298 | 0 | — | 0 | 0 |
| optimization/inline-primitiverow-major-ref | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-primitiverow-major-set | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| optimization/inline-primitivesimple-vector-p | 250 | 0 | 0 | 250 | 0 | — | 0 | 0 |
| optimization/inline-primitivevector-length | 227 | 0 | 0 | 227 | 0 | — | 0 | 0 |
| optimization/inline-primitivezero-number | 112 | 0 | 0 | 112 | 0 | — | 0 | 0 |
| optimization/inline-shiftleft | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/inline-shiftright | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/inline-vectorread | 4,127 | 0 | 0 | 4,127 | 0 | — | 0 | 0 |
| optimization/inline-vectorwrite | 434 | 0 | 0 | 434 | 0 | — | 0 | 0 |
| optimization/literal-function-fusionall | 1,694,465 | 637,864 | 363,954 | 12,690 | 106,656 | — | 254,619 | 318,682 |
| optimization/local-copy-backall | 1,806 | 1,026 | 218 | 44 | 71 | — | 153 | 294 |
| optimization/local-copy-fold32 | 18,281 | 2,392 | 1,700 | 309 | 6,961 | — | 4,870 | 2,049 |
| optimization/local-copy-fold33 | 498,680 | 172,516 | 139,174 | 4,287 | 46,431 | — | 69,908 | 66,364 |
| optimization/local-self-teeall | 15,715 | 10,340 | 677 | 579 | 799 | — | 1,790 | 1,530 |
| optimization/local-slots-removedall | 2,955,190 | 925,704 | 700,535 | 22,734 | 260,385 | — | 421,659 | 624,173 |
| optimization/loop-hoistcapture | 16,695 | 189 | 328 | 947 | 13,442 | — | 769 | 1,020 |
| optimization/loop-hoisteq | 34 | 0 | 0 | 34 | 0 | — | 0 | 0 |
| optimization/loop-hoistnull | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| optimization/proven-condition0 | 948 | 719 | 0 | 225 | 0 | — | 0 | 4 |
| optimization/proven-condition1 | 833 | 0 | 269 | 0 | 288 | — | 170 | 106 |
| optimization/proven-condition3 | 14 | 0 | 2 | 12 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch80 | 44 | 0 | 0 | 44 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch81 | 208 | 0 | 0 | 208 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch82 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch83 | 30 | 0 | 0 | 30 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch85 | 30 | 0 | 0 | 30 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch87 | 10 | 0 | 0 | 10 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branch89 | 184 | 0 | 0 | 184 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branchconsp | 338 | 0 | 0 | 338 | 0 | — | 0 | 0 |
| optimization/raw-predicate-brancheq | 3,350 | 0 | 0 | 3,350 | 0 | — | 0 | 0 |
| optimization/raw-predicate-brancheql | 544 | 0 | 0 | 544 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branchevenp | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/raw-predicate-branchnull | 490 | 0 | 0 | 490 | 0 | — | 0 | 0 |
| optimization/removed-importsall | 7,739,558 | 2,486,157 | 3,101,953 | 36,401 | 14,485 | — | 90,920 | 2,009,642 |
| optimization/shared-bodyall | 1,053,925 | 211,946 | 334,645 | 74 | 96,290 | — | 211,072 | 199,898 |
| optimization/single-value-joinall | 95,329 | 19,818 | 15,704 | 8,857 | 19,558 | — | 15,154 | 16,238 |
| optimization/unboxed-argument-initializeall | 6 | 0 | 0 | 6 | 0 | — | 0 | 0 |
| optimization/unboxed-argument-readall | 44 | 0 | 0 | 44 | 0 | — | 0 | 0 |
| optimization/unboxed-cellcell-new | 26 | 0 | 0 | 26 | 0 | — | 0 | 0 |
| optimization/unboxed-cellcell-read | 68 | 0 | 0 | 68 | 0 | — | 0 | 0 |
| optimization/unboxed-cellcell-write | 44 | 0 | 0 | 44 | 0 | — | 0 | 0 |
| optimization/unboxed-result124 | 143 | 0 | 0 | 143 | 0 | — | 0 | 0 |
| optimization/unboxed-result125 | 111 | 0 | 0 | 111 | 0 | — | 0 | 0 |
| optimization/unboxed-result126 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/unboxed-result131 | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| optimization/unboxed-result132 | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| optimization/unboxed-result133 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| optimization/unboxed-result134 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| optimization/unboxed-result135 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| optimization/unboxed-result-boxall | 282 | 0 | 0 | 282 | 0 | — | 0 | 0 |
| optimization/unboxed-result-readall | 194 | 0 | 0 | 194 | 0 | — | 0 | 0 |
| planning/inline-primitive124 | 143 | 0 | 0 | 143 | 0 | — | 0 | 0 |
| planning/inline-primitive125 | 111 | 0 | 0 | 111 | 0 | — | 0 | 0 |
| planning/inline-primitive126 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| planning/inline-primitive131 | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| planning/inline-primitive132 | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| planning/inline-primitive133 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/inline-primitive134 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| planning/inline-primitive135 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| planning/inline-primitive80 | 52 | 0 | 0 | 52 | 0 | — | 0 | 0 |
| planning/inline-primitive81 | 216 | 0 | 0 | 216 | 0 | — | 0 | 0 |
| planning/inline-primitive82 | 6 | 0 | 0 | 6 | 0 | — | 0 | 0 |
| planning/inline-primitive83 | 44 | 0 | 0 | 44 | 0 | — | 0 | 0 |
| planning/inline-primitive85 | 34 | 0 | 0 | 34 | 0 | — | 0 | 0 |
| planning/inline-primitive87 | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| planning/inline-primitive89 | 192 | 0 | 0 | 192 | 0 | — | 0 | 0 |
| planning/inline-primitiveash-general | 66 | 0 | 0 | 66 | 0 | — | 0 | 0 |
| planning/inline-primitivecar | 73 | 0 | 0 | 73 | 0 | — | 0 | 0 |
| planning/inline-primitivecar-cons | 1,298 | 0 | 0 | 1,298 | 0 | — | 0 | 0 |
| planning/inline-primitivecdr | 323 | 0 | 0 | 323 | 0 | — | 0 | 0 |
| planning/inline-primitivecdr-cons | 664 | 0 | 0 | 664 | 0 | — | 0 | 0 |
| planning/inline-primitivechecked-car | 2,185 | 0 | 0 | 2,185 | 0 | — | 0 | 0 |
| planning/inline-primitivechecked-cdr | 1,575 | 0 | 0 | 1,575 | 0 | — | 0 | 0 |
| planning/inline-primitivecode-character | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/inline-primitivecons | 944 | 0 | 0 | 944 | 0 | — | 0 | 0 |
| planning/inline-primitiveconsp | 346 | 0 | 0 | 346 | 0 | — | 0 | 0 |
| planning/inline-primitiveeq | 4,042 | 0 | 0 | 4,042 | 0 | — | 0 | 0 |
| planning/inline-primitiveeql | 614 | 0 | 0 | 614 | 0 | — | 0 | 0 |
| planning/inline-primitiveevenp | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| planning/inline-primitivegethash | 694 | 0 | 0 | 694 | 0 | — | 0 | 0 |
| planning/inline-primitivegreater-real | 94 | 0 | 0 | 94 | 0 | — | 0 | 0 |
| planning/inline-primitiveinteger-length | 18 | 0 | 0 | 18 | 0 | — | 0 | 0 |
| planning/inline-primitivelength | 709 | 0 | 2 | 703 | 0 | — | 0 | 4 |
| planning/inline-primitiveless-real | 286 | 0 | 0 | 286 | 0 | — | 0 | 0 |
| planning/inline-primitivelist | 1,142 | 0 | 0 | 1,142 | 0 | — | 0 | 0 |
| planning/inline-primitivelogand-general | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| planning/inline-primitivenot-greater-real | 142 | 0 | 0 | 142 | 0 | — | 0 | 0 |
| planning/inline-primitivenot-less-real | 308 | 0 | 0 | 308 | 0 | — | 0 | 0 |
| planning/inline-primitivenull | 916 | 0 | 0 | 916 | 0 | — | 0 | 0 |
| planning/inline-primitiveputhash | 298 | 0 | 0 | 298 | 0 | — | 0 | 0 |
| planning/inline-primitiverow-major-ref | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| planning/inline-primitiverow-major-set | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/inline-primitivesimple-vector-p | 250 | 0 | 0 | 250 | 0 | — | 0 | 0 |
| planning/inline-primitivetrue | 20 | 0 | 0 | 20 | 0 | — | 0 | 0 |
| planning/inline-primitivevector-length | 227 | 0 | 0 | 227 | 0 | — | 0 | 0 |
| planning/inline-primitivezero-number | 112 | 0 | 0 | 112 | 0 | — | 0 | 0 |
| planning/inline-vectoraref | 132 | 0 | 0 | 132 | 0 | — | 0 | 0 |
| planning/inline-vectorsvref | 4,429 | 0 | 0 | 4,429 | 0 | — | 0 | 0 |
| planning/unboxed-argument33 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| planning/unboxed-argument9 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-cell13 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-cell32 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-cell33 | 6 | 0 | 0 | 6 | 0 | — | 0 | 0 |
| planning/unboxed-cell34 | 12 | 0 | 0 | 12 | 0 | — | 0 | 0 |
| planning/unboxed-cell4 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-cell64 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-result124 | 143 | 0 | 0 | 143 | 0 | — | 0 | 0 |
| planning/unboxed-result125 | 111 | 0 | 0 | 111 | 0 | — | 0 | 0 |
| planning/unboxed-result126 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| planning/unboxed-result131 | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| planning/unboxed-result132 | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| planning/unboxed-result133 | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| planning/unboxed-result134 | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| planning/unboxed-result135 | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| proof/branch-premiseall | 115 | 66 | 12 | 0 | 9 | — | 8 | 20 |
| proof/branch-premisecons | 588 | 0 | 0 | 588 | 0 | — | 0 | 0 |
| proof/branch-premiseplusp | 34 | 0 | 0 | 34 | 0 | — | 0 | 0 |
| proof/branch-premisesimple-vector | 506 | 0 | 0 | 506 | 0 | — | 0 | 0 |
| proof/branch-premiset | 67,551 | 23,971 | 8,049 | 4,584 | 4,621 | — | 11,102 | 15,224 |
| proof/branch-premisezerop | 32 | 0 | 0 | 32 | 0 | — | 0 | 0 |
| proof/branch-reachabilityall | 41 | 8 | 2 | 0 | 15 | — | 16 | 0 |
| proof/branch-reachabilityt | 1,625 | 699 | 244 | 237 | 272 | — | 131 | 42 |
| proof/branch-write-barrierall | 4,354 | 263 | 1,750 | 842 | 11 | — | 660 | 828 |
| proof/integer-branch-refinementplusp | 22 | 0 | 0 | 22 | 0 | — | 0 | 0 |
| proof/integer-branch-refinementzerop | 12 | 0 | 0 | 12 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown/= | 18 | 0 | 0 | 18 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown< | 324 | 0 | 0 | 324 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown<= | 160 | 0 | 0 | 160 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown= | 630 | 0 | 0 | 630 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown> | 108 | 0 | 0 | 108 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknown>= | 504 | 0 | 0 | 504 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknowneq | 1,645 | 0 | 0 | 1,645 | 0 | — | 0 | 0 |
| proof/integer-comparison-unknowneql | 3,184 | 0 | 0 | 3,184 | 0 | — | 0 | 0 |
| proof/integer-complement-rangeall | 2 | 0 | 0 | 2 | 0 | — | 0 | 0 |
| proof/integer-identity-known- | 15 | 0 | 0 | 1 | 14 | — | 0 | 0 |
| proof/integer-identity-known+ | 1,669 | 0 | 0 | 306 | 0 | — | 1,363 | 0 |
| proof/integer-identity-knownash | 7 | 0 | 0 | 7 | 0 | — | 0 | 0 |
| proof/integer-identity-knownlogior | 10 | 0 | 0 | 10 | 0 | — | 0 | 0 |
| proof/integer-identity-unknown- | 2,153 | 4 | 4 | 701 | 10 | — | 1,430 | 4 |
| proof/integer-identity-unknown* | 107 | 14 | 4 | 64 | 0 | — | 25 | 0 |
| proof/integer-identity-unknown+ | 3,646 | 66 | 4 | 2,679 | 15 | — | 810 | 72 |
| proof/integer-identity-unknownash | 187 | 0 | 0 | 187 | 0 | — | 0 | 0 |
| proof/integer-identity-unknownlogand | 68 | 0 | 0 | 68 | 0 | — | 0 | 0 |
| proof/integer-identity-unknownlogior | 142 | 0 | 0 | 142 | 0 | — | 0 | 0 |
| proof/integer-identity-unknownlogxor | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| proof/integer-predicate-trueplusp | 36 | 0 | 0 | 36 | 0 | — | 0 | 0 |
| proof/integer-predicate-unknownevenp | 12 | 0 | 0 | 12 | 0 | — | 0 | 0 |
| proof/integer-predicate-unknownminusp | 94 | 0 | 0 | 94 | 0 | — | 0 | 0 |
| proof/integer-predicate-unknownoddp | 14 | 0 | 0 | 14 | 0 | — | 0 | 0 |
| proof/integer-predicate-unknownplusp | 152 | 0 | 0 | 152 | 0 | — | 0 | 0 |
| proof/integer-predicate-unknownzerop | 320 | 0 | 0 | 320 | 0 | — | 0 | 0 |
| proof/integer-shift-rangeleft | 4 | 0 | 0 | 4 | 0 | — | 0 | 0 |
| proof/integer-shift-rangeright | 8 | 0 | 0 | 8 | 0 | — | 0 | 0 |
| proof/integer-shift-result-rangeleft | 29 | 0 | 0 | 29 | 0 | — | 0 | 0 |
| proof/integer-shift-result-rangeright | 16 | 0 | 0 | 16 | 0 | — | 0 | 0 |
| proof/interval-wideningall | 403 | 6 | 0 | 391 | 4 | — | 2 | 0 |