Overview

Job 1483

CakeML:d799d23caefc9c1971792072350c9dd7c1779c53
  Update COPYING
HOL:02777f989ba557fe906094a01dd6a18ec7fb2e94
  emacs-mode: fix indentation bug identified in c3e0ecb4ce1
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               4s  93MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 236MB
 Starting semantics
 Finished semantics                                             1m34s 980MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m36s 868MB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  8s 317MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m17s 776MB
 Starting basis/pure
 Finished basis/pure                                            3m11s 868MB
 Starting translator
 Finished translator                                            2m48s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m14s   2GB
 Starting characteristic
 Finished characteristic                                        6m15s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m42s   1GB
 Starting basis
 Finished basis                                                46m59s  11GB
 Starting compiler/inference
 Finished compiler/inference                                    1m13s 980MB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m08s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m48s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      5m04s   4GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   22s 660MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m06s 991MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                2m11s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  39s 965MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m37s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m49s 899MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  18s 594MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    19s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   21s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   19s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   20s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  20s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m13s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m54s 860MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m36s 966MB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           33m23s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m47s 988MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              58m44s  13GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m30s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        14m13s   6GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         7m07s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m52s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        9m41s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m49s 719MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             21s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            23s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            20s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            21s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           22s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         13m40s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m57s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       29s 883MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 705MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m55s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m47s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m50s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             5m54s   5GB
 Starting candle/overloading/syntax
 Finished candle/overloading/syntax                             3m22s   1GB
 Starting candle/overloading/semantics
 Finished candle/overloading/semantics                         13m06s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m19s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   15m52s   8GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           3m21s   2GB
 Starting examples
 Finished examples                                              9m00s   4GB
 Starting examples/compilation/x64
 FAILED: examples/compilation/x64
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
/home/cake/oven/regression/cakeml-1483/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml  
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "catCompile">>
                to_flat eval: runtime: 6.7s,    gctime: 0.35608s,     systime: 0.20071s.
                to_flat real: 6.9s
                to_flat size: 72691
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.37713s,    gctime: 0.06009s,     systime: 0.01796s.
                to_clos real: 0.39575s
                to_clos size: 42660
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 4.4s,    gctime: 0.14563s,     systime: 0.01899s.
                 to_bvl real: 4.5s
                 to_bvl size: 75939
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 36.0s,    gctime: 0.21992s,     systime: 0.02097s.
                 to_bvi real: 36.1s
                 to_bvi size: 80359
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 10.6s,    gctime: 0.44684s,     systime: 0.03798s.
                to_data real: 10.7s
                to_data size: 128946
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 14.9s,    gctime: 0.33971s,     systime: 0.02799s.
           data_to_word real: 14.9s
           data_to_word size: 322925
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m09s,    gctime: 2.3s,     systime: 0.25786s.
 inst,ssa,two-reg (par) real: 31.5s
 inst,ssa,two-reg (par) size: 1286204
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 7.9s,    gctime: 0.89199s,     systime: 0.09379s.
        get_clash (par) real: 3.8s
        get_clash (par) size: 1996027
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 940	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 11	coalesced: 11
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 17	coalesceable: 11	coalesced: 11
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 17	coalesceable: 11	coalesced: 11
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 17	coalesceable: 11	coalesced: 11
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 4375	coalesceable: 2573	coalesced: 2573
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 17	coalesceable: 11	coalesced: 11
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 17	coalesceable: 11	coalesced: 11
149 moves: 17	coalesceable: 11	coalesced: 11
150 moves: 17	coalesceable: 11	coalesced: 11
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 17	coalesceable: 11	coalesced: 11
153 moves: 17	coalesceable: 11	coalesced: 11
154 moves: 10	coalesceable: 6	coalesced: 6
155 moves: 60	coalesceable: 41	coalesced: 40
156 moves: 17	coalesceable: 11	coalesced: 11
157 moves: 17	coalesceable: 11	coalesced: 11
158 moves: 17	coalesceable: 11	coalesced: 11
159 moves: 17	coalesceable: 11	coalesced: 11
160 moves: 17	coalesceable: 11	coalesced: 11
161 moves: 17	coalesceable: 11	coalesced: 11
162 moves: 17	coalesceable: 11	coalesced: 11
163 moves: 17	coalesceable: 11	coalesced: 11
164 moves: 17	coalesceable: 11	coalesced: 11
165 moves: 17	coalesceable: 11	coalesced: 11
166 moves: 2	coalesceable: 2	coalesced: 2
167 moves: 17	coalesceable: 11	coalesced: 11
168 moves: 17	coalesceable: 11	coalesced: 11
169 moves: 17	coalesceable: 11	coalesced: 11
170 moves: 5	coalesceable: 3	coalesced: 3
171 moves: 6	coalesceable: 6	coalesced: 6
172 moves: 29	coalesceable: 19	coalesced: 13
173 moves: 4	coalesceable: 4	coalesced: 4
174 moves: 7	coalesceable: 7	coalesced: 7
175 moves: 4	coalesceable: 4	coalesced: 4
176 moves: 9	coalesceable: 9	coalesced: 8
177 moves: 8	coalesceable: 8	coalesced: 8
178 moves: 124	coalesceable: 72	coalesced: 58
179 moves: 6	coalesceable: 6	coalesced: 6
180 moves: 62	coalesceable: 31	coalesced: 29
181 moves: 4	coalesceable: 4	coalesced: 4
182 moves: 48	coalesceable: 23	coalesced: 21
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 23	coalesceable: 15	coalesced: 11
185 moves: 6	coalesceable: 6	coalesced: 6
186 moves: 23	coalesceable: 15	coalesced: 11
187 moves: 6	coalesceable: 6	coalesced: 6
188 moves: 30	coalesceable: 19	coalesced: 16
189 moves: 6	coalesceable: 6	coalesced: 6
190 moves: 29	coalesceable: 21	coalesced: 17
191 moves: 6	coalesceable: 6	coalesced: 6
192 moves: 24	coalesceable: 16	coalesced: 13
193 moves: 6	coalesceable: 6	coalesced: 6
194 moves: 24	coalesceable: 16	coalesced: 13
195 moves: 6	coalesceable: 6	coalesced: 6
196 moves: 30	coalesceable: 22	coalesced: 19
197 moves: 6	coalesceable: 6	coalesced: 6
198 moves: 60	coalesceable: 44	coalesced: 41
199 moves: 6	coalesceable: 6	coalesced: 6
200 moves: 62	coalesceable: 31	coalesced: 29
201 moves: 4	coalesceable: 4	coalesced: 4
202 moves: 3	coalesceable: 3	coalesced: 3
203 moves: 4	coalesceable: 4	coalesced: 4
204 moves: 43	coalesceable: 29	coalesced: 25
205 moves: 4	coalesceable: 4	coalesced: 4
206 moves: 3	coalesceable: 3	coalesced: 3
207 moves: 4	coalesceable: 4	coalesced: 4
208 moves: 18	coalesceable: 16	coalesced: 16
209 moves: 4	coalesceable: 4	coalesced: 4
210 moves: 25	coalesceable: 18	coalesced: 16
211 moves: 4	coalesceable: 4	coalesced: 4
212 moves: 3	coalesceable: 3	coalesced: 3
213 moves: 6	coalesceable: 6	coalesced: 6
214 moves: 36	coalesceable: 23	coalesced: 17
215 moves: 6	coalesceable: 6	coalesced: 6
216 moves: 21	coalesceable: 19	coalesced: 19
217 moves: 8	coalesceable: 8	coalesced: 8
218 moves: 22	coalesceable: 20	coalesced: 20
219 moves: 12	coalesceable: 12	coalesced: 12
220 moves: 218	coalesceable: 134	coalesced: 94
221 moves: 8	coalesceable: 8	coalesced: 8
222 moves: 124	coalesceable: 72	coalesced: 58
223 moves: 4	coalesceable: 4	coalesced: 4
224 moves: 77	coalesceable: 56	coalesced: 53
225 moves: 6	coalesceable: 6	coalesced: 6
226 moves: 110	coalesceable: 79	coalesced: 69
227 moves: 8	coalesceable: 8	coalesced: 8
228 moves: 407	coalesceable: 208	coalesced: 175
229 moves: 4	coalesceable: 4	coalesced: 4
230 moves: 56	coalesceable: 33	coalesced: 30
231 moves: 4	coalesceable: 4	coalesced: 4
232 moves: 8	coalesceable: 6	coalesced: 6
233 moves: 8	coalesceable: 8	coalesced: 8
234 moves: 163	coalesceable: 110	coalesced: 96
235 moves: 6	coalesceable: 6	coalesced: 6
236 moves: 114	coalesceable: 80	coalesced: 72
237 moves: 4	coalesceable: 4	coalesced: 4
238 moves: 6	coalesceable: 6	coalesced: 6
239 moves: 4	coalesceable: 4	coalesced: 4
240 moves: 6	coalesceable: 6	coalesced: 6
241 moves: 8	coalesceable: 8	coalesced: 8
242 moves: 128	coalesceable: 77	coalesced: 70
243 moves: 8	coalesceable: 8	coalesced: 8
244 moves: 111	coalesceable: 66	coalesced: 51
245 moves: 6	coalesceable: 6	coalesced: 6
246 moves: 50	coalesceable: 38	coalesced: 35
247 moves: 6	coalesceable: 6	coalesced: 6
248 moves: 427	coalesceable: 263	coalesced: 198
249 moves: 4	coalesceable: 4	coalesced: 4
250 moves: 5	coalesceable: 5	coalesced: 5
251 moves: 4	coalesceable: 4	coalesced: 4
252 moves: 272	coalesceable: 139	coalesced: 131
253 moves: 4	coalesceable: 4	coalesced: 4
254 moves: 69	coalesceable: 54	coalesced: 54
255 moves: 6	coalesceable: 6	coalesced: 6
256 moves: 78	coalesceable: 59	coalesced: 56
257 moves: 4	coalesceable: 4	coalesced: 4
258 moves: 21	coalesceable: 18	coalesced: 16
259 moves: 4	coalesceable: 4	coalesced: 4
260 moves: 15	coalesceable: 12	coalesced: 12
261 moves: 25	coalesceable: 21	coalesced: 21
262 moves: 24	coalesceable: 15	coalesced: 15
263 moves: 4	coalesceable: 4	coalesced: 4
264 moves: 34	coalesceable: 19	coalesced: 17
265 moves: 4	coalesceable: 4	coalesced: 4
266 moves: 16	coalesceable: 11	coalesced: 10
267 moves: 4	coalesceable: 4	coalesced: 4
268 moves: 11	coalesceable: 7	coalesced: 7

runtime: 9.2s,    gctime: 0.12233s,     systime: 0.01196s.
        external oracle real: 9.2s
        external oracle size: 146748
     apply colour (par) eval: runtime: 1m28s,    gctime: 6.6s,     systime: 0.67242s.
     apply colour (par) real: 49.8s
     apply colour (par) size: 647308
           check colour eval: runtime: 1.3s,    gctime: 0.12723s,     systime: 0.01897s.
           check colour real: 1.3s
           check colour size: 647578
          word_to_stack eval: runtime: 1m02s,    gctime: 1.9s,     systime: 0.26337s.
          word_to_stack real: 1m02s
          word_to_stack size: 527185
          stack_rawcall eval: runtime: 40.1s,    gctime: 4.2s,     systime: 0.26360s.
          stack_rawcall real: 40.4s
          stack_rawcall size: 520032
      stack_alloc (par) eval: runtime: 50.6s,    gctime: 0.85258s,     systime: 0.11071s.
      stack_alloc (par) real: 22.9s
      stack_alloc (par) size: 521980
expand stack_remove_def eval: runtime: 0.03506s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03513s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m14s,    gctime: 8.1s,     systime: 0.91348s.
     stack_remove (par) real: 42.3s
     stack_remove (par) size: 889970
      stack_names (par) eval: runtime: 35.4s,    gctime: 0.67345s,     systime: 0.07584s.
      stack_names (par) real: 16.5s
      stack_names (par) size: 918563
     stack_to_lab (par) eval: runtime: 1m12s,    gctime: 1.3s,     systime: 0.13379s.
     stack_to_lab (par) real: 33.2s
     stack_to_lab (par) size: 1119677
          lab_to_target eval: runtime: 3m33s,    gctime: 10.1s,     systime: 0.89597s.
          lab_to_target real: 3m34s
          lab_to_target size: 1801640
                      export: runtime: 0.47625s,    gctime: 0.00000s,     systime: 0.15379s.
Saved theorem _____ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 13m40s to build
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "diffCompile">>
                to_flat eval: runtime: 7.6s,    gctime: 0.46123s,     systime: 0.09794s.
                to_flat real: 7.7s
                to_flat size: 120491
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.79011s,    gctime: 0.09699s,     systime: 0.00500s.
                to_clos real: 0.79626s
                to_clos size: 64819
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 6.1s,    gctime: 0.23551s,     systime: 0.02495s.
                 to_bvl real: 6.1s
                 to_bvl size: 120565
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 45.0s,    gctime: 0.44740s,     systime: 0.03587s.
                 to_bvi real: 45.1s
                 to_bvi size: 118173
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 12.8s,    gctime: 0.53005s,     systime: 0.04496s.
                to_data real: 12.9s
                to_data size: 189749
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 19.5s,    gctime: 0.61796s,     systime: 0.04490s.
           data_to_word real: 19.6s
           data_to_word size: 432035
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m02s,    gctime: 8.4s,     systime: 0.81601s.
 inst,ssa,two-reg (par) real: 41.9s
 inst,ssa,two-reg (par) size: 1675692
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 14.0s,    gctime: 1.3s,     systime: 0.11683s.
        get_clash (par) real: 4.6s
        get_clash (par) size: 2632093
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 972	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 11	coalesced: 11
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 17	coalesceable: 11	coalesced: 11
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 17	coalesceable: 11	coalesced: 11
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 17	coalesceable: 11	coalesced: 11
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 17	coalesceable: 11	coalesced: 11
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 17	coalesceable: 11	coalesced: 11
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 17	coalesceable: 11	coalesced: 11
149 moves: 17	coalesceable: 11	coalesced: 11
150 moves: 4375	coalesceable: 2573	coalesced: 2573
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 17	coalesceable: 11	coalesced: 11
153 moves: 17	coalesceable: 11	coalesced: 11
154 moves: 17	coalesceable: 11	coalesced: 11
155 moves: 17	coalesceable: 11	coalesced: 11
156 moves: 17	coalesceable: 11	coalesced: 11
157 moves: 17	coalesceable: 11	coalesced: 11
158 moves: 17	coalesceable: 11	coalesced: 11
159 moves: 17	coalesceable: 11	coalesced: 11
160 moves: 17	coalesceable: 11	coalesced: 11
161 moves: 17	coalesceable: 11	coalesced: 11
162 moves: 17	coalesceable: 11	coalesced: 11
163 moves: 17	coalesceable: 11	coalesced: 11
164 moves: 17	coalesceable: 11	coalesced: 11
165 moves: 17	coalesceable: 11	coalesced: 11
166 moves: 17	coalesceable: 11	coalesced: 11
167 moves: 17	coalesceable: 11	coalesced: 11
168 moves: 17	coalesceable: 11	coalesced: 11
169 moves: 10	coalesceable: 6	coalesced: 6
170 moves: 60	coalesceable: 41	coalesced: 40
171 moves: 60	coalesceable: 41	coalesced: 40
172 moves: 17	coalesceable: 11	coalesced: 11
173 moves: 17	coalesceable: 11	coalesced: 11
174 moves: 17	coalesceable: 11	coalesced: 11
175 moves: 17	coalesceable: 11	coalesced: 11
176 moves: 17	coalesceable: 11	coalesced: 11
177 moves: 17	coalesceable: 11	coalesced: 11
178 moves: 17	coalesceable: 11	coalesced: 11
179 moves: 17	coalesceable: 11	coalesced: 11
180 moves: 17	coalesceable: 11	coalesced: 11
181 moves: 17	coalesceable: 11	coalesced: 11
182 moves: 17	coalesceable: 11	coalesced: 11
183 moves: 17	coalesceable: 11	coalesced: 11
184 moves: 17	coalesceable: 11	coalesced: 11
185 moves: 2	coalesceable: 2	coalesced: 2
186 moves: 17	coalesceable: 11	coalesced: 11
187 moves: 17	coalesceable: 11	coalesced: 11
188 moves: 17	coalesceable: 11	coalesced: 11
189 moves: 17	coalesceable: 11	coalesced: 11
190 moves: 17	coalesceable: 11	coalesced: 11
191 moves: 17	coalesceable: 11	coalesced: 11
192 moves: 17	coalesceable: 11	coalesced: 11
193 moves: 17	coalesceable: 11	coalesced: 11
194 moves: 17	coalesceable: 11	coalesced: 11
195 moves: 17	coalesceable: 11	coalesced: 11
196 moves: 17	coalesceable: 11	coalesced: 11
197 moves: 17	coalesceable: 11	coalesced: 11
198 moves: 17	coalesceable: 11	coalesced: 11
199 moves: 17	coalesceable: 11	coalesced: 11
200 moves: 17	coalesceable: 11	coalesced: 11
201 moves: 17	coalesceable: 11	coalesced: 11
202 moves: 17	coalesceable: 11	coalesced: 11
203 moves: 114	coalesceable: 84	coalesced: 84
204 moves: 17	coalesceable: 11	coalesced: 11
205 moves: 17	coalesceable: 11	coalesced: 11
206 moves: 5	coalesceable: 3	coalesced: 3
207 moves: 4	coalesceable: 4	coalesced: 4
208 moves: 6	coalesceable: 6	coalesced: 6
209 moves: 4	coalesceable: 4	coalesced: 4
210 moves: 6	coalesceable: 6	coalesced: 6
211 moves: 6	coalesceable: 6	coalesced: 6
212 moves: 29	coalesceable: 19	coalesced: 13
213 moves: 6	coalesceable: 6	coalesced: 6
214 moves: 32	coalesceable: 23	coalesced: 18
215 moves: 4	coalesceable: 4	coalesced: 4
216 moves: 5	coalesceable: 5	coalesced: 3
217 moves: 6	coalesceable: 6	coalesced: 6
218 moves: 36	coalesceable: 25	coalesced: 24
219 moves: 4	coalesceable: 4	coalesced: 4
220 moves: 5	coalesceable: 5	coalesced: 3
221 moves: 4	coalesceable: 4	coalesced: 4
222 moves: 7	coalesceable: 7	coalesced: 7
223 moves: 4	coalesceable: 4	coalesced: 4
224 moves: 7	coalesceable: 7	coalesced: 7
225 moves: 4	coalesceable: 4	coalesced: 4
226 moves: 45	coalesceable: 35	coalesced: 33
227 moves: 6	coalesceable: 6	coalesced: 6
228 moves: 86	coalesceable: 57	coalesced: 51
229 moves: 6	coalesceable: 6	coalesced: 6
230 moves: 76	coalesceable: 47	coalesced: 43
231 moves: 4	coalesceable: 4	coalesced: 4
232 moves: 9	coalesceable: 9	coalesced: 8
233 moves: 8	coalesceable: 8	coalesced: 8
234 moves: 124	coalesceable: 72	coalesced: 58
235 moves: 6	coalesceable: 6	coalesced: 6
236 moves: 62	coalesceable: 31	coalesced: 29
237 moves: 4	coalesceable: 4	coalesced: 4
238 moves: 48	coalesceable: 23	coalesced: 21
239 moves: 6	coalesceable: 6	coalesced: 6
240 moves: 23	coalesceable: 15	coalesced: 11
241 moves: 6	coalesceable: 6	coalesced: 6
242 moves: 23	coalesceable: 15	coalesced: 11
243 moves: 6	coalesceable: 6	coalesced: 6
244 moves: 30	coalesceable: 19	coalesced: 16
245 moves: 6	coalesceable: 6	coalesced: 6
246 moves: 29	coalesceable: 21	coalesced: 17
247 moves: 6	coalesceable: 6	coalesced: 6
248 moves: 24	coalesceable: 16	coalesced: 13
249 moves: 6	coalesceable: 6	coalesced: 6
250 moves: 24	coalesceable: 16	coalesced: 13
251 moves: 6	coalesceable: 6	coalesced: 6
252 moves: 30	coalesceable: 22	coalesced: 19
253 moves: 6	coalesceable: 6	coalesced: 6
254 moves: 60	coalesceable: 44	coalesced: 41
255 moves: 6	coalesceable: 6	coalesced: 6
256 moves: 62	coalesceable: 31	coalesced: 29
257 moves: 6	coalesceable: 6	coalesced: 6
258 moves: 79	coalesceable: 52	coalesced: 46
259 moves: 4	coalesceable: 4	coalesced: 4
260 moves: 162	coalesceable: 108	coalesced: 98
261 moves: 8	coalesceable: 8	coalesced: 8
262 moves: 284	coalesceable: 173	coalesced: 140
263 moves: 8	coalesceable: 8	coalesced: 8
264 moves: 119	coalesceable: 79	coalesced: 60
265 moves: 4	coalesceable: 4	coalesced: 4
266 moves: 423	coalesceable: 264	coalesced: 209
267 moves: 4	coalesceable: 4	coalesced: 4
268 moves: 3	coalesceable: 3	coalesced: 3
269 moves: 4	coalesceable: 4	coalesced: 4
270 moves: 43	coalesceable: 29	coalesced: 25
271 moves: 4	coalesceable: 4	coalesced: 4
272 moves: 25	coalesceable: 18	coalesced: 16
273 moves: 4	coalesceable: 4	coalesced: 4
274 moves: 3	coalesceable: 3	coalesced: 3
275 moves: 6	coalesceable: 6	coalesced: 6
276 moves: 36	coalesceable: 23	coalesced: 17
277 moves: 6	coalesceable: 6	coalesced: 6
278 moves: 21	coalesceable: 19	coalesced: 19
279 moves: 4	coalesceable: 4	coalesced: 4
280 moves: 9	coalesceable: 9	coalesced: 8
281 moves: 8	coalesceable: 8	coalesced: 8
282 moves: 22	coalesceable: 20	coalesced: 20
283 moves: 12	coalesceable: 12	coalesced: 12
284 moves: 218	coalesceable: 134	coalesced: 94
285 moves: 12	coalesceable: 12	coalesced: 12
286 moves: 218	coalesceable: 134	coalesced: 94
287 moves: 8	coalesceable: 8	coalesced: 8
288 moves: 124	coalesceable: 72	coalesced: 58
289 moves: 4	coalesceable: 4	coalesced: 4
290 moves: 77	coalesceable: 56	coalesced: 53
291 moves: 6	coalesceable: 6	coalesced: 6
292 moves: 110	coalesceable: 79	coalesced: 69
293 moves: 8	coalesceable: 8	coalesced: 8
294 moves: 407	coalesceable: 208	coalesced: 175
295 moves: 4	coalesceable: 4	coalesced: 4
296 moves: 56	coalesceable: 33	coalesced: 30
297 moves: 4	coalesceable: 4	coalesced: 4
298 moves: 8	coalesceable: 6	coalesced: 6
299 moves: 8	coalesceable: 8	coalesced: 8
300 moves: 163	coalesceable: 110	coalesced: 96
301 moves: 6	coalesceable: 6	coalesced: 6
302 moves: 114	coalesceable: 80	coalesced: 72
303 moves: 4	coalesceable: 4	coalesced: 4
304 moves: 6	coalesceable: 6	coalesced: 6
305 moves: 4	coalesceable: 4	coalesced: 4
306 moves: 6	coalesceable: 6	coalesced: 6
307 moves: 8	coalesceable: 8	coalesced: 8
308 moves: 128	coalesceable: 77	coalesced: 70
309 moves: 8	coalesceable: 8	coalesced: 8
310 moves: 111	coalesceable: 66	coalesced: 51
311 moves: 6	coalesceable: 6	coalesced: 6
312 moves: 427	coalesceable: 263	coalesced: 198
313 moves: 4	coalesceable: 4	coalesced: 4
314 moves: 5	coalesceable: 5	coalesced: 5
315 moves: 4	coalesceable: 4	coalesced: 4
316 moves: 17	coalesceable: 12	coalesced: 11
317 moves: 4	coalesceable: 4	coalesced: 4
318 moves: 272	coalesceable: 139	coalesced: 131
319 moves: 4	coalesceable: 4	coalesced: 4
320 moves: 69	coalesceable: 54	coalesced: 54
321 moves: 6	coalesceable: 6	coalesced: 6
322 moves: 78	coalesceable: 59	coalesced: 56
323 moves: 4	coalesceable: 4	coalesced: 4
324 moves: 21	coalesceable: 18	coalesced: 16
325 moves: 4	coalesceable: 4	coalesced: 4
326 moves: 164	coalesceable: 106	coalesced: 89
327 moves: 224	coalesceable: 137	coalesced: 113
328 moves: 217	coalesceable: 133	coalesced: 108
329 moves: 4	coalesceable: 4	coalesced: 4
330 moves: 45	coalesceable: 26	coalesced: 24
331 moves: 4	coalesceable: 4	coalesced: 4
332 moves: 42	coalesceable: 23	coalesced: 22
333 moves: 4	coalesceable: 4	coalesced: 4
334 moves: 15	coalesceable: 12	coalesced: 12
335 moves: 36	coalesceable: 18	coalesced: 18
336 moves: 6	coalesceable: 6	coalesced: 6
337 moves: 95	coalesceable: 59	coalesced: 59
338 moves: 12	coalesceable: 12	coalesced: 12
339 moves: 362	coalesceable: 166	coalesced: 106
340 moves: 8	coalesceable: 8	coalesced: 8
341 moves: 98	coalesceable: 66	coalesced: 52
342 moves: 6	coalesceable: 6	coalesced: 6
343 moves: 84	coalesceable: 52	coalesced: 43
344 moves: 6	coalesceable: 6	coalesced: 6
345 moves: 55	coalesceable: 28	coalesced: 23
346 moves: 6	coalesceable: 6	coalesced: 6
347 moves: 90	coalesceable: 61	coalesced: 58
348 moves: 8	coalesceable: 8	coalesced: 8
349 moves: 157	coalesceable: 106	coalesced: 88
350 moves: 6	coalesceable: 6	coalesced: 6
351 moves: 99	coalesceable: 62	coalesced: 56
352 moves: 6	coalesceable: 6	coalesced: 6
353 moves: 275	coalesceable: 122	coalesced: 107
354 moves: 6	coalesceable: 6	coalesced: 6
355 moves: 7	coalesceable: 7	coalesced: 7
356 moves: 10	coalesceable: 10	coalesced: 10
357 moves: 375	coalesceable: 141	coalesced: 119
358 moves: 6	coalesceable: 6	coalesced: 6
359 moves: 35	coalesceable: 25	coalesced: 20
360 moves: 10	coalesceable: 10	coalesced: 10
361 moves: 1001	coalesceable: 448	coalesced: 387
362 moves: 6	coalesceable: 6	coalesced: 6
363 moves: 162	coalesceable: 92	coalesced: 88
364 moves: 33	coalesceable: 25	coalesced: 23
365 moves: 33	coalesceable: 25	coalesced: 23
366 moves: 12	coalesceable: 12	coalesced: 12
367 moves: 2015	coalesceable: 1063	coalesced: 797
368 moves: 6	coalesceable: 6	coalesced: 6
369 moves: 690	coalesceable: 353	coalesced: 200
370 moves: 4	coalesceable: 4	coalesced: 4
371 moves: 266	coalesceable: 170	coalesced: 166
372 moves: 6	coalesceable: 6	coalesced: 6
373 moves: 570	coalesceable: 359	coalesced: 352
374 moves: 4	coalesceable: 4	coalesced: 4
375 moves: 47	coalesceable: 39	coalesced: 39

runtime: 9.1s,    gctime: 0.14109s,     systime: 0.02193s.
        external oracle real: 9.2s
        external oracle size: 198691
     apply colour (par) eval: runtime: 2m29s,    gctime: 7.8s,     systime: 0.98985s.
     apply colour (par) real: 56.8s
     apply colour (par) size: 849607
           check colour eval: runtime: 3.1s,    gctime: 0.42791s,     systime: 0.07092s.
           check colour real: 3.2s
           check colour size: 849984
          word_to_stack eval: runtime: 1m31s,    gctime: 7.7s,     systime: 1.1s.
          word_to_stack real: 1m32s
          word_to_stack size: 673984
          stack_rawcall eval: runtime: 46.9s,    gctime: 0.54946s,     systime: 0.06479s.
          stack_rawcall real: 47.0s
          stack_rawcall size: 665204
      stack_alloc (par) eval: runtime: 1m14s,    gctime: 0.73894s,     systime: 0.10783s.
      stack_alloc (par) real: 24.5s
      stack_alloc (par) size: 669170
expand stack_remove_def eval: runtime: 0.03394s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03401s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m41s,    gctime: 0.97235s,     systime: 0.14349s.
     stack_remove (par) real: 37.8s
     stack_remove (par) size: 1120033
      stack_names (par) eval: runtime: 51.7s,    gctime: 0.85036s,     systime: 0.09976s.
      stack_names (par) real: 17.2s
      stack_names (par) size: 1156806
     stack_to_lab (par) eval: runtime: 1m47s,    gctime: 1.7s,     systime: 0.17274s.
     stack_to_lab (par) real: 35.0s
     stack_to_lab (par) size: 1425269
          lab_to_target eval: runtime: 4m38s,    gctime: 19.3s,     systime: 1.8s.
          lab_to_target real: 4m41s
          lab_to_target size: 2313542
                      export: runtime: 0.48799s,    gctime: 0.00000s,     systime: 0.00199s.
Saved theorem _____ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 19m28s to build
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "echoCompile">>
                to_flat eval: runtime: 6.5s,    gctime: 0.27650s,     systime: 0.11785s.
                to_flat real: 6.6s
                to_flat size: 67572
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.33475s,    gctime: 0.06708s,     systime: 0.00301s.
                to_clos real: 0.33839s
                to_clos size: 40080
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 4.1s,    gctime: 0.14212s,     systime: 0.01803s.
                 to_bvl real: 4.1s
                 to_bvl size: 67165
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 34.6s,    gctime: 0.38284s,     systime: 0.03406s.
                 to_bvi real: 34.6s
                 to_bvi size: 72907
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 10.3s,    gctime: 0.51623s,     systime: 0.04694s.
                to_data real: 10.4s
                to_data size: 121432
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 14.6s,    gctime: 0.59158s,     systime: 0.04486s.
           data_to_word real: 14.7s
           data_to_word size: 311616
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m05s,    gctime: 2.7s,     systime: 0.31045s.
 inst,ssa,two-reg (par) real: 31.8s
 inst,ssa,two-reg (par) size: 1252479
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 7.6s,    gctime: 1.1s,     systime: 0.09988s.
        get_clash (par) real: 3.9s
        get_clash (par) size: 1948615
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 934	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 11	coalesced: 11
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 17	coalesceable: 11	coalesced: 11
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 17	coalesceable: 11	coalesced: 11
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 4375	coalesceable: 2573	coalesced: 2573
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 17	coalesceable: 11	coalesced: 11
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 17	coalesceable: 11	coalesced: 11
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 17	coalesceable: 11	coalesced: 11
149 moves: 10	coalesceable: 6	coalesced: 6
150 moves: 60	coalesceable: 41	coalesced: 40
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 17	coalesceable: 11	coalesced: 11
153 moves: 17	coalesceable: 11	coalesced: 11
154 moves: 17	coalesceable: 11	coalesced: 11
155 moves: 17	coalesceable: 11	coalesced: 11
156 moves: 2	coalesceable: 2	coalesced: 2
157 moves: 17	coalesceable: 11	coalesced: 11
158 moves: 5	coalesceable: 3	coalesced: 3
159 moves: 6	coalesceable: 6	coalesced: 6
160 moves: 29	coalesceable: 19	coalesced: 13
161 moves: 4	coalesceable: 4	coalesced: 4
162 moves: 7	coalesceable: 7	coalesced: 7
163 moves: 4	coalesceable: 4	coalesced: 4
164 moves: 9	coalesceable: 9	coalesced: 8
165 moves: 8	coalesceable: 8	coalesced: 8
166 moves: 124	coalesceable: 72	coalesced: 58
167 moves: 6	coalesceable: 6	coalesced: 6
168 moves: 62	coalesceable: 31	coalesced: 29
169 moves: 8	coalesceable: 8	coalesced: 8
170 moves: 180	coalesceable: 93	coalesced: 89
171 moves: 6	coalesceable: 6	coalesced: 6
172 moves: 7	coalesceable: 7	coalesced: 4
173 moves: 6	coalesceable: 6	coalesced: 6
174 moves: 23	coalesceable: 15	coalesced: 11
175 moves: 6	coalesceable: 6	coalesced: 6
176 moves: 23	coalesceable: 15	coalesced: 11
177 moves: 6	coalesceable: 6	coalesced: 6
178 moves: 30	coalesceable: 19	coalesced: 16
179 moves: 6	coalesceable: 6	coalesced: 6
180 moves: 29	coalesceable: 21	coalesced: 17
181 moves: 6	coalesceable: 6	coalesced: 6
182 moves: 24	coalesceable: 16	coalesced: 13
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 24	coalesceable: 16	coalesced: 13
185 moves: 6	coalesceable: 6	coalesced: 6
186 moves: 30	coalesceable: 22	coalesced: 19
187 moves: 4	coalesceable: 4	coalesced: 4
188 moves: 3	coalesceable: 3	coalesced: 3
189 moves: 4	coalesceable: 4	coalesced: 4
190 moves: 25	coalesceable: 18	coalesced: 16
191 moves: 4	coalesceable: 4	coalesced: 4
192 moves: 3	coalesceable: 3	coalesced: 3
193 moves: 6	coalesceable: 6	coalesced: 6
194 moves: 36	coalesceable: 23	coalesced: 17
195 moves: 6	coalesceable: 6	coalesced: 6
196 moves: 21	coalesceable: 19	coalesced: 19
197 moves: 8	coalesceable: 8	coalesced: 8
198 moves: 22	coalesceable: 20	coalesced: 20
199 moves: 12	coalesceable: 12	coalesced: 12
200 moves: 218	coalesceable: 134	coalesced: 94
201 moves: 8	coalesceable: 8	coalesced: 8
202 moves: 124	coalesceable: 72	coalesced: 58
203 moves: 4	coalesceable: 4	coalesced: 4
204 moves: 77	coalesceable: 56	coalesced: 53
205 moves: 6	coalesceable: 6	coalesced: 6
206 moves: 110	coalesceable: 79	coalesced: 69
207 moves: 8	coalesceable: 8	coalesced: 8
208 moves: 407	coalesceable: 208	coalesced: 175
209 moves: 4	coalesceable: 4	coalesced: 4
210 moves: 56	coalesceable: 33	coalesced: 30
211 moves: 4	coalesceable: 4	coalesced: 4
212 moves: 8	coalesceable: 6	coalesced: 6
213 moves: 8	coalesceable: 8	coalesced: 8
214 moves: 163	coalesceable: 110	coalesced: 96
215 moves: 6	coalesceable: 6	coalesced: 6
216 moves: 114	coalesceable: 80	coalesced: 72
217 moves: 4	coalesceable: 4	coalesced: 4
218 moves: 6	coalesceable: 6	coalesced: 6
219 moves: 8	coalesceable: 8	coalesced: 8
220 moves: 128	coalesceable: 77	coalesced: 70
221 moves: 8	coalesceable: 8	coalesced: 8
222 moves: 111	coalesceable: 66	coalesced: 51
223 moves: 6	coalesceable: 6	coalesced: 6
224 moves: 50	coalesceable: 38	coalesced: 35
225 moves: 6	coalesceable: 6	coalesced: 6
226 moves: 427	coalesceable: 263	coalesced: 198
227 moves: 4	coalesceable: 4	coalesced: 4
228 moves: 5	coalesceable: 5	coalesced: 5
229 moves: 4	coalesceable: 4	coalesced: 4
230 moves: 36	coalesceable: 21	coalesced: 19

runtime: 9.5s,    gctime: 0.13874s,     systime: 0.01593s.
        external oracle real: 9.5s
        external oracle size: 141827
     apply colour (par) eval: runtime: 1m23s,    gctime: 7.3s,     systime: 0.81411s.
     apply colour (par) real: 50.6s
     apply colour (par) size: 625527
           check colour eval: runtime: 1.1s,    gctime: 0.10143s,     systime: 0.01400s.
           check colour real: 1.2s
           check colour size: 625759
          word_to_stack eval: runtime: 1m01s,    gctime: 1.7s,     systime: 0.24052s.
          word_to_stack real: 1m01s
          word_to_stack size: 511058
          stack_rawcall eval: runtime: 36.0s,    gctime: 1.0s,     systime: 0.17168s.
          stack_rawcall real: 36.2s
          stack_rawcall size: 504423
      stack_alloc (par) eval: runtime: 47.9s,    gctime: 0.62748s,     systime: 0.22042s.
      stack_alloc (par) real: 22.6s
      stack_alloc (par) size: 506070
expand stack_remove_def eval: runtime: 0.03374s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03381s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m04s,    gctime: 1.9s,     systime: 0.30841s.
     stack_remove (par) real: 35.6s
     stack_remove (par) size: 864239
      stack_names (par) eval: runtime: 36.7s,    gctime: 3.8s,     systime: 0.65145s.
      stack_names (par) real: 19.4s
      stack_names (par) size: 891944
     stack_to_lab (par) eval: runtime: 1m08s,    gctime: 1.2s,     systime: 0.12481s.
     stack_to_lab (par) real: 32.0s
     stack_to_lab (par) size: 1085176
          lab_to_target eval: runtime: 3m20s,    gctime: 5.0s,     systime: 0.57978s.
          lab_to_target real: 3m21s
          lab_to_target size: 1742975
                      export: runtime: 0.46518s,    gctime: 0.05054s,     systime: 0.03695s.
Saved theorem _____ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 13m03s to build
cc cat.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o  -o cake_cat
cc diff.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o  -o cake_diff
cc echo.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o  -o cake_echo
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "grepCompile">>
                to_flat eval: runtime: 14.7s,    gctime: 0.67592s,     systime: 0.16266s.
                to_flat real: 14.9s
                to_flat size: 316098
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 2.6s,    gctime: 0.23480s,     systime: 0.02397s.
                to_clos real: 2.6s
                to_clos size: 150578
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 14.8s,    gctime: 0.55652s,     systime: 0.03485s.
                 to_bvl real: 14.8s
                 to_bvl size: 268774
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 1m33s,    gctime: 1.2s,     systime: 0.08180s.
                 to_bvi real: 1m33s
                 to_bvi size: 238174
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 27.9s,    gctime: 1.6s,     systime: 0.13877s.
                to_data real: 28.1s
                to_data size: 444515
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 1m04s,    gctime: 3.2s,     systime: 0.21161s.
           data_to_word real: 1m04s
           data_to_word size: 1269032
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 13m07s,    gctime: 1m17s,     systime: 10.2s.
 inst,ssa,two-reg (par) real: 9m02s
 inst,ssa,two-reg (par) size: 4751385
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 39.5s,    gctime: 3.9s,     systime: 0.43718s.
        get_clash (par) real: 14.2s
        get_clash (par) size: 7257967
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 200	coalesceable: 2	coalesced: 2
118 moves: 1002	coalesceable: 2	coalesced: 2
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 17	coalesceable: 11	coalesced: 11
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 17	coalesceable: 11	coalesced: 11
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 17	coalesceable: 11	coalesced: 11
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 17	coalesceable: 11	coalesced: 11
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 17	coalesceable: 11	coalesced: 11
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 17	coalesceable: 11	coalesced: 11
149 moves: 17	coalesceable: 11	coalesced: 11
150 moves: 17	coalesceable: 11	coalesced: 11
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 17	coalesceable: 11	coalesced: 11
153 moves: 17	coalesceable: 11	coalesced: 11
154 moves: 17	coalesceable: 11	coalesced: 11
155 moves: 17	coalesceable: 11	coalesced: 11
156 moves: 17	coalesceable: 11	coalesced: 11
157 moves: 17	coalesceable: 11	coalesced: 11
158 moves: 17	coalesceable: 11	coalesced: 11
159 moves: 4375	coalesceable: 2573	coalesced: 2573
160 moves: 17	coalesceable: 11	coalesced: 11
161 moves: 17	coalesceable: 11	coalesced: 11
162 moves: 17	coalesceable: 11	coalesced: 11
163 moves: 17	coalesceable: 11	coalesced: 11
164 moves: 17	coalesceable: 11	coalesced: 11
165 moves: 17	coalesceable: 11	coalesced: 11
166 moves: 17	coalesceable: 11	coalesced: 11
167 moves: 17	coalesceable: 11	coalesced: 11
168 moves: 17	coalesceable: 11	coalesced: 11
169 moves: 17	coalesceable: 11	coalesced: 11
170 moves: 17	coalesceable: 11	coalesced: 11
171 moves: 17	coalesceable: 11	coalesced: 11
172 moves: 17	coalesceable: 11	coalesced: 11
173 moves: 17	coalesceable: 11	coalesced: 11
174 moves: 17	coalesceable: 11	coalesced: 11
175 moves: 17	coalesceable: 11	coalesced: 11
176 moves: 17	coalesceable: 11	coalesced: 11
177 moves: 17	coalesceable: 11	coalesced: 11
178 moves: 10	coalesceable: 6	coalesced: 6
179 moves: 60	coalesceable: 41	coalesced: 40
180 moves: 60	coalesceable: 41	coalesced: 40
181 moves: 17	coalesceable: 11	coalesced: 11
182 moves: 17	coalesceable: 11	coalesced: 11
183 moves: 17	coalesceable: 11	coalesced: 11
184 moves: 17	coalesceable: 11	coalesced: 11
185 moves: 17	coalesceable: 11	coalesced: 11
186 moves: 17	coalesceable: 11	coalesced: 11
187 moves: 17	coalesceable: 11	coalesced: 11
188 moves: 17	coalesceable: 11	coalesced: 11
189 moves: 17	coalesceable: 11	coalesced: 11
190 moves: 17	coalesceable: 11	coalesced: 11
191 moves: 2	coalesceable: 2	coalesced: 2
192 moves: 17	coalesceable: 11	coalesced: 11
193 moves: 573	coalesceable: 374	coalesced: 314
194 moves: 2	coalesceable: 2	coalesced: 2
195 moves: 17	coalesceable: 11	coalesced: 11
196 moves: 17	coalesceable: 11	coalesced: 11
197 moves: 17	coalesceable: 11	coalesced: 11
198 moves: 17	coalesceable: 11	coalesced: 11
199 moves: 2	coalesceable: 2	coalesced: 2
200 moves: 2	coalesceable: 2	coalesced: 2
201 moves: 17	coalesceable: 11	coalesced: 11
202 moves: 17	coalesceable: 11	coalesced: 11
203 moves: 17	coalesceable: 11	coalesced: 11
204 moves: 17	coalesceable: 11	coalesced: 11
205 moves: 17	coalesceable: 11	coalesced: 11
206 moves: 17	coalesceable: 11	coalesced: 11
207 moves: 2	coalesceable: 2	coalesced: 2
208 moves: 17	coalesceable: 11	coalesced: 11
209 moves: 17	coalesceable: 11	coalesced: 11
210 moves: 17	coalesceable: 11	coalesced: 11
211 moves: 17	coalesceable: 11	coalesced: 11
212 moves: 17	coalesceable: 11	coalesced: 11
213 moves: 17	coalesceable: 11	coalesced: 11
214 moves: 17	coalesceable: 11	coalesced: 11
215 moves: 17	coalesceable: 11	coalesced: 11
216 moves: 17	coalesceable: 11	coalesced: 11
217 moves: 17	coalesceable: 11	coalesced: 11
218 moves: 17	coalesceable: 11	coalesced: 11
219 moves: 17	coalesceable: 11	coalesced: 11
220 moves: 17	coalesceable: 11	coalesced: 11
221 moves: 51	coalesceable: 31	coalesced: 31
222 moves: 17	coalesceable: 11	coalesced: 11
223 moves: 17	coalesceable: 11	coalesced: 11
224 moves: 17	coalesceable: 11	coalesced: 11
225 moves: 17	coalesceable: 11	coalesced: 11
226 moves: 17	coalesceable: 11	coalesced: 11
227 moves: 16	coalesceable: 11	coalesced: 11
228 moves: 17	coalesceable: 11	coalesced: 11
229 moves: 17	coalesceable: 11	coalesced: 11
230 moves: 24	coalesceable: 16	coalesced: 16
231 moves: 17	coalesceable: 11	coalesced: 11
232 moves: 17	coalesceable: 11	coalesced: 11
233 moves: 17	coalesceable: 11	coalesced: 11
234 moves: 17	coalesceable: 11	coalesced: 11
235 moves: 17	coalesceable: 11	coalesced: 11
236 moves: 17	coalesceable: 11	coalesced: 11
237 moves: 17	coalesceable: 11	coalesced: 11
238 moves: 17	coalesceable: 11	coalesced: 11
239 moves: 17	coalesceable: 11	coalesced: 11
240 moves: 17	coalesceable: 11	coalesced: 11
241 moves: 2312	coalesceable: 1286	coalesced: 1286
242 moves: 17	coalesceable: 11	coalesced: 11
243 moves: 17	coalesceable: 11	coalesced: 11
244 moves: 17	coalesceable: 11	coalesced: 11
245 moves: 17	coalesceable: 11	coalesced: 11
246 moves: 17	coalesceable: 11	coalesced: 11
247 moves: 74	coalesceable: 49	coalesced: 43
248 moves: 17	coalesceable: 11	coalesced: 11
249 moves: 17	coalesceable: 11	coalesced: 11
250 moves: 17	coalesceable: 11	coalesced: 11
251 moves: 17	coalesceable: 11	coalesced: 11
252 moves: 17	coalesceable: 11	coalesced: 11
253 moves: 17	coalesceable: 11	coalesced: 11
254 moves: 17	coalesceable: 11	coalesced: 11
255 moves: 17	coalesceable: 11	coalesced: 11
256 moves: 17	coalesceable: 11	coalesced: 11
257 moves: 17	coalesceable: 11	coalesced: 11
258 moves: 17	coalesceable: 11	coalesced: 11
259 moves: 17	coalesceable: 11	coalesced: 11
260 moves: 17	coalesceable: 11	coalesced: 11
261 moves: 17	coalesceable: 11	coalesced: 11
262 moves: 5885	coalesceable: 3532	coalesced: 3033
263 moves: 11474	coalesceable: 7187	coalesced: 6357
264 moves: 10448	coalesceable: 6311	coalesced: 5527
265 moves: 17	coalesceable: 11	coalesced: 11
266 moves: 17	coalesceable: 11	coalesced: 11
267 moves: 17	coalesceable: 11	coalesced: 11
268 moves: 17	coalesceable: 11	coalesced: 11
269 moves: 17	coalesceable: 11	coalesced: 11
270 moves: 17	coalesceable: 11	coalesced: 11
271 moves: 17	coalesceable: 11	coalesced: 11
272 moves: 17	coalesceable: 11	coalesced: 11
273 moves: 17	coalesceable: 11	coalesced: 11
274 moves: 17	coalesceable: 11	coalesced: 11
275 moves: 17	coalesceable: 11	coalesced: 11
276 moves: 102	coalesceable: 58	coalesced: 58
277 moves: 17	coalesceable: 11	coalesced: 11
278 moves: 17	coalesceable: 11	coalesced: 11
279 moves: 17	coalesceable: 11	coalesced: 11
280 moves: 17	coalesceable: 11	coalesced: 11
281 moves: 17	coalesceable: 11	coalesced: 11
282 moves: 17	coalesceable: 11	coalesced: 11
283 moves: 1828	coalesceable: 1001	coalesced: 913
284 moves: 17	coalesceable: 11	coalesced: 11
285 moves: 17	coalesceable: 11	coalesced: 11
286 moves: 17	coalesceable: 11	coalesced: 11
287 moves: 17	coalesceable: 11	coalesced: 11
288 moves: 17	coalesceable: 11	coalesced: 11
289 moves: 158	coalesceable: 117	coalesced: 117
290 moves: 17	coalesceable: 11	coalesced: 11
291 moves: 17	coalesceable: 11	coalesced: 11
292 moves: 17	coalesceable: 11	coalesced: 11
293 moves: 17	coalesceable: 11	coalesced: 11
294 moves: 5	coalesceable: 3	coalesced: 3
295 moves: 4	coalesceable: 4	coalesced: 4
296 moves: 6	coalesceable: 6	coalesced: 6
297 moves: 4	coalesceable: 4	coalesced: 4
298 moves: 6	coalesceable: 6	coalesced: 6
299 moves: 8	coalesceable: 8	coalesced: 8
300 moves: 46	coalesceable: 34	coalesced: 33
301 moves: 4	coalesceable: 4	coalesced: 4
302 moves: 3	coalesceable: 3	coalesced: 3
303 moves: 6	coalesceable: 6	coalesced: 6
304 moves: 3	coalesceable: 3	coalesced: 2
305 moves: 8	coalesceable: 8	coalesced: 8
306 moves: 99	coalesceable: 63	coalesced: 50
307 moves: 6	coalesceable: 6	coalesced: 6
308 moves: 7	coalesceable: 7	coalesced: 4
309 moves: 6	coalesceable: 6	coalesced: 6
310 moves: 29	coalesceable: 19	coalesced: 13
311 moves: 8	coalesceable: 8	coalesced: 8
312 moves: 103	coalesceable: 64	coalesced: 59
313 moves: 4	coalesceable: 4	coalesced: 4
314 moves: 7	coalesceable: 7	coalesced: 7
315 moves: 6	coalesceable: 6	coalesced: 6
316 moves: 49	coalesceable: 36	coalesced: 34
317 moves: 6	coalesceable: 6	coalesced: 6
318 moves: 32	coalesceable: 23	coalesced: 18
319 moves: 4	coalesceable: 4	coalesced: 4
320 moves: 5	coalesceable: 5	coalesced: 3
321 moves: 4	coalesceable: 4	coalesced: 4
322 moves: 7	coalesceable: 7	coalesced: 7
323 moves: 6	coalesceable: 6	coalesced: 6
324 moves: 86	coalesceable: 57	coalesced: 51
325 moves: 6	coalesceable: 6	coalesced: 6
326 moves: 76	coalesceable: 47	coalesced: 43
327 moves: 6	coalesceable: 6	coalesced: 6
328 moves: 42	coalesceable: 27	coalesced: 25
329 moves: 8	coalesceable: 8	coalesced: 8
330 moves: 52	coalesceable: 37	coalesced: 31
331 moves: 4	coalesceable: 4	coalesced: 4
332 moves: 95	coalesceable: 58	coalesced: 57
333 moves: 6	coalesceable: 6	coalesced: 6
334 moves: 49	coalesceable: 37	coalesced: 35
335 moves: 4	coalesceable: 4	coalesced: 4
336 moves: 73	coalesceable: 49	coalesced: 47
337 moves: 6	coalesceable: 6	coalesced: 6
338 moves: 79	coalesceable: 57	coalesced: 54
339 moves: 6	coalesceable: 6	coalesced: 6
340 moves: 42	coalesceable: 27	coalesced: 26
341 moves: 4	coalesceable: 4	coalesced: 4
342 moves: 12	coalesceable: 11	coalesced: 9
343 moves: 4	coalesceable: 4	coalesced: 4
344 moves: 9	coalesceable: 9	coalesced: 8
345 moves: 4	coalesceable: 4	coalesced: 4
346 moves: 29	coalesceable: 12	coalesced: 11
347 moves: 8	coalesceable: 8	coalesced: 8
348 moves: 124	coalesceable: 72	coalesced: 58
349 moves: 6	coalesceable: 6	coalesced: 6
350 moves: 62	coalesceable: 31	coalesced: 29
351 moves: 4	coalesceable: 4	coalesced: 4
352 moves: 48	coalesceable: 23	coalesced: 21
353 moves: 6	coalesceable: 6	coalesced: 6
354 moves: 23	coalesceable: 15	coalesced: 11
355 moves: 6	coalesceable: 6	coalesced: 6
356 moves: 23	coalesceable: 15	coalesced: 11
357 moves: 6	coalesceable: 6	coalesced: 6
358 moves: 30	coalesceable: 19	coalesced: 16
359 moves: 6	coalesceable: 6	coalesced: 6
360 moves: 29	coalesceable: 21	coalesced: 17
361 moves: 6	coalesceable: 6	coalesced: 6
362 moves: 24	coalesceable: 16	coalesced: 13
363 moves: 6	coalesceable: 6	coalesced: 6
364 moves: 24	coalesceable: 16	coalesced: 13
365 moves: 6	coalesceable: 6	coalesced: 6
366 moves: 30	coalesceable: 22	coalesced: 19
367 moves: 6	coalesceable: 6	coalesced: 6
368 moves: 60	coalesceable: 44	coalesced: 41
369 moves: 6	coalesceable: 6	coalesced: 6
370 moves: 62	coalesceable: 31	coalesced: 29
371 moves: 4	coalesceable: 4	coalesced: 4
372 moves: 3	coalesceable: 3	coalesced: 3
373 moves: 4	coalesceable: 4	coalesced: 4
374 moves: 43	coalesceable: 29	coalesced: 25
375 moves: 4	coalesceable: 4	coalesced: 4
376 moves: 25	coalesceable: 18	coalesced: 16
377 moves: 4	coalesceable: 4	coalesced: 4
378 moves: 3	coalesceable: 3	coalesced: 3
379 moves: 6	coalesceable: 6	coalesced: 6
380 moves: 36	coalesceable: 23	coalesced: 17
381 moves: 6	coalesceable: 6	coalesced: 6
382 moves: 21	coalesceable: 19	coalesced: 19
383 moves: 4	coalesceable: 4	coalesced: 4
384 moves: 9	coalesceable: 9	coalesced: 8
385 moves: 8	coalesceable: 8	coalesced: 8
386 moves: 22	coalesceable: 20	coalesced: 20
387 moves: 12	coalesceable: 12	coalesced: 12
388 moves: 218	coalesceable: 134	coalesced: 94
389 moves: 12	coalesceable: 12	coalesced: 12
390 moves: 218	coalesceable: 134	coalesced: 94
391 moves: 8	coalesceable: 8	coalesced: 8
392 moves: 124	coalesceable: 72	coalesced: 58
393 moves: 4	coalesceable: 4	coalesced: 4
394 moves: 77	coalesceable: 56	coalesced: 53
395 moves: 6	coalesceable: 6	coalesced: 6
396 moves: 110	coalesceable: 79	coalesced: 69
397 moves: 8	coalesceable: 8	coalesced: 8
398 moves: 407	coalesceable: 208	coalesced: 175
399 moves: 4	coalesceable: 4	coalesced: 4
400 moves: 56	coalesceable: 33	coalesced: 30
401 moves: 4	coalesceable: 4	coalesced: 4
402 moves: 8	coalesceable: 6	coalesced: 6
403 moves: 8	coalesceable: 8	coalesced: 8
404 moves: 163	coalesceable: 110	coalesced: 96
405 moves: 6	coalesceable: 6	coalesced: 6
406 moves: 114	coalesceable: 80	coalesced: 72
407 moves: 4	coalesceable: 4	coalesced: 4
408 moves: 6	coalesceable: 6	coalesced: 6
409 moves: 4	coalesceable: 4	coalesced: 4
410 moves: 6	coalesceable: 6	coalesced: 6
411 moves: 8	coalesceable: 8	coalesced: 8
412 moves: 128	coalesceable: 77	coalesced: 70
413 moves: 8	coalesceable: 8	coalesced: 8
414 moves: 111	coalesceable: 66	coalesced: 51
415 moves: 6	coalesceable: 6	coalesced: 6
416 moves: 427	coalesceable: 263	coalesced: 198
417 moves: 4	coalesceable: 4	coalesced: 4
418 moves: 5	coalesceable: 5	coalesced: 5
419 moves: 4	coalesceable: 4	coalesced: 4
420 moves: 272	coalesceable: 139	coalesced: 131
421 moves: 4	coalesceable: 4	coalesced: 4
422 moves: 69	coalesceable: 54	coalesced: 54
423 moves: 6	coalesceable: 6	coalesced: 6
424 moves: 78	coalesceable: 59	coalesced: 56
425 moves: 4	coalesceable: 4	coalesced: 4
426 moves: 21	coalesceable: 18	coalesced: 16
427 moves: 4	coalesceable: 4	coalesced: 4
428 moves: 164	coalesceable: 106	coalesced: 89
429 moves: 224	coalesceable: 137	coalesced: 113
430 moves: 217	coalesceable: 133	coalesced: 108
431 moves: 4	coalesceable: 4	coalesced: 4
432 moves: 45	coalesceable: 26	coalesced: 24
433 moves: 6	coalesceable: 6	coalesced: 6
434 moves: 152	coalesceable: 102	coalesced: 97
435 moves: 6	coalesceable: 6	coalesced: 6
436 moves: 847	coalesceable: 556	coalesced: 502
437 moves: 6	coalesceable: 6	coalesced: 6
438 moves: 30	coalesceable: 21	coalesced: 16
439 moves: 4	coalesceable: 4	coalesced: 4
440 moves: 7	coalesceable: 7	coalesced: 7
441 moves: 6	coalesceable: 6	coalesced: 6
442 moves: 30	coalesceable: 17	coalesced: 16
443 moves: 10	coalesceable: 10	coalesced: 10
444 moves: 2844	coalesceable: 1470	coalesced: 781
445 moves: 10	coalesceable: 10	coalesced: 10
446 moves: 2803	coalesceable: 1454	coalesced: 770
447 moves: 4	coalesceable: 4	coalesced: 4
448 moves: 150	coalesceable: 86	coalesced: 76
449 moves: 4	coalesceable: 4	coalesced: 4
450 moves: 4	coalesceable: 4	coalesced: 4
451 moves: 8	coalesceable: 8	coalesced: 8
452 moves: 99	coalesceable: 63	coalesced: 57
453 moves: 8	coalesceable: 8	coalesced: 8
454 moves: 72	coalesceable: 48	coalesced: 44
455 moves: 10	coalesceable: 10	coalesced: 10
456 moves: 195	coalesceable: 104	coalesced: 68
457 moves: 8	coalesceable: 8	coalesced: 8
458 moves: 74	coalesceable: 47	coalesced: 43
459 moves: 6	coalesceable: 6	coalesced: 6
460 moves: 58	coalesceable: 40	coalesced: 33
461 moves: 6	coalesceable: 6	coalesced: 6
462 moves: 634	coalesceable: 440	coalesced: 316
463 moves: 6	coalesceable: 6	coalesced: 6
464 moves: 15	coalesceable: 15	coalesced: 15
465 moves: 4	coalesceable: 4	coalesced: 4
466 moves: 321	coalesceable: 204	coalesced: 200
467 moves: 8	coalesceable: 8	coalesced: 8
468 moves: 107	coalesceable: 65	coalesced: 65
469 moves: 10	coalesceable: 10	coalesced: 10
470 moves: 514	coalesceable: 292	coalesced: 271
471 moves: 4	coalesceable: 4	coalesced: 4
472 moves: 26	coalesceable: 19	coalesced: 17
473 moves: 8	coalesceable: 8	coalesced: 8
474 moves: 256	coalesceable: 149	coalesced: 130
475 moves: 8	coalesceable: 8	coalesced: 8
476 moves: 789	coalesceable: 475	coalesced: 427
477 moves: 6	coalesceable: 6	coalesced: 6
478 moves: 37	coalesceable: 23	coalesced: 22
479 moves: 4	coalesceable: 4	coalesced: 4
480 moves: 201	coalesceable: 119	coalesced: 113
481 moves: 6	coalesceable: 6	coalesced: 6
482 moves: 220	coalesceable: 158	coalesced: 129
483 moves: 4	coalesceable: 4	coalesced: 4
484 moves: 477	coalesceable: 295	coalesced: 290
485 moves: 6	coalesceable: 6	coalesced: 6
486 moves: 16	coalesceable: 9	coalesced: 6
487 moves: 6	coalesceable: 6	coalesced: 6
488 moves: 42	coalesceable: 26	coalesced: 25
489 moves: 4	coalesceable: 4	coalesced: 4
490 moves: 208	coalesceable: 121	coalesced: 117
491 moves: 4	coalesceable: 4	coalesced: 4
492 moves: 419	coalesceable: 260	coalesced: 230
493 moves: 4	coalesceable: 4	coalesced: 4
494 moves: 21	coalesceable: 14	coalesced: 13
495 moves: 6	coalesceable: 6	coalesced: 6
496 moves: 188	coalesceable: 117	coalesced: 112
497 moves: 6	coalesceable: 6	coalesced: 6
498 moves: 161	coalesceable: 117	coalesced: 95
499 moves: 4	coalesceable: 4	coalesced: 4
500 moves: 156	coalesceable: 103	coalesced: 98
501 moves: 4	coalesceable: 4	coalesced: 4
502 moves: 138	coalesceable: 92	coalesced: 88
503 moves: 4	coalesceable: 4	coalesced: 4
504 moves: 4	coalesceable: 4	coalesced: 4
505 moves: 4	coalesceable: 4	coalesced: 4
506 moves: 100	coalesceable: 64	coalesced: 61
507 moves: 6	coalesceable: 6	coalesced: 6
508 moves: 7	coalesceable: 7	coalesced: 7
509 moves: 10	coalesceable: 10	coalesced: 10
510 moves: 70	coalesceable: 61	coalesced: 55
511 moves: 4	coalesceable: 4	coalesced: 4
512 moves: 174	coalesceable: 110	coalesced: 105
513 moves: 4	coalesceable: 4	coalesced: 4
514 moves: 23	coalesceable: 15	coalesced: 14
515 moves: 9	coalesceable: 9	coalesced: 9
516 moves: 6	coalesceable: 6	coalesced: 6
517 moves: 232	coalesceable: 126	coalesced: 117
518 moves: 37	coalesceable: 23	coalesced: 20
519 moves: 4	coalesceable: 4	coalesced: 4
520 moves: 25	coalesceable: 16	coalesced: 14
521 moves: 10	coalesceable: 10	coalesced: 10
522 moves: 224	coalesceable: 128	coalesced: 94
523 moves: 8	coalesceable: 8	coalesced: 8
524 moves: 282	coalesceable: 163	coalesced: 151
525 moves: 6	coalesceable: 6	coalesced: 6
526 moves: 8	coalesceable: 8	coalesced: 6
527 moves: 6	coalesceable: 6	coalesced: 6
528 moves: 11	coalesceable: 11	coalesced: 9
529 moves: 10	coalesceable: 10	coalesced: 10
530 moves: 405	coalesceable: 209	coalesced: 162
531 moves: 10	coalesceable: 10	coalesced: 10
532 moves: 1186	coalesceable: 706	coalesced: 410
533 moves: 10	coalesceable: 10	coalesced: 10
534 moves: 96	coalesceable: 62	coalesced: 53
535 moves: 6	coalesceable: 6	coalesced: 6
536 moves: 24	coalesceable: 16	coalesced: 13
537 moves: 4	coalesceable: 4	coalesced: 4
538 moves: 36	coalesceable: 24	coalesced: 23
539 moves: 6	coalesceable: 6	coalesced: 6
540 moves: 24	coalesceable: 16	coalesced: 13
541 moves: 4	coalesceable: 4	coalesced: 4
542 moves: 147	coalesceable: 73	coalesced: 54
543 moves: 4	coalesceable: 4	coalesced: 4
544 moves: 89	coalesceable: 54	coalesced: 47
545 moves: 4	coalesceable: 4	coalesced: 4
546 moves: 22	coalesceable: 14	coalesced: 13
547 moves: 6	coalesceable: 6	coalesced: 6
548 moves: 40	coalesceable: 23	coalesced: 19
549 moves: 8	coalesceable: 8	coalesced: 8
550 moves: 64	coalesceable: 35	coalesced: 33
551 moves: 6	coalesceable: 6	coalesced: 6
552 moves: 24	coalesceable: 16	coalesced: 13
553 moves: 4	coalesceable: 4	coalesced: 4
554 moves: 59	coalesceable: 34	coalesced: 31
555 moves: 4	coalesceable: 4	coalesced: 4
556 moves: 252	coalesceable: 137	coalesced: 115
557 moves: 4	coalesceable: 4	coalesced: 4
558 moves: 18	coalesceable: 10	coalesced: 10
559 moves: 6	coalesceable: 6	coalesced: 6
560 moves: 148	coalesceable: 60	coalesced: 56
561 moves: 4	coalesceable: 4	coalesced: 4
562 moves: 6	coalesceable: 6	coalesced: 6
563 moves: 4	coalesceable: 4	coalesced: 4
564 moves: 6	coalesceable: 6	coalesced: 6
565 moves: 6	coalesceable: 6	coalesced: 6
566 moves: 86	coalesceable: 55	coalesced: 53
567 moves: 6	coalesceable: 6	coalesced: 6
568 moves: 77	coalesceable: 49	coalesced: 44
569 moves: 4	coalesceable: 4	coalesced: 4
570 moves: 21	coalesceable: 14	coalesced: 13
571 moves: 4	coalesceable: 4	coalesced: 4
572 moves: 21	coalesceable: 14	coalesced: 13
573 moves: 1595	coalesceable: 918	coalesced: 834
574 moves: 4	coalesceable: 4	coalesced: 4
575 moves: 10	coalesceable: 9	coalesced: 9
576 moves: 6	coalesceable: 6	coalesced: 6
577 moves: 40	coalesceable: 25	coalesced: 24
578 moves: 14	coalesceable: 14	coalesced: 14
579 moves: 79	coalesceable: 47	coalesced: 41
580 moves: 4	coalesceable: 4	coalesced: 4
581 moves: 18	coalesceable: 16	coalesced: 16
582 moves: 4	coalesceable: 4	coalesced: 4
583 moves: 158	coalesceable: 90	coalesced: 87
584 moves: 4	coalesceable: 4	coalesced: 4
585 moves: 111	coalesceable: 80	coalesced: 77
586 moves: 4	coalesceable: 4	coalesced: 4
587 moves: 30	coalesceable: 19	coalesced: 18
588 moves: 4	coalesceable: 4	coalesced: 4
589 moves: 17	coalesceable: 15	coalesced: 15
590 moves: 4	coalesceable: 4	coalesced: 4
591 moves: 12	coalesceable: 11	coalesced: 11
592 moves: 4	coalesceable: 4	coalesced: 4
593 moves: 69	coalesceable: 40	coalesced: 39
594 moves: 6	coalesceable: 6	coalesced: 6
595 moves: 3	coalesceable: 3	coalesced: 2
596 moves: 6	coalesceable: 6	coalesced: 6
597 moves: 37	coalesceable: 22	coalesced: 21
598 moves: 6	coalesceable: 6	coalesced: 6
599 moves: 3	coalesceable: 3	coalesced: 3
600 moves: 6	coalesceable: 6	coalesced: 6
601 moves: 37	coalesceable: 22	coalesced: 21
602 moves: 4	coalesceable: 4	coalesced: 4
603 moves: 55	coalesceable: 35	coalesced: 31
604 moves: 6	coalesceable: 6	coalesced: 6
605 moves: 23	coalesceable: 21	coalesced: 21
606 moves: 4	coalesceable: 4	coalesced: 4
607 moves: 25	coalesceable: 17	coalesced: 16
608 moves: 4	coalesceable: 4	coalesced: 4
609 moves: 77	coalesceable: 51	coalesced: 48
610 moves: 6	coalesceable: 6	coalesced: 6
611 moves: 20	coalesceable: 18	coalesced: 14
612 moves: 38	coalesceable: 25	coalesced: 24
613 moves: 79	coalesceable: 50	coalesced: 47
614 moves: 6	coalesceable: 6	coalesced: 6
615 moves: 85	coalesceable: 57	coalesced: 54
616 moves: 4	coalesceable: 4	coalesced: 4
617 moves: 40	coalesceable: 25	coalesced: 24
618 moves: 6	coalesceable: 6	coalesced: 6
619 moves: 26	coalesceable: 19	coalesced: 19
620 moves: 4	coalesceable: 4	coalesced: 4
621 moves: 21	coalesceable: 14	coalesced: 13
622 moves: 4	coalesceable: 4	coalesced: 4
623 moves: 53	coalesceable: 34	coalesced: 32
624 moves: 167	coalesceable: 107	coalesced: 107
625 moves: 37	coalesceable: 26	coalesced: 25
626 moves: 6	coalesceable: 6	coalesced: 6
627 moves: 34	coalesceable: 23	coalesced: 21
628 moves: 4	coalesceable: 4	coalesced: 4
629 moves: 5	coalesceable: 5	coalesced: 5
630 moves: 38	coalesceable: 25	coalesced: 24
631 moves: 110	coalesceable: 74	coalesced: 72
632 moves: 6	coalesceable: 6	coalesced: 6
633 moves: 34	coalesceable: 23	coalesced: 21
634 moves: 32	coalesceable: 22	coalesced: 22
635 moves: 102	coalesceable: 69	coalesced: 67
636 moves: 6	coalesceable: 6	coalesced: 6
637 moves: 34	coalesceable: 23	coalesced: 21
638 moves: 4	coalesceable: 4	coalesced: 4
639 moves: 5	coalesceable: 5	coalesced: 5
640 moves: 4	coalesceable: 4	coalesced: 4
641 moves: 21	coalesceable: 14	coalesced: 13
642 moves: 4	coalesceable: 4	coalesced: 4
643 moves: 132	coalesceable: 89	coalesced: 80
644 moves: 4	coalesceable: 4	coalesced: 4
645 moves: 88	coalesceable: 59	coalesced: 56
646 moves: 4	coalesceable: 4	coalesced: 4
647 moves: 29	coalesceable: 23	coalesced: 21
648 moves: 4	coalesceable: 4	coalesced: 4
649 moves: 49	coalesceable: 37	coalesced: 37
650 moves: 4	coalesceable: 4	coalesced: 4
651 moves: 5	coalesceable: 5	coalesced: 5
652 moves: 4	coalesceable: 4	coalesced: 4
653 moves: 49	coalesceable: 37	coalesced: 37
654 moves: 4	coalesceable: 4	coalesced: 4
655 moves: 5	coalesceable: 5	coalesced: 5
656 moves: 4	coalesceable: 4	coalesced: 4
657 moves: 5	coalesceable: 5	coalesced: 5
658 moves: 4	coalesceable: 4	coalesced: 4
659 moves: 5	coalesceable: 5	coalesced: 5
660 moves: 4	coalesceable: 4	coalesced: 4
661 moves: 5	coalesceable: 5	coalesced: 5
662 moves: 4	coalesceable: 4	coalesced: 4
663 moves: 5	coalesceable: 5	coalesced: 5
664 moves: 4	coalesceable: 4	coalesced: 4
665 moves: 5	coalesceable: 5	coalesced: 5
666 moves: 4	coalesceable: 4	coalesced: 4
667 moves: 51	coalesceable: 29	coalesced: 28
668 moves: 4	coalesceable: 4	coalesced: 4
669 moves: 108	coalesceable: 74	coalesced: 72
670 moves: 8	coalesceable: 8	coalesced: 8
671 moves: 99	coalesceable: 51	coalesced: 48
672 moves: 4	coalesceable: 4	coalesced: 4
673 moves: 266	coalesceable: 170	coalesced: 166
674 moves: 6	coalesceable: 6	coalesced: 6
675 moves: 503	coalesceable: 392	coalesced: 384
676 moves: 125	coalesceable: 50	coalesced: 45
677 moves: 4	coalesceable: 4	coalesced: 4
678 moves: 210	coalesceable: 128	coalesced: 124
679 moves: 6	coalesceable: 6	coalesced: 6
680 moves: 14	coalesceable: 12	coalesced: 12
681 moves: 6	coalesceable: 6	coalesced: 6
682 moves: 35	coalesceable: 25	coalesced: 22
683 moves: 38	coalesceable: 28	coalesced: 23
684 moves: 4	coalesceable: 4	coalesced: 4
685 moves: 302	coalesceable: 186	coalesced: 181

runtime: 6m22s,    gctime: 5.0s,     systime: 0.36490s.
        external oracle real: 6m23s
        external oracle size: 552987
     apply colour (par) eval: runtime: 7m08s,    gctime: 19.3s,     systime: 2.6s.
     apply colour (par) real: 2m31s
     apply colour (par) size: 2110074
           check colour eval: runtime: 20.9s,    gctime: 5.1s,     systime: 0.82880s.
           check colour real: 21.8s
           check colour size: 2110761
          word_to_stack eval: runtime: 2m59s,    gctime: 3.1s,     systime: 0.48039s.
          word_to_stack real: 3m00s
          word_to_stack size: 1648117
          stack_rawcall eval: runtime: 1m54s,    gctime: 1.8s,     systime: 0.19617s.
          stack_rawcall real: 1m54s
          stack_rawcall size: 1635100
      stack_alloc (par) eval: runtime: 3m12s,    gctime: 2.2s,     systime: 0.35772s.
      stack_alloc (par) real: 1m00s
      stack_alloc (par) size: 1650958
expand stack_remove_def eval: runtime: 0.03610s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03603s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 4m02s,    gctime: 3.0s,     systime: 0.53263s.
     stack_remove (par) real: 1m05s
     stack_remove (par) size: 2710987
      stack_names (par) eval: runtime: 2m14s,    gctime: 3.3s,     systime: 0.35511s.
      stack_names (par) real: 44.2s
      stack_names (par) size: 2801809
     stack_to_lab (par) eval: runtime: 5m03s,    gctime: 31.3s,     systime: 2.2s.
     stack_to_lab (par) real: 1m55s
     stack_to_lab (par) size: 3422428
          lab_to_target eval: runtime: 8m05s,    gctime: 19.3s,     systime: 2.7s.
          lab_to_target real: 8m08s
          lab_to_target size: 5117408
                      export: runtime: 0.95898s,    gctime: 0.26061s,     systime: 0.02896s.
Saved theorem _____ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 59m58s to build
cc grep.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o  -o cake_grep
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "helloCompile">>
                to_flat eval: runtime: 6.8s,    gctime: 0.39318s,     systime: 0.05387s.
                to_flat real: 6.9s
                to_flat size: 56823
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.23215s,    gctime: 0.05153s,     systime: 0.00597s.
                to_clos real: 0.23857s
                to_clos size: 33725
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 3.8s,    gctime: 0.16997s,     systime: 0.01102s.
                 to_bvl real: 3.8s
                 to_bvl size: 55296
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 32.8s,    gctime: 0.47886s,     systime: 0.04401s.
                 to_bvi real: 32.9s
                 to_bvi size: 63033
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 10.5s,    gctime: 0.51793s,     systime: 0.03697s.
                to_data real: 10.6s
                to_data size: 111238
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 14.4s,    gctime: 0.61943s,     systime: 0.04593s.
           data_to_word real: 14.5s
           data_to_word size: 296757
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m02s,    gctime: 4.0s,     systime: 0.31865s.
 inst,ssa,two-reg (par) real: 33.7s
 inst,ssa,two-reg (par) size: 1199208
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 12.8s,    gctime: 6.7s,     systime: 0.83254s.
        get_clash (par) real: 10.1s
        get_clash (par) size: 1867589
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 934	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 11	coalesced: 11
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 4375	coalesceable: 2573	coalesced: 2573
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 17	coalesceable: 11	coalesced: 11
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 17	coalesceable: 11	coalesced: 11
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 10	coalesceable: 6	coalesced: 6
137 moves: 60	coalesceable: 41	coalesced: 40
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 2	coalesceable: 2	coalesced: 2
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 5	coalesceable: 3	coalesced: 3
145 moves: 4	coalesceable: 4	coalesced: 4
146 moves: 9	coalesceable: 9	coalesced: 8
147 moves: 8	coalesceable: 8	coalesced: 8
148 moves: 124	coalesceable: 72	coalesced: 58
149 moves: 6	coalesceable: 6	coalesced: 6
150 moves: 23	coalesceable: 15	coalesced: 11
151 moves: 6	coalesceable: 6	coalesced: 6
152 moves: 23	coalesceable: 15	coalesced: 11
153 moves: 6	coalesceable: 6	coalesced: 6
154 moves: 30	coalesceable: 19	coalesced: 16
155 moves: 6	coalesceable: 6	coalesced: 6
156 moves: 29	coalesceable: 21	coalesced: 17
157 moves: 6	coalesceable: 6	coalesced: 6
158 moves: 24	coalesceable: 16	coalesced: 13
159 moves: 6	coalesceable: 6	coalesced: 6
160 moves: 24	coalesceable: 16	coalesced: 13
161 moves: 6	coalesceable: 6	coalesced: 6
162 moves: 30	coalesceable: 22	coalesced: 19
163 moves: 4	coalesceable: 4	coalesced: 4
164 moves: 25	coalesceable: 18	coalesced: 16
165 moves: 4	coalesceable: 4	coalesced: 4
166 moves: 3	coalesceable: 3	coalesced: 3
167 moves: 6	coalesceable: 6	coalesced: 6
168 moves: 21	coalesceable: 19	coalesced: 19
169 moves: 8	coalesceable: 8	coalesced: 8
170 moves: 22	coalesceable: 20	coalesced: 20
171 moves: 12	coalesceable: 12	coalesced: 12
172 moves: 218	coalesceable: 134	coalesced: 94
173 moves: 8	coalesceable: 8	coalesced: 8
174 moves: 163	coalesceable: 110	coalesced: 96
175 moves: 6	coalesceable: 6	coalesced: 6
176 moves: 114	coalesceable: 80	coalesced: 72
177 moves: 4	coalesceable: 4	coalesced: 4
178 moves: 6	coalesceable: 6	coalesced: 6
179 moves: 8	coalesceable: 8	coalesced: 8
180 moves: 128	coalesceable: 77	coalesced: 70
181 moves: 8	coalesceable: 8	coalesced: 8
182 moves: 111	coalesceable: 66	coalesced: 51
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 427	coalesceable: 263	coalesced: 198
185 moves: 4	coalesceable: 4	coalesced: 4
186 moves: 5	coalesceable: 5	coalesced: 5
187 moves: 4	coalesceable: 4	coalesced: 4
188 moves: 64	coalesceable: 47	coalesced: 47

runtime: 8.9s,    gctime: 0.02193s,     systime: 0.04590s.
        external oracle real: 9.0s
        external oracle size: 133870
     apply colour (par) eval: runtime: 1m14s,    gctime: 1.8s,     systime: 0.72928s.
     apply colour (par) real: 45.8s
     apply colour (par) size: 592770
           check colour eval: runtime: 0.88733s,    gctime: 0.00000s,     systime: 0.00000s.
           check colour real: 0.88881s
           check colour size: 592960
          word_to_stack eval: runtime: 59.0s,    gctime: 0.95471s,     systime: 0.12468s.
          word_to_stack real: 59.2s
          word_to_stack size: 487197
          stack_rawcall eval: runtime: 33.6s,    gctime: 0.36369s,     systime: 0.04888s.
          stack_rawcall real: 33.7s
          stack_rawcall size: 481116
      stack_alloc (par) eval: runtime: 44.8s,    gctime: 0.59542s,     systime: 0.09193s.
      stack_alloc (par) real: 22.8s
      stack_alloc (par) size: 482377
expand stack_remove_def eval: runtime: 0.03411s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03418s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m00s,    gctime: 0.70774s,     systime: 0.08865s.
     stack_remove (par) real: 35.3s
     stack_remove (par) size: 826411
      stack_names (par) eval: runtime: 31.7s,    gctime: 0.66482s,     systime: 0.06288s.
      stack_names (par) real: 16.3s
      stack_names (par) size: 852930
     stack_to_lab (par) eval: runtime: 1m04s,    gctime: 1.2s,     systime: 0.13589s.
     stack_to_lab (par) real: 32.9s
     stack_to_lab (par) size: 1035167
          lab_to_target eval: runtime: 3m18s,    gctime: 5.1s,     systime: 0.56482s.
          lab_to_target real: 3m19s
          lab_to_target size: 1656145
                      export: runtime: 0.38493s,    gctime: 0.00637s,     systime: 0.02596s.
Saved theorem _____ "hello_compiled"
Exporting theory "helloCompile" ... done.
Theory "helloCompile" took 12m23s to build
cc hello.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o  -o cake_hello
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
  val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "helloErrCompile">>
                to_flat eval: runtime: 6.6s,    gctime: 0.36687s,     systime: 0.21370s.
                to_flat real: 6.8s
                to_flat size: 57713
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.24417s,    gctime: 0.05660s,     systime: 0.02394s.
                to_clos real: 0.26860s
                to_clos size: 34220
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 3.7s,    gctime: 0.13065s,     systime: 0.01294s.
                 to_bvl real: 3.7s
                 to_bvl size: 56636
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 32.8s,    gctime: 0.24827s,     systime: 0.02679s.
                 to_bvi real: 32.9s
                 to_bvi size: 64310
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 10.1s,    gctime: 0.43435s,     systime: 0.04390s.
                to_data real: 10.1s
                to_data size: 112949
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 13.9s,    gctime: 0.44034s,     systime: 0.05091s.
           data_to_word real: 14.0s
           data_to_word size: 299804
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 59.5s,    gctime: 2.4s,     systime: 0.28287s.
 inst,ssa,two-reg (par) real: 31.0s
 inst,ssa,two-reg (par) size: 1207123
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 6.8s,    gctime: 0.98342s,     systime: 0.08598s.
        get_clash (par) real: 3.8s
        get_clash (par) size: 1878430
        external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75	coalesceable: 61	coalesced: 53
1 moves: 24	coalesceable: 22	coalesced: 20
2 moves: 90	coalesceable: 68	coalesced: 53
3 moves: 25	coalesceable: 19	coalesced: 17
4 moves: 16	coalesceable: 15	coalesced: 12
5 moves: 148	coalesceable: 116	coalesced: 110
6 moves: 7	coalesceable: 7	coalesced: 7
7 moves: 7	coalesceable: 7	coalesced: 7
8 moves: 7	coalesceable: 7	coalesced: 7
9 moves: 7	coalesceable: 7	coalesced: 7
10 moves: 7	coalesceable: 7	coalesced: 7
11 moves: 19	coalesceable: 17	coalesced: 12
12 moves: 47	coalesceable: 41	coalesced: 37
13 moves: 31	coalesceable: 20	coalesced: 17
14 moves: 58	coalesceable: 48	coalesced: 42
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 10	coalesceable: 8	coalesced: 5
17 moves: 11	coalesceable: 6	coalesced: 6
18 moves: 21	coalesceable: 20	coalesced: 20
19 moves: 22	coalesceable: 21	coalesced: 20
20 moves: 19	coalesceable: 15	coalesced: 15
21 moves: 35	coalesceable: 29	coalesced: 25
22 moves: 40	coalesceable: 34	coalesced: 33
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 19	coalesceable: 17	coalesced: 15
25 moves: 42	coalesceable: 38	coalesced: 29
26 moves: 20	coalesceable: 20	coalesced: 14
27 moves: 20	coalesceable: 20	coalesced: 10
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 316	coalesceable: 269	coalesced: 269
31 moves: 26	coalesceable: 23	coalesced: 23
32 moves: 24	coalesceable: 23	coalesced: 23
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 90	coalesceable: 81	coalesced: 81
36 moves: 85	coalesceable: 82	coalesced: 82
37 moves: 65	coalesceable: 62	coalesced: 62
38 moves: 88	coalesceable: 85	coalesced: 85
39 moves: 29	coalesceable: 26	coalesced: 26
40 moves: 48	coalesceable: 45	coalesced: 45
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 21	coalesceable: 18	coalesced: 18
45 moves: 51	coalesceable: 48	coalesced: 48
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 22	coalesceable: 19	coalesced: 19
49 moves: 26	coalesceable: 23	coalesced: 23
50 moves: 15	coalesceable: 14	coalesced: 14
51 moves: 20	coalesceable: 17	coalesced: 17
52 moves: 24	coalesceable: 21	coalesced: 21
53 moves: 190	coalesceable: 117	coalesced: 103
54 moves: 92	coalesceable: 65	coalesced: 51
55 moves: 41	coalesceable: 26	coalesced: 25
56 moves: 35	coalesceable: 26	coalesced: 21
57 moves: 56	coalesceable: 42	coalesced: 36
58 moves: 71	coalesceable: 46	coalesced: 40
59 moves: 48	coalesceable: 37	coalesced: 32
60 moves: 71	coalesceable: 46	coalesced: 38
61 moves: 927	coalesceable: 603	coalesced: 410
62 moves: 1088	coalesceable: 687	coalesced: 404
63 moves: 1169	coalesceable: 725	coalesced: 434
64 moves: 1254	coalesceable: 765	coalesced: 434
65 moves: 1343	coalesceable: 807	coalesced: 407
66 moves: 1436	coalesceable: 851	coalesced: 420
67 moves: 1533	coalesceable: 897	coalesced: 459
68 moves: 1634	coalesceable: 943	coalesced: 482
69 moves: 1739	coalesceable: 989	coalesced: 504
70 moves: 1848	coalesceable: 1035	coalesced: 506
71 moves: 17	coalesceable: 15	coalesced: 15
72 moves: 19	coalesceable: 17	coalesced: 17
73 moves: 21	coalesceable: 18	coalesced: 17
74 moves: 21	coalesceable: 19	coalesced: 19
75 moves: 23	coalesceable: 20	coalesced: 19
76 moves: 25	coalesceable: 21	coalesced: 20
77 moves: 23	coalesceable: 21	coalesced: 21
78 moves: 25	coalesceable: 22	coalesced: 21
79 moves: 27	coalesceable: 23	coalesced: 22
80 moves: 29	coalesceable: 24	coalesced: 23
81 moves: 25	coalesceable: 23	coalesced: 19
82 moves: 27	coalesceable: 24	coalesced: 20
83 moves: 29	coalesceable: 25	coalesced: 21
84 moves: 31	coalesceable: 26	coalesced: 22
85 moves: 33	coalesceable: 27	coalesced: 23
86 moves: 27	coalesceable: 24	coalesced: 21
87 moves: 29	coalesceable: 25	coalesced: 22
88 moves: 31	coalesceable: 26	coalesced: 23
89 moves: 33	coalesceable: 27	coalesced: 24
90 moves: 35	coalesceable: 28	coalesced: 25
91 moves: 37	coalesceable: 29	coalesced: 26
92 moves: 29	coalesceable: 25	coalesced: 16
93 moves: 31	coalesceable: 26	coalesced: 18
94 moves: 33	coalesceable: 27	coalesced: 23
95 moves: 35	coalesceable: 28	coalesced: 21
96 moves: 37	coalesceable: 29	coalesced: 22
97 moves: 39	coalesceable: 30	coalesced: 23
98 moves: 41	coalesceable: 31	coalesced: 24
99 moves: 31	coalesceable: 25	coalesced: 12
100 moves: 33	coalesceable: 27	coalesced: 9
101 moves: 35	coalesceable: 28	coalesced: 16
102 moves: 37	coalesceable: 29	coalesced: 23
103 moves: 39	coalesceable: 30	coalesced: 23
104 moves: 41	coalesceable: 31	coalesced: 21
105 moves: 43	coalesceable: 32	coalesced: 22
106 moves: 45	coalesceable: 33	coalesced: 25
107 moves: 33	coalesceable: 25	coalesced: 14
108 moves: 35	coalesceable: 27	coalesced: 10
109 moves: 37	coalesceable: 29	coalesced: 11
110 moves: 39	coalesceable: 30	coalesced: 14
111 moves: 41	coalesceable: 31	coalesced: 21
112 moves: 43	coalesceable: 32	coalesced: 23
113 moves: 45	coalesceable: 33	coalesced: 23
114 moves: 47	coalesceable: 34	coalesced: 23
115 moves: 49	coalesceable: 35	coalesced: 25
116 moves: 62	coalesceable: 11	coalesced: 7
117 moves: 934	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 11	coalesced: 11
119 moves: 17	coalesceable: 11	coalesced: 11
120 moves: 17	coalesceable: 11	coalesced: 11
121 moves: 17	coalesceable: 11	coalesced: 11
122 moves: 17	coalesceable: 11	coalesced: 11
123 moves: 17	coalesceable: 11	coalesced: 11
124 moves: 17	coalesceable: 11	coalesced: 11
125 moves: 17	coalesceable: 11	coalesced: 11
126 moves: 17	coalesceable: 11	coalesced: 11
127 moves: 17	coalesceable: 11	coalesced: 11
128 moves: 17	coalesceable: 11	coalesced: 11
129 moves: 4375	coalesceable: 2573	coalesced: 2573
130 moves: 17	coalesceable: 11	coalesced: 11
131 moves: 17	coalesceable: 11	coalesced: 11
132 moves: 17	coalesceable: 11	coalesced: 11
133 moves: 17	coalesceable: 11	coalesced: 11
134 moves: 17	coalesceable: 11	coalesced: 11
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 17	coalesceable: 11	coalesced: 11
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 10	coalesceable: 6	coalesced: 6
139 moves: 60	coalesceable: 41	coalesced: 40
140 moves: 60	coalesceable: 41	coalesced: 40
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 2	coalesceable: 2	coalesced: 2
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 5	coalesceable: 3	coalesced: 3
148 moves: 4	coalesceable: 4	coalesced: 4
149 moves: 69	coalesceable: 44	coalesced: 38
150 moves: 4	coalesceable: 4	coalesced: 4
151 moves: 3	coalesceable: 3	coalesced: 3
152 moves: 4	coalesceable: 4	coalesced: 4
153 moves: 9	coalesceable: 9	coalesced: 8
154 moves: 8	coalesceable: 8	coalesced: 8
155 moves: 124	coalesceable: 72	coalesced: 58
156 moves: 6	coalesceable: 6	coalesced: 6
157 moves: 23	coalesceable: 15	coalesced: 11
158 moves: 6	coalesceable: 6	coalesced: 6
159 moves: 23	coalesceable: 15	coalesced: 11
160 moves: 6	coalesceable: 6	coalesced: 6
161 moves: 30	coalesceable: 19	coalesced: 16
162 moves: 6	coalesceable: 6	coalesced: 6
163 moves: 29	coalesceable: 21	coalesced: 17
164 moves: 6	coalesceable: 6	coalesced: 6
165 moves: 24	coalesceable: 16	coalesced: 13
166 moves: 6	coalesceable: 6	coalesced: 6
167 moves: 24	coalesceable: 16	coalesced: 13
168 moves: 6	coalesceable: 6	coalesced: 6
169 moves: 30	coalesceable: 22	coalesced: 19
170 moves: 4	coalesceable: 4	coalesced: 4
171 moves: 25	coalesceable: 18	coalesced: 16
172 moves: 4	coalesceable: 4	coalesced: 4
173 moves: 3	coalesceable: 3	coalesced: 3
174 moves: 6	coalesceable: 6	coalesced: 6
175 moves: 21	coalesceable: 19	coalesced: 19
176 moves: 8	coalesceable: 8	coalesced: 8
177 moves: 22	coalesceable: 20	coalesced: 20
178 moves: 12	coalesceable: 12	coalesced: 12
179 moves: 218	coalesceable: 134	coalesced: 94
180 moves: 8	coalesceable: 8	coalesced: 8
181 moves: 163	coalesceable: 110	coalesced: 96
182 moves: 6	coalesceable: 6	coalesced: 6
183 moves: 114	coalesceable: 80	coalesced: 72
184 moves: 4	coalesceable: 4	coalesced: 4
185 moves: 6	coalesceable: 6	coalesced: 6
186 moves: 8	coalesceable: 8	coalesced: 8
187 moves: 128	coalesceable: 77	coalesced: 70
188 moves: 8	coalesceable: 8	coalesced: 8
189 moves: 111	coalesceable: 66	coalesced: 51
190 moves: 6	coalesceable: 6	coalesced: 6
191 moves: 427	coalesceable: 263	coalesced: 198
192 moves: 4	coalesceable: 4	coalesced: 4
193 moves: 5	coalesceable: 5	coalesced: 5
194 moves: 4	coalesceable: 4	coalesced: 4
195 moves: 71	coalesceable: 51	coalesced: 51

runtime: 9.1s,    gctime: 0.09115s,     systime: 0.01094s.
        external oracle real: 9.1s
        external oracle size: 135006
     apply colour (par) eval: runtime: 1m20s,    gctime: 8.8s,     systime: 0.86696s.
     apply colour (par) real: 52.0s
     apply colour (par) size: 597855
           check colour eval: runtime: 1.0s,    gctime: 0.11515s,     systime: 0.00199s.
           check colour real: 1.0s
           check colour size: 598052
          word_to_stack eval: runtime: 57.3s,    gctime: 1.1s,     systime: 0.05956s.
          word_to_stack real: 57.5s
          word_to_stack size: 490894
          stack_rawcall eval: runtime: 33.8s,    gctime: 0.42785s,     systime: 0.02682s.
          stack_rawcall real: 33.8s
          stack_rawcall size: 484724
      stack_alloc (par) eval: runtime: 44.6s,    gctime: 0.46708s,     systime: 0.03092s.
      stack_alloc (par) real: 22.4s
      stack_alloc (par) size: 486045
expand stack_remove_def eval: runtime: 0.03374s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03383s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 59.5s,    gctime: 0.84219s,     systime: 0.08884s.
     stack_remove (par) real: 34.4s
     stack_remove (par) size: 831882
      stack_names (par) eval: runtime: 31.7s,    gctime: 0.69986s,     systime: 0.06091s.
      stack_names (par) real: 16.1s
      stack_names (par) size: 858623
     stack_to_lab (par) eval: runtime: 1m03s,    gctime: 1.3s,     systime: 0.14179s.
     stack_to_lab (par) real: 32.2s
     stack_to_lab (par) size: 1042262
          lab_to_target eval: runtime: 3m13s,    gctime: 6.4s,     systime: 0.55978s.
          lab_to_target real: 3m14s
          lab_to_target size: 1667906
                      export: runtime: 0.48073s,    gctime: 0.07626s,     systime: 0.02197s.
Saved theorem _____ "helloErr_compiled"
Exporting theory "helloErrCompile" ... Run out of store - interrupting threads

Failure while writing theory!
error in quse /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript.sml : Interrupt
error in load /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript : Interrupt
Uncaught exception: Interrupt
Failed script build for /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript - exited with code 1