Job 1635

CakeML:13eb6f5aa6a5bb9c159b02dfa1cc8c1d7bfc4d3a
  Fix a mistake [Nov 09 13:44:27]
#842 (ramsey)
Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5
  Merge pull request #843 from CakeML/newline-fix [Nov 13 19:24:32]
HOL:7e1cdab63fa78a67a3fabc28a9f2a909e65b6921
  Make RPROD (and PAIR_REL and ###) more polymorphic [Nov 12 10:36:34]
Machine:oven3 4.19.67.1.amd64-smp

Nov 14 09:56:09 Claimed job
Nov 14 09:56:30 Building HOL
Nov 14 10:16:05 Starting developers
Nov 14 10:16:14 Finished developers                                               8s  98MB
Nov 14 10:16:14 Starting developers/bin
Nov 14 10:16:27 Finished developers/bin                                          12s   1GB
Nov 14 10:16:27 Starting semantics/ffi
Nov 14 10:16:53 Finished semantics/ffi                                           25s 257MB
Nov 14 10:16:53 Starting semantics
Nov 14 10:20:07 Finished semantics                                             3m13s   1GB
Nov 14 10:20:08 Starting semantics/proofs
Nov 14 10:28:17 Finished semantics/proofs                                      8m08s   1GB
Nov 14 10:28:17 Starting semantics/alt_semantics
Nov 14 10:28:40 Finished semantics/alt_semantics                                 22s 444MB
Nov 14 10:28:40 Starting semantics/alt_semantics/proofs
Nov 14 10:34:05 Finished semantics/alt_semantics/proofs                        5m24s 994MB
Nov 14 10:34:05 Starting basis/pure
Nov 14 10:40:12 Finished basis/pure                                            6m05s 886MB
Nov 14 10:40:13 Starting translator
Nov 14 10:47:22 Finished translator                                            7m08s   1GB
Nov 14 10:47:22 Starting compiler/parsing
Nov 14 10:50:00 Finished compiler/parsing                                      2m38s   3GB
Nov 14 10:50:01 Starting characteristic
Nov 14 11:02:09 Finished characteristic                                       12m08s   2GB
Nov 14 11:02:10 Starting translator/monadic
Nov 14 11:05:40 Finished translator/monadic                                    3m30s   1GB
Nov 14 11:05:40 Starting basis
Nov 14 12:47:18 Finished basis                                              1h41m37s  16GB
Nov 14 12:47:19 Starting compiler/inference
Nov 14 12:50:03 Finished compiler/inference                                    2m44s   1GB
Nov 14 12:50:04 Starting compiler/backend/reg_alloc
Nov 14 12:52:13 Finished compiler/backend/reg_alloc                            2m08s   1GB
Nov 14 12:52:13 Starting compiler/backend/gc
Nov 14 12:59:12 Finished compiler/backend/gc                                   6m59s   2GB
Nov 14 12:59:13 Starting compiler/backend
Nov 14 13:09:07 Finished compiler/backend                                      9m54s   5GB
Nov 14 13:09:07 Starting compiler/encoders/asm
Nov 14 13:09:57 Finished compiler/encoders/asm                                   49s 811MB
Nov 14 13:09:57 Starting compiler/encoders/x64
Nov 14 13:12:14 Finished compiler/encoders/x64                                 2m16s 994MB
Nov 14 13:12:14 Starting compiler/encoders/arm7
Nov 14 13:16:53 Finished compiler/encoders/arm7                                4m39s   1GB
Nov 14 13:16:53 Starting compiler/encoders/arm8
Nov 14 13:18:16 Finished compiler/encoders/arm8                                1m22s 746MB
Nov 14 13:18:17 Starting compiler/encoders/mips
Nov 14 13:21:27 Finished compiler/encoders/mips                                3m10s   1GB
Nov 14 13:21:28 Starting compiler/encoders/riscv
Nov 14 13:25:31 Finished compiler/encoders/riscv                               4m02s   1GB
Nov 14 13:25:31 Starting compiler/encoders/ag32
Nov 14 13:26:11 Finished compiler/encoders/ag32                                  40s 716MB
Nov 14 13:26:12 Starting compiler/backend/x64
Nov 14 13:26:54 Finished compiler/backend/x64                                    41s   1GB
Nov 14 13:26:54 Starting compiler/backend/arm7
Nov 14 13:27:40 Finished compiler/backend/arm7                                   46s   1GB
Nov 14 13:27:40 Starting compiler/backend/arm8
Nov 14 13:28:23 Finished compiler/backend/arm8                                   42s   1GB
Nov 14 13:28:23 Starting compiler/backend/mips
Nov 14 13:29:04 Finished compiler/backend/mips                                   40s   1GB
Nov 14 13:29:04 Starting compiler/backend/riscv
Nov 14 13:29:47 Finished compiler/backend/riscv                                  42s   1GB
Nov 14 13:29:47 Starting compiler/backend/ag32
Nov 14 13:32:18 Finished compiler/backend/ag32                                 2m30s   2GB
Nov 14 13:32:18 Starting compiler/parsing/proofs
Nov 14 13:46:57 Finished compiler/parsing/proofs                              14m38s   1GB
Nov 14 13:46:57 Starting compiler/inference/proofs
Nov 14 13:52:28 Finished compiler/inference/proofs                             5m30s   1GB
Nov 14 13:52:28 Starting compiler/backend/semantics
Nov 14 14:55:06 Finished compiler/backend/semantics                         1h02m36s   2GB
Nov 14 14:55:06 Starting compiler/backend/reg_alloc/proofs
Nov 14 15:02:39 Finished compiler/backend/reg_alloc/proofs                     7m32s   1GB
Nov 14 15:02:39 Starting compiler/backend/proofs
Nov 14 16:45:02 Finished compiler/backend/proofs                            1h42m22s  17GB
Nov 14 16:45:02 Starting compiler/backend/serialiser
Nov 14 16:47:26 Finished compiler/backend/serialiser                           2m24s   1GB
Nov 14 16:47:27 Starting compiler/encoders/x64/proofs
Nov 14 17:08:55 Finished compiler/encoders/x64/proofs                         21m28s   5GB
Nov 14 17:08:56 Starting compiler/encoders/arm7/proofs
Nov 14 17:39:08 Finished compiler/encoders/arm7/proofs                        30m11s   4GB
Nov 14 17:39:08 Starting compiler/encoders/arm8/proofs
Nov 14 17:55:05 Finished compiler/encoders/arm8/proofs                        15m56s   1GB
Nov 14 17:55:05 Starting compiler/encoders/mips/proofs
Nov 14 18:18:06 Finished compiler/encoders/mips/proofs                        23m00s   2GB
Nov 14 18:18:06 Starting compiler/encoders/riscv/proofs
Nov 14 18:38:04 Finished compiler/encoders/riscv/proofs                       19m57s   1GB
Nov 14 18:38:05 Starting compiler/encoders/ag32/proofs
Nov 14 18:43:52 Finished compiler/encoders/ag32/proofs                         5m46s 817MB
Nov 14 18:43:52 Starting compiler/backend/x64/proofs
Nov 14 18:44:42 Finished compiler/backend/x64/proofs                             49s   1GB
Nov 14 18:44:42 Starting compiler/backend/arm7/proofs
Nov 14 18:45:34 Finished compiler/backend/arm7/proofs                            51s   1GB
Nov 14 18:45:34 Starting compiler/backend/arm8/proofs
Nov 14 18:46:23 Finished compiler/backend/arm8/proofs                            48s   1GB
Nov 14 18:46:23 Starting compiler/backend/mips/proofs
Nov 14 18:47:12 Finished compiler/backend/mips/proofs                            48s   1GB
Nov 14 18:47:12 Starting compiler/backend/riscv/proofs
Nov 14 18:48:02 Finished compiler/backend/riscv/proofs                           50s   1GB
Nov 14 18:48:02 Starting compiler/backend/ag32/proofs
Nov 14 19:16:12 Finished compiler/backend/ag32/proofs                         28m09s   3GB
Nov 14 19:16:12 Starting compiler/proofs
Nov 14 19:20:42 Finished compiler/proofs                                       4m29s   3GB
Nov 14 19:20:42 Starting candle/set-theory
Nov 14 19:21:42 Finished candle/set-theory                                       59s 699MB
Nov 14 19:21:42 Starting candle/syntax-lib
Nov 14 19:22:07 Finished candle/syntax-lib                                       24s 454MB
Nov 14 19:22:07 Starting candle/standard/syntax
Nov 14 19:26:07 Finished candle/standard/syntax                                3m59s   1GB
Nov 14 19:26:07 Starting candle/standard/semantics
Nov 14 19:29:57 Finished candle/standard/semantics                             3m50s   1GB
Nov 14 19:29:57 Starting candle/standard/monadic
Nov 14 19:33:42 Finished candle/standard/monadic                               3m44s   1GB
Nov 14 19:33:42 Starting candle/standard/ml_kernel
Nov 14 19:45:57 Finished candle/standard/ml_kernel                            12m14s   4GB
Nov 14 19:45:57 Starting candle/overloading/syntax
Nov 14 19:52:34 Finished candle/overloading/syntax                             6m36s   1GB
Nov 14 19:52:34 Starting candle/overloading/semantics
Nov 14 20:19:39 Finished candle/overloading/semantics                         27m04s   5GB
Nov 14 20:19:39 Starting pancake
Nov 14 20:23:32 Finished pancake                                               3m52s   2GB
Nov 14 20:23:32 Starting pancake/ffi
Nov 14 20:23:33 Finished pancake/ffi                                              0s   9MB
Nov 14 20:23:33 Starting pancake/semantics
Nov 14 20:28:23 Finished pancake/semantics                                     4m50s   1GB
Nov 14 20:28:23 Starting pancake/proofs
Nov 14 20:55:40 Finished pancake/proofs                                       27m16s   6GB
Nov 14 20:55:41 Starting characteristic/examples
Nov 14 20:59:12 Finished characteristic/examples                               3m31s   3GB
Nov 14 20:59:12 Starting tutorial/solutions
Nov 14 21:34:26 Finished tutorial/solutions                                   35m13s  14GB
Nov 14 21:34:26 Starting translator/monadic/examples
Nov 14 21:40:20 Finished translator/monadic/examples                           5m53s   2GB
Nov 14 21:40:20 Starting examples
Nov 14 21:57:47 Finished examples                                             17m26s   3GB
Nov 14 21:57:47 Starting examples/compilation/x64
Nov 15 01:35:23 FAILED: examples/compilation/x64
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
/root/regression/cakeml-1635/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml  
Linking /root/regression/cakeml-1635/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 48.8s,    gctime: 1.5s,     systime: 0.28335s.
                to_flat real: 49.0s
                to_flat size: 108009
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.64856s,    gctime: 0.00000s,     systime: 0.00000s.
                to_clos real: 0.64852s
                to_clos size: 44737
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 9.7s,    gctime: 0.33470s,     systime: 0.07652s.
                 to_bvl real: 9.8s
                 to_bvl size: 79180
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 1m35s,    gctime: 1.3s,     systime: 0.43307s.
                 to_bvi real: 1m35s
                 to_bvi size: 83752
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 22.1s,    gctime: 1.4s,     systime: 0.22668s.
                to_data real: 22.4s
                to_data size: 132457
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 32.6s,    gctime: 1.8s,     systime: 0.21324s.
           data_to_word real: 32.8s
           data_to_word size: 432495
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m35s,    gctime: 20.7s,     systime: 8.2s.
 inst,ssa,two-reg (par) real: 1m28s
 inst,ssa,two-reg (par) size: 1289047
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 1m42s,    gctime: 21.2s,     systime: 9.6s.
        get_clash (par) real: 42.8s
        get_clash (par) size: 1999840
        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: 966	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 12	coalesced: 12
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: 4375	coalesceable: 2573	coalesced: 2573
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: 10	coalesceable: 6	coalesced: 6
156 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
168 moves: 17	coalesceable: 11	coalesced: 11
169 moves: 17	coalesceable: 11	coalesced: 11
170 moves: 17	coalesceable: 11	coalesced: 11
171 moves: 5	coalesceable: 3	coalesced: 3
172 moves: 6	coalesceable: 6	coalesced: 6
173 moves: 29	coalesceable: 19	coalesced: 13
174 moves: 4	coalesceable: 4	coalesced: 4
175 moves: 7	coalesceable: 7	coalesced: 7
176 moves: 4	coalesceable: 4	coalesced: 4
177 moves: 9	coalesceable: 9	coalesced: 8
178 moves: 8	coalesceable: 8	coalesced: 8
179 moves: 124	coalesceable: 72	coalesced: 58
180 moves: 6	coalesceable: 6	coalesced: 6
181 moves: 62	coalesceable: 31	coalesced: 29
182 moves: 4	coalesceable: 4	coalesced: 4
183 moves: 48	coalesceable: 23	coalesced: 21
184 moves: 6	coalesceable: 6	coalesced: 6
185 moves: 23	coalesceable: 15	coalesced: 11
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 23	coalesceable: 15	coalesced: 11
188 moves: 6	coalesceable: 6	coalesced: 6
189 moves: 30	coalesceable: 19	coalesced: 16
190 moves: 6	coalesceable: 6	coalesced: 6
191 moves: 29	coalesceable: 21	coalesced: 17
192 moves: 6	coalesceable: 6	coalesced: 6
193 moves: 24	coalesceable: 16	coalesced: 13
194 moves: 6	coalesceable: 6	coalesced: 6
195 moves: 24	coalesceable: 16	coalesced: 13
196 moves: 6	coalesceable: 6	coalesced: 6
197 moves: 30	coalesceable: 22	coalesced: 19
198 moves: 6	coalesceable: 6	coalesced: 6
199 moves: 60	coalesceable: 44	coalesced: 41
200 moves: 6	coalesceable: 6	coalesced: 6
201 moves: 62	coalesceable: 31	coalesced: 29
202 moves: 4	coalesceable: 4	coalesced: 4
203 moves: 3	coalesceable: 3	coalesced: 3
204 moves: 4	coalesceable: 4	coalesced: 4
205 moves: 43	coalesceable: 29	coalesced: 25
206 moves: 4	coalesceable: 4	coalesced: 4
207 moves: 3	coalesceable: 3	coalesced: 3
208 moves: 4	coalesceable: 4	coalesced: 4
209 moves: 18	coalesceable: 16	coalesced: 16
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 25	coalesceable: 18	coalesced: 16
212 moves: 4	coalesceable: 4	coalesced: 4
213 moves: 3	coalesceable: 3	coalesced: 3
214 moves: 6	coalesceable: 6	coalesced: 6
215 moves: 36	coalesceable: 23	coalesced: 17
216 moves: 6	coalesceable: 6	coalesced: 6
217 moves: 21	coalesceable: 19	coalesced: 19
218 moves: 8	coalesceable: 8	coalesced: 8
219 moves: 22	coalesceable: 20	coalesced: 20
220 moves: 12	coalesceable: 12	coalesced: 12
221 moves: 218	coalesceable: 134	coalesced: 94
222 moves: 8	coalesceable: 8	coalesced: 8
223 moves: 124	coalesceable: 72	coalesced: 58
224 moves: 4	coalesceable: 4	coalesced: 4
225 moves: 77	coalesceable: 56	coalesced: 53
226 moves: 6	coalesceable: 6	coalesced: 6
227 moves: 110	coalesceable: 79	coalesced: 69
228 moves: 8	coalesceable: 8	coalesced: 8
229 moves: 407	coalesceable: 208	coalesced: 175
230 moves: 4	coalesceable: 4	coalesced: 4
231 moves: 56	coalesceable: 33	coalesced: 30
232 moves: 4	coalesceable: 4	coalesced: 4
233 moves: 8	coalesceable: 6	coalesced: 6
234 moves: 8	coalesceable: 8	coalesced: 8
235 moves: 163	coalesceable: 110	coalesced: 96
236 moves: 6	coalesceable: 6	coalesced: 6
237 moves: 114	coalesceable: 80	coalesced: 72
238 moves: 4	coalesceable: 4	coalesced: 4
239 moves: 6	coalesceable: 6	coalesced: 6
240 moves: 4	coalesceable: 4	coalesced: 4
241 moves: 6	coalesceable: 6	coalesced: 6
242 moves: 8	coalesceable: 8	coalesced: 8
243 moves: 128	coalesceable: 77	coalesced: 70
244 moves: 8	coalesceable: 8	coalesced: 8
245 moves: 111	coalesceable: 66	coalesced: 51
246 moves: 6	coalesceable: 6	coalesced: 6
247 moves: 50	coalesceable: 38	coalesced: 35
248 moves: 6	coalesceable: 6	coalesced: 6
249 moves: 427	coalesceable: 263	coalesced: 198
250 moves: 4	coalesceable: 4	coalesced: 4
251 moves: 5	coalesceable: 5	coalesced: 5
252 moves: 4	coalesceable: 4	coalesced: 4
253 moves: 272	coalesceable: 139	coalesced: 131
254 moves: 4	coalesceable: 4	coalesced: 4
255 moves: 69	coalesceable: 54	coalesced: 54
256 moves: 6	coalesceable: 6	coalesced: 6
257 moves: 78	coalesceable: 59	coalesced: 56
258 moves: 4	coalesceable: 4	coalesced: 4
259 moves: 21	coalesceable: 18	coalesced: 16
260 moves: 4	coalesceable: 4	coalesced: 4
261 moves: 15	coalesceable: 12	coalesced: 12
262 moves: 25	coalesceable: 21	coalesced: 21
263 moves: 24	coalesceable: 15	coalesced: 15
264 moves: 4	coalesceable: 4	coalesced: 4
265 moves: 34	coalesceable: 19	coalesced: 17
266 moves: 4	coalesceable: 4	coalesced: 4
267 moves: 16	coalesceable: 11	coalesced: 10
268 moves: 4	coalesceable: 4	coalesced: 4
269 moves: 11	coalesceable: 7	coalesced: 7

runtime: 18.1s,    gctime: 0.05014s,     systime: 1.3s.
        external oracle real: 19.3s
        external oracle size: 147263
     apply colour (par) eval: runtime: 2m46s,    gctime: 4.6s,     systime: 16.6s.
     apply colour (par) real: 1m45s
     apply colour (par) size: 648992
           check colour eval: runtime: 2.6s,    gctime: 0.00000s,     systime: 0.02674s.
           check colour real: 2.7s
           check colour size: 649263
          word_to_stack eval: runtime: 2m10s,    gctime: 2.2s,     systime: 2.7s.
          word_to_stack real: 2m12s
          word_to_stack size: 528688
          stack_rawcall eval: runtime: 1m09s,    gctime: 1.1s,     systime: 1.0s.
          stack_rawcall real: 1m10s
          stack_rawcall size: 521518
      stack_alloc (par) eval: runtime: 1m37s,    gctime: 1.2s,     systime: 7.6s.
      stack_alloc (par) real: 50.4s
      stack_alloc (par) size: 523487
expand stack_remove_def eval: runtime: 0.07680s,    gctime: 0.00000s,     systime: 0.04000s.
expand stack_remove_def real: 0.11686s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m14s,    gctime: 1.8s,     systime: 6.9s.
     stack_remove (par) real: 1m17s
     stack_remove (par) size: 892450
      stack_names (par) eval: runtime: 1m09s,    gctime: 1.6s,     systime: 6.6s.
      stack_names (par) real: 36.3s
      stack_names (par) size: 921087
     stack_to_lab (par) eval: runtime: 2m19s,    gctime: 2.9s,     systime: 6.3s.
     stack_to_lab (par) real: 1m08s
     stack_to_lab (par) size: 1122989
          lab_to_target eval: runtime: 7m40s,    gctime: 13.9s,     systime: 6.6s.
          lab_to_target real: 7m47s
          lab_to_target size: 1892751
                      export: runtime: 0.88911s,    gctime: 0.09087s,     systime: 0.11666s.
Saved theorem _____ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 31m17s to build
Linking /root/regression/cakeml-1635/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 1m09s,    gctime: 16.7s,     systime: 1.8s.
                to_flat real: 1m11s
                to_flat size: 156286
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 1.6s,    gctime: 0.14928s,     systime: 0.02001s.
                to_clos real: 1.7s
                to_clos size: 67482
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 13.5s,    gctime: 0.46351s,     systime: 0.16648s.
                 to_bvl real: 13.7s
                 to_bvl size: 124969
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 2m00s,    gctime: 0.58642s,     systime: 0.80970s.
                 to_bvi real: 2m00s
                 to_bvi size: 122734
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 26.4s,    gctime: 1.0s,     systime: 0.30004s.
                to_data real: 26.7s
                to_data size: 194423
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 40.4s,    gctime: 1.5s,     systime: 0.45983s.
           data_to_word real: 40.9s
           data_to_word size: 576662
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 3m14s,    gctime: 9.1s,     systime: 5.2s.
 inst,ssa,two-reg (par) real: 1m11s
 inst,ssa,two-reg (par) size: 1678536
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 3m46s,    gctime: 57.6s,     systime: 21.5s.
        get_clash (par) real: 1m31s
        get_clash (par) size: 2635906
        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: 998	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 12	coalesced: 12
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: 4375	coalesceable: 2573	coalesced: 2573
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: 17	coalesceable: 11	coalesced: 11
170 moves: 10	coalesceable: 6	coalesced: 6
171 moves: 60	coalesceable: 41	coalesced: 40
172 moves: 60	coalesceable: 41	coalesced: 40
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: 17	coalesceable: 11	coalesced: 11
186 moves: 2	coalesceable: 2	coalesced: 2
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: 17	coalesceable: 11	coalesced: 11
204 moves: 114	coalesceable: 84	coalesced: 84
205 moves: 17	coalesceable: 11	coalesced: 11
206 moves: 17	coalesceable: 11	coalesced: 11
207 moves: 5	coalesceable: 3	coalesced: 3
208 moves: 4	coalesceable: 4	coalesced: 4
209 moves: 6	coalesceable: 6	coalesced: 6
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 6	coalesceable: 6	coalesced: 6
212 moves: 6	coalesceable: 6	coalesced: 6
213 moves: 29	coalesceable: 19	coalesced: 13
214 moves: 6	coalesceable: 6	coalesced: 6
215 moves: 32	coalesceable: 23	coalesced: 18
216 moves: 4	coalesceable: 4	coalesced: 4
217 moves: 5	coalesceable: 5	coalesced: 3
218 moves: 6	coalesceable: 6	coalesced: 6
219 moves: 36	coalesceable: 25	coalesced: 24
220 moves: 4	coalesceable: 4	coalesced: 4
221 moves: 5	coalesceable: 5	coalesced: 3
222 moves: 4	coalesceable: 4	coalesced: 4
223 moves: 7	coalesceable: 7	coalesced: 7
224 moves: 4	coalesceable: 4	coalesced: 4
225 moves: 7	coalesceable: 7	coalesced: 7
226 moves: 4	coalesceable: 4	coalesced: 4
227 moves: 45	coalesceable: 35	coalesced: 33
228 moves: 6	coalesceable: 6	coalesced: 6
229 moves: 86	coalesceable: 57	coalesced: 51
230 moves: 6	coalesceable: 6	coalesced: 6
231 moves: 76	coalesceable: 47	coalesced: 43
232 moves: 4	coalesceable: 4	coalesced: 4
233 moves: 9	coalesceable: 9	coalesced: 8
234 moves: 8	coalesceable: 8	coalesced: 8
235 moves: 124	coalesceable: 72	coalesced: 58
236 moves: 6	coalesceable: 6	coalesced: 6
237 moves: 62	coalesceable: 31	coalesced: 29
238 moves: 4	coalesceable: 4	coalesced: 4
239 moves: 48	coalesceable: 23	coalesced: 21
240 moves: 6	coalesceable: 6	coalesced: 6
241 moves: 23	coalesceable: 15	coalesced: 11
242 moves: 6	coalesceable: 6	coalesced: 6
243 moves: 23	coalesceable: 15	coalesced: 11
244 moves: 6	coalesceable: 6	coalesced: 6
245 moves: 30	coalesceable: 19	coalesced: 16
246 moves: 6	coalesceable: 6	coalesced: 6
247 moves: 29	coalesceable: 21	coalesced: 17
248 moves: 6	coalesceable: 6	coalesced: 6
249 moves: 24	coalesceable: 16	coalesced: 13
250 moves: 6	coalesceable: 6	coalesced: 6
251 moves: 24	coalesceable: 16	coalesced: 13
252 moves: 6	coalesceable: 6	coalesced: 6
253 moves: 30	coalesceable: 22	coalesced: 19
254 moves: 6	coalesceable: 6	coalesced: 6
255 moves: 60	coalesceable: 44	coalesced: 41
256 moves: 6	coalesceable: 6	coalesced: 6
257 moves: 62	coalesceable: 31	coalesced: 29
258 moves: 6	coalesceable: 6	coalesced: 6
259 moves: 79	coalesceable: 52	coalesced: 46
260 moves: 4	coalesceable: 4	coalesced: 4
261 moves: 162	coalesceable: 108	coalesced: 98
262 moves: 8	coalesceable: 8	coalesced: 8
263 moves: 284	coalesceable: 173	coalesced: 140
264 moves: 8	coalesceable: 8	coalesced: 8
265 moves: 119	coalesceable: 79	coalesced: 60
266 moves: 4	coalesceable: 4	coalesced: 4
267 moves: 423	coalesceable: 264	coalesced: 209
268 moves: 4	coalesceable: 4	coalesced: 4
269 moves: 3	coalesceable: 3	coalesced: 3
270 moves: 4	coalesceable: 4	coalesced: 4
271 moves: 43	coalesceable: 29	coalesced: 25
272 moves: 4	coalesceable: 4	coalesced: 4
273 moves: 25	coalesceable: 18	coalesced: 16
274 moves: 4	coalesceable: 4	coalesced: 4
275 moves: 3	coalesceable: 3	coalesced: 3
276 moves: 6	coalesceable: 6	coalesced: 6
277 moves: 36	coalesceable: 23	coalesced: 17
278 moves: 6	coalesceable: 6	coalesced: 6
279 moves: 21	coalesceable: 19	coalesced: 19
280 moves: 4	coalesceable: 4	coalesced: 4
281 moves: 9	coalesceable: 9	coalesced: 8
282 moves: 8	coalesceable: 8	coalesced: 8
283 moves: 22	coalesceable: 20	coalesced: 20
284 moves: 12	coalesceable: 12	coalesced: 12
285 moves: 218	coalesceable: 134	coalesced: 94
286 moves: 12	coalesceable: 12	coalesced: 12
287 moves: 218	coalesceable: 134	coalesced: 94
288 moves: 8	coalesceable: 8	coalesced: 8
289 moves: 124	coalesceable: 72	coalesced: 58
290 moves: 4	coalesceable: 4	coalesced: 4
291 moves: 77	coalesceable: 56	coalesced: 53
292 moves: 6	coalesceable: 6	coalesced: 6
293 moves: 110	coalesceable: 79	coalesced: 69
294 moves: 8	coalesceable: 8	coalesced: 8
295 moves: 407	coalesceable: 208	coalesced: 175
296 moves: 4	coalesceable: 4	coalesced: 4
297 moves: 56	coalesceable: 33	coalesced: 30
298 moves: 4	coalesceable: 4	coalesced: 4
299 moves: 8	coalesceable: 6	coalesced: 6
300 moves: 8	coalesceable: 8	coalesced: 8
301 moves: 163	coalesceable: 110	coalesced: 96
302 moves: 6	coalesceable: 6	coalesced: 6
303 moves: 114	coalesceable: 80	coalesced: 72
304 moves: 4	coalesceable: 4	coalesced: 4
305 moves: 6	coalesceable: 6	coalesced: 6
306 moves: 4	coalesceable: 4	coalesced: 4
307 moves: 6	coalesceable: 6	coalesced: 6
308 moves: 8	coalesceable: 8	coalesced: 8
309 moves: 128	coalesceable: 77	coalesced: 70
310 moves: 8	coalesceable: 8	coalesced: 8
311 moves: 111	coalesceable: 66	coalesced: 51
312 moves: 6	coalesceable: 6	coalesced: 6
313 moves: 427	coalesceable: 263	coalesced: 198
314 moves: 4	coalesceable: 4	coalesced: 4
315 moves: 5	coalesceable: 5	coalesced: 5
316 moves: 4	coalesceable: 4	coalesced: 4
317 moves: 17	coalesceable: 12	coalesced: 11
318 moves: 4	coalesceable: 4	coalesced: 4
319 moves: 272	coalesceable: 139	coalesced: 131
320 moves: 4	coalesceable: 4	coalesced: 4
321 moves: 69	coalesceable: 54	coalesced: 54
322 moves: 6	coalesceable: 6	coalesced: 6
323 moves: 78	coalesceable: 59	coalesced: 56
324 moves: 4	coalesceable: 4	coalesced: 4
325 moves: 21	coalesceable: 18	coalesced: 16
326 moves: 4	coalesceable: 4	coalesced: 4
327 moves: 164	coalesceable: 106	coalesced: 89
328 moves: 224	coalesceable: 137	coalesced: 113
329 moves: 217	coalesceable: 133	coalesced: 108
330 moves: 4	coalesceable: 4	coalesced: 4
331 moves: 45	coalesceable: 26	coalesced: 24
332 moves: 4	coalesceable: 4	coalesced: 4
333 moves: 42	coalesceable: 23	coalesced: 22
334 moves: 4	coalesceable: 4	coalesced: 4
335 moves: 15	coalesceable: 12	coalesced: 12
336 moves: 36	coalesceable: 18	coalesced: 18
337 moves: 6	coalesceable: 6	coalesced: 6
338 moves: 95	coalesceable: 59	coalesced: 59
339 moves: 12	coalesceable: 12	coalesced: 12
340 moves: 362	coalesceable: 166	coalesced: 106
341 moves: 8	coalesceable: 8	coalesced: 8
342 moves: 98	coalesceable: 66	coalesced: 52
343 moves: 6	coalesceable: 6	coalesced: 6
344 moves: 84	coalesceable: 52	coalesced: 43
345 moves: 6	coalesceable: 6	coalesced: 6
346 moves: 55	coalesceable: 28	coalesced: 23
347 moves: 6	coalesceable: 6	coalesced: 6
348 moves: 90	coalesceable: 61	coalesced: 58
349 moves: 8	coalesceable: 8	coalesced: 8
350 moves: 157	coalesceable: 106	coalesced: 88
351 moves: 6	coalesceable: 6	coalesced: 6
352 moves: 99	coalesceable: 62	coalesced: 56
353 moves: 6	coalesceable: 6	coalesced: 6
354 moves: 275	coalesceable: 122	coalesced: 107
355 moves: 6	coalesceable: 6	coalesced: 6
356 moves: 7	coalesceable: 7	coalesced: 7
357 moves: 10	coalesceable: 10	coalesced: 10
358 moves: 375	coalesceable: 141	coalesced: 119
359 moves: 6	coalesceable: 6	coalesced: 6
360 moves: 35	coalesceable: 25	coalesced: 20
361 moves: 10	coalesceable: 10	coalesced: 10
362 moves: 1001	coalesceable: 448	coalesced: 387
363 moves: 6	coalesceable: 6	coalesced: 6
364 moves: 162	coalesceable: 92	coalesced: 88
365 moves: 33	coalesceable: 25	coalesced: 23
366 moves: 33	coalesceable: 25	coalesced: 23
367 moves: 12	coalesceable: 12	coalesced: 12
368 moves: 2015	coalesceable: 1063	coalesced: 797
369 moves: 6	coalesceable: 6	coalesced: 6
370 moves: 690	coalesceable: 353	coalesced: 200
371 moves: 4	coalesceable: 4	coalesced: 4
372 moves: 266	coalesceable: 170	coalesced: 166
373 moves: 6	coalesceable: 6	coalesced: 6
374 moves: 570	coalesceable: 359	coalesced: 352
375 moves: 4	coalesceable: 4	coalesced: 4
376 moves: 47	coalesceable: 39	coalesced: 39

runtime: 21.0s,    gctime: 0.03128s,     systime: 0.57311s.
        external oracle real: 21.7s
        external oracle size: 199313
     apply colour (par) eval: runtime: 3m55s,    gctime: 5.7s,     systime: 20.8s.
     apply colour (par) real: 1m51s
     apply colour (par) size: 851292
           check colour eval: runtime: 6.1s,    gctime: 0.59597s,     systime: 0.17661s.
           check colour real: 6.3s
           check colour size: 851670
          word_to_stack eval: runtime: 3m06s,    gctime: 2.8s,     systime: 10.9s.
          word_to_stack real: 3m16s
          word_to_stack size: 675490
          stack_rawcall eval: runtime: 1m30s,    gctime: 1.0s,     systime: 2.6s.
          stack_rawcall real: 1m32s
          stack_rawcall size: 666691
      stack_alloc (par) eval: runtime: 2m09s,    gctime: 1.4s,     systime: 10.0s.
      stack_alloc (par) real: 50.0s
      stack_alloc (par) size: 670678
expand stack_remove_def eval: runtime: 0.10235s,    gctime: 0.00000s,     systime: 0.00661s.
expand stack_remove_def real: 0.10901s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m56s,    gctime: 1.7s,     systime: 7.7s.
     stack_remove (par) real: 1m16s
     stack_remove (par) size: 1122514
      stack_names (par) eval: runtime: 1m31s,    gctime: 1.3s,     systime: 6.5s.
      stack_names (par) real: 36.8s
      stack_names (par) size: 1159331
     stack_to_lab (par) eval: runtime: 3m06s,    gctime: 2.8s,     systime: 11.8s.
     stack_to_lab (par) real: 1m09s
     stack_to_lab (par) size: 1428576
          lab_to_target eval: runtime: 9m46s,    gctime: 13.3s,     systime: 15.8s.
          lab_to_target real: 10m02s
          lab_to_target size: 2428612
                      export: runtime: 0.98177s,    gctime: 0.00000s,     systime: 0.00007s.
Saved theorem _____ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 42m36s to build
Linking /root/regression/cakeml-1635/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 49.7s,    gctime: 0.85813s,     systime: 0.93652s.
                to_flat real: 50.7s
                to_flat size: 102649
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.56245s,    gctime: 0.00000s,     systime: 0.00010s.
                to_clos real: 0.56246s
                to_clos size: 41877
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 9.2s,    gctime: 0.26652s,     systime: 0.07329s.
                 to_bvl real: 9.2s
                 to_bvl size: 69850
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 1m31s,    gctime: 0.52873s,     systime: 0.73685s.
                 to_bvi real: 1m32s
                 to_bvi size: 75750
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 21.5s,    gctime: 0.87242s,     systime: 0.25331s.
                to_data real: 21.8s
                to_data size: 124389
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 31.0s,    gctime: 1.2s,     systime: 0.41662s.
           data_to_word real: 31.4s
           data_to_word size: 413772
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m11s,    gctime: 5.4s,     systime: 5.7s.
 inst,ssa,two-reg (par) real: 1m08s
 inst,ssa,two-reg (par) size: 1255320
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 1m32s,    gctime: 24.5s,     systime: 9.7s.
        get_clash (par) real: 46.1s
        get_clash (par) size: 1952396
        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: 960	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 12	coalesced: 12
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: 4375	coalesceable: 2573	coalesced: 2573
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: 10	coalesceable: 6	coalesced: 6
151 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
158 moves: 17	coalesceable: 11	coalesced: 11
159 moves: 5	coalesceable: 3	coalesced: 3
160 moves: 6	coalesceable: 6	coalesced: 6
161 moves: 29	coalesceable: 19	coalesced: 13
162 moves: 4	coalesceable: 4	coalesced: 4
163 moves: 7	coalesceable: 7	coalesced: 7
164 moves: 4	coalesceable: 4	coalesced: 4
165 moves: 9	coalesceable: 9	coalesced: 8
166 moves: 8	coalesceable: 8	coalesced: 8
167 moves: 124	coalesceable: 72	coalesced: 58
168 moves: 6	coalesceable: 6	coalesced: 6
169 moves: 62	coalesceable: 31	coalesced: 29
170 moves: 8	coalesceable: 8	coalesced: 8
171 moves: 180	coalesceable: 93	coalesced: 89
172 moves: 6	coalesceable: 6	coalesced: 6
173 moves: 7	coalesceable: 7	coalesced: 4
174 moves: 6	coalesceable: 6	coalesced: 6
175 moves: 23	coalesceable: 15	coalesced: 11
176 moves: 6	coalesceable: 6	coalesced: 6
177 moves: 23	coalesceable: 15	coalesced: 11
178 moves: 6	coalesceable: 6	coalesced: 6
179 moves: 30	coalesceable: 19	coalesced: 16
180 moves: 6	coalesceable: 6	coalesced: 6
181 moves: 29	coalesceable: 21	coalesced: 17
182 moves: 6	coalesceable: 6	coalesced: 6
183 moves: 24	coalesceable: 16	coalesced: 13
184 moves: 6	coalesceable: 6	coalesced: 6
185 moves: 24	coalesceable: 16	coalesced: 13
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 30	coalesceable: 22	coalesced: 19
188 moves: 4	coalesceable: 4	coalesced: 4
189 moves: 3	coalesceable: 3	coalesced: 3
190 moves: 4	coalesceable: 4	coalesced: 4
191 moves: 25	coalesceable: 18	coalesced: 16
192 moves: 4	coalesceable: 4	coalesced: 4
193 moves: 3	coalesceable: 3	coalesced: 3
194 moves: 6	coalesceable: 6	coalesced: 6
195 moves: 36	coalesceable: 23	coalesced: 17
196 moves: 6	coalesceable: 6	coalesced: 6
197 moves: 21	coalesceable: 19	coalesced: 19
198 moves: 8	coalesceable: 8	coalesced: 8
199 moves: 22	coalesceable: 20	coalesced: 20
200 moves: 12	coalesceable: 12	coalesced: 12
201 moves: 218	coalesceable: 134	coalesced: 94
202 moves: 8	coalesceable: 8	coalesced: 8
203 moves: 124	coalesceable: 72	coalesced: 58
204 moves: 4	coalesceable: 4	coalesced: 4
205 moves: 77	coalesceable: 56	coalesced: 53
206 moves: 6	coalesceable: 6	coalesced: 6
207 moves: 110	coalesceable: 79	coalesced: 69
208 moves: 8	coalesceable: 8	coalesced: 8
209 moves: 407	coalesceable: 208	coalesced: 175
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 56	coalesceable: 33	coalesced: 30
212 moves: 4	coalesceable: 4	coalesced: 4
213 moves: 8	coalesceable: 6	coalesced: 6
214 moves: 8	coalesceable: 8	coalesced: 8
215 moves: 163	coalesceable: 110	coalesced: 96
216 moves: 6	coalesceable: 6	coalesced: 6
217 moves: 114	coalesceable: 80	coalesced: 72
218 moves: 4	coalesceable: 4	coalesced: 4
219 moves: 6	coalesceable: 6	coalesced: 6
220 moves: 8	coalesceable: 8	coalesced: 8
221 moves: 128	coalesceable: 77	coalesced: 70
222 moves: 8	coalesceable: 8	coalesced: 8
223 moves: 111	coalesceable: 66	coalesced: 51
224 moves: 6	coalesceable: 6	coalesced: 6
225 moves: 50	coalesceable: 38	coalesced: 35
226 moves: 6	coalesceable: 6	coalesced: 6
227 moves: 427	coalesceable: 263	coalesced: 198
228 moves: 4	coalesceable: 4	coalesced: 4
229 moves: 5	coalesceable: 5	coalesced: 5
230 moves: 4	coalesceable: 4	coalesced: 4
231 moves: 36	coalesceable: 21	coalesced: 19

runtime: 18.4s,    gctime: 0.10071s,     systime: 0.44331s.
        external oracle real: 18.8s
        external oracle size: 142302
     apply colour (par) eval: runtime: 2m43s,    gctime: 4.5s,     systime: 14.8s.
     apply colour (par) real: 1m46s
     apply colour (par) size: 627225
           check colour eval: runtime: 2.2s,    gctime: 0.25093s,     systime: 0.12007s.
           check colour real: 2.3s
           check colour size: 627458
          word_to_stack eval: runtime: 2m09s,    gctime: 2.4s,     systime: 2.0s.
          word_to_stack real: 2m11s
          word_to_stack size: 512579
          stack_rawcall eval: runtime: 1m07s,    gctime: 0.81045s,     systime: 0.72975s.
          stack_rawcall real: 1m07s
          stack_rawcall size: 505923
      stack_alloc (par) eval: runtime: 1m32s,    gctime: 1.2s,     systime: 4.4s.
      stack_alloc (par) real: 47.3s
      stack_alloc (par) size: 507592
expand stack_remove_def eval: runtime: 0.08129s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.08134s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m11s,    gctime: 1.9s,     systime: 6.2s.
     stack_remove (par) real: 1m16s
     stack_remove (par) size: 866734
      stack_names (par) eval: runtime: 1m05s,    gctime: 1.5s,     systime: 3.4s.
      stack_names (par) real: 34.1s
      stack_names (par) size: 894483
     stack_to_lab (par) eval: runtime: 2m11s,    gctime: 2.9s,     systime: 3.9s.
     stack_to_lab (par) real: 1m05s
     stack_to_lab (par) size: 1088542
          lab_to_target eval: runtime: 7m37s,    gctime: 13.5s,     systime: 5.5s.
          lab_to_target real: 7m42s
          lab_to_target size: 1829551
                      export: runtime: 0.96564s,    gctime: 0.22219s,     systime: 0.03671s.
Saved theorem _____ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 29m38s to build
cc cat.S /root/regression/cakeml-1635/basis/basis_ffi.o  -o cake_cat
cc diff.S /root/regression/cakeml-1635/basis/basis_ffi.o  -o cake_diff
cc echo.S /root/regression/cakeml-1635/basis/basis_ffi.o  -o cake_echo
Linking /root/regression/cakeml-1635/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 1m37s,    gctime: 2.0s,     systime: 0.83263s.
                to_flat real: 1m38s
                to_flat size: 387627
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 5.9s,    gctime: 0.28061s,     systime: 0.09672s.
                to_clos real: 6.0s
                to_clos size: 163422
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 35.1s,    gctime: 1.2s,     systime: 0.35996s.
                 to_bvl real: 35.5s
                 to_bvl size: 293259
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 4m17s,    gctime: 2.7s,     systime: 1.4s.
                 to_bvi real: 4m19s
                 to_bvi size: 254526
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 57.9s,    gctime: 3.3s,     systime: 0.53342s.
                to_data real: 58.4s
                to_data size: 468364
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 2m19s,    gctime: 7.6s,     systime: 0.96979s.
           data_to_word real: 2m20s
           data_to_word size: 1579797
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 22m50s,    gctime: 2m17s,     systime: 40.1s.
 inst,ssa,two-reg (par) real: 17m44s
 inst,ssa,two-reg (par) size: 4926391
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 10m43s,    gctime: 1m47s,     systime: 37.7s.
        get_clash (par) real: 3m20s
        get_clash (par) size: 7516528
        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: 242	coalesceable: 2	coalesced: 2
118 moves: 1002	coalesceable: 2	coalesced: 2
119 moves: 17	coalesceable: 12	coalesced: 12
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: 17	coalesceable: 11	coalesced: 11
248 moves: 74	coalesceable: 49	coalesced: 43
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: 17	coalesceable: 11	coalesced: 11
263 moves: 17	coalesceable: 11	coalesced: 11
264 moves: 17	coalesceable: 11	coalesced: 11
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: 5885	coalesceable: 3532	coalesced: 3033
273 moves: 11474	coalesceable: 7187	coalesced: 6357
274 moves: 10448	coalesceable: 6311	coalesced: 5527
275 moves: 17	coalesceable: 11	coalesced: 11
276 moves: 17	coalesceable: 11	coalesced: 11
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: 17	coalesceable: 11	coalesced: 11
284 moves: 17	coalesceable: 11	coalesced: 11
285 moves: 17	coalesceable: 11	coalesced: 11
286 moves: 102	coalesceable: 58	coalesced: 58
287 moves: 17	coalesceable: 11	coalesced: 11
288 moves: 17	coalesceable: 11	coalesced: 11
289 moves: 17	coalesceable: 11	coalesced: 11
290 moves: 17	coalesceable: 11	coalesced: 11
291 moves: 17	coalesceable: 11	coalesced: 11
292 moves: 17	coalesceable: 11	coalesced: 11
293 moves: 2705	coalesceable: 1486	coalesced: 1387
294 moves: 17	coalesceable: 11	coalesced: 11
295 moves: 17	coalesceable: 11	coalesced: 11
296 moves: 17	coalesceable: 11	coalesced: 11
297 moves: 17	coalesceable: 11	coalesced: 11
298 moves: 17	coalesceable: 11	coalesced: 11
299 moves: 158	coalesceable: 117	coalesced: 117
300 moves: 17	coalesceable: 11	coalesced: 11
301 moves: 17	coalesceable: 11	coalesced: 11
302 moves: 17	coalesceable: 11	coalesced: 11
303 moves: 17	coalesceable: 11	coalesced: 11
304 moves: 5	coalesceable: 3	coalesced: 3
305 moves: 4	coalesceable: 4	coalesced: 4
306 moves: 6	coalesceable: 6	coalesced: 6
307 moves: 4	coalesceable: 4	coalesced: 4
308 moves: 6	coalesceable: 6	coalesced: 6
309 moves: 8	coalesceable: 8	coalesced: 8
310 moves: 46	coalesceable: 34	coalesced: 33
311 moves: 4	coalesceable: 4	coalesced: 4
312 moves: 3	coalesceable: 3	coalesced: 3
313 moves: 6	coalesceable: 6	coalesced: 6
314 moves: 3	coalesceable: 3	coalesced: 2
315 moves: 8	coalesceable: 8	coalesced: 8
316 moves: 99	coalesceable: 63	coalesced: 50
317 moves: 6	coalesceable: 6	coalesced: 6
318 moves: 7	coalesceable: 7	coalesced: 4
319 moves: 6	coalesceable: 6	coalesced: 6
320 moves: 29	coalesceable: 19	coalesced: 13
321 moves: 8	coalesceable: 8	coalesced: 8
322 moves: 103	coalesceable: 64	coalesced: 59
323 moves: 4	coalesceable: 4	coalesced: 4
324 moves: 7	coalesceable: 7	coalesced: 7
325 moves: 6	coalesceable: 6	coalesced: 6
326 moves: 49	coalesceable: 36	coalesced: 34
327 moves: 6	coalesceable: 6	coalesced: 6
328 moves: 32	coalesceable: 23	coalesced: 18
329 moves: 4	coalesceable: 4	coalesced: 4
330 moves: 5	coalesceable: 5	coalesced: 3
331 moves: 4	coalesceable: 4	coalesced: 4
332 moves: 7	coalesceable: 7	coalesced: 7
333 moves: 6	coalesceable: 6	coalesced: 6
334 moves: 86	coalesceable: 57	coalesced: 51
335 moves: 6	coalesceable: 6	coalesced: 6
336 moves: 76	coalesceable: 47	coalesced: 43
337 moves: 6	coalesceable: 6	coalesced: 6
338 moves: 42	coalesceable: 27	coalesced: 25
339 moves: 4	coalesceable: 4	coalesced: 4
340 moves: 95	coalesceable: 58	coalesced: 57
341 moves: 6	coalesceable: 6	coalesced: 6
342 moves: 49	coalesceable: 37	coalesced: 35
343 moves: 4	coalesceable: 4	coalesced: 4
344 moves: 73	coalesceable: 49	coalesced: 47
345 moves: 6	coalesceable: 6	coalesced: 6
346 moves: 79	coalesceable: 57	coalesced: 54
347 moves: 6	coalesceable: 6	coalesced: 6
348 moves: 42	coalesceable: 27	coalesced: 26
349 moves: 4	coalesceable: 4	coalesced: 4
350 moves: 12	coalesceable: 11	coalesced: 9
351 moves: 4	coalesceable: 4	coalesced: 4
352 moves: 9	coalesceable: 9	coalesced: 8
353 moves: 4	coalesceable: 4	coalesced: 4
354 moves: 29	coalesceable: 12	coalesced: 11
355 moves: 8	coalesceable: 8	coalesced: 8
356 moves: 124	coalesceable: 72	coalesced: 58
357 moves: 6	coalesceable: 6	coalesced: 6
358 moves: 62	coalesceable: 31	coalesced: 29
359 moves: 4	coalesceable: 4	coalesced: 4
360 moves: 48	coalesceable: 23	coalesced: 21
361 moves: 6	coalesceable: 6	coalesced: 6
362 moves: 23	coalesceable: 15	coalesced: 11
363 moves: 6	coalesceable: 6	coalesced: 6
364 moves: 23	coalesceable: 15	coalesced: 11
365 moves: 6	coalesceable: 6	coalesced: 6
366 moves: 30	coalesceable: 19	coalesced: 16
367 moves: 6	coalesceable: 6	coalesced: 6
368 moves: 29	coalesceable: 21	coalesced: 17
369 moves: 6	coalesceable: 6	coalesced: 6
370 moves: 24	coalesceable: 16	coalesced: 13
371 moves: 6	coalesceable: 6	coalesced: 6
372 moves: 24	coalesceable: 16	coalesced: 13
373 moves: 6	coalesceable: 6	coalesced: 6
374 moves: 30	coalesceable: 22	coalesced: 19
375 moves: 6	coalesceable: 6	coalesced: 6
376 moves: 60	coalesceable: 44	coalesced: 41
377 moves: 6	coalesceable: 6	coalesced: 6
378 moves: 62	coalesceable: 31	coalesced: 29
379 moves: 4	coalesceable: 4	coalesced: 4
380 moves: 3	coalesceable: 3	coalesced: 3
381 moves: 4	coalesceable: 4	coalesced: 4
382 moves: 43	coalesceable: 29	coalesced: 25
383 moves: 4	coalesceable: 4	coalesced: 4
384 moves: 25	coalesceable: 18	coalesced: 16
385 moves: 4	coalesceable: 4	coalesced: 4
386 moves: 3	coalesceable: 3	coalesced: 3
387 moves: 6	coalesceable: 6	coalesced: 6
388 moves: 36	coalesceable: 23	coalesced: 17
389 moves: 6	coalesceable: 6	coalesced: 6
390 moves: 21	coalesceable: 19	coalesced: 19
391 moves: 4	coalesceable: 4	coalesced: 4
392 moves: 9	coalesceable: 9	coalesced: 8
393 moves: 8	coalesceable: 8	coalesced: 8
394 moves: 22	coalesceable: 20	coalesced: 20
395 moves: 12	coalesceable: 12	coalesced: 12
396 moves: 218	coalesceable: 134	coalesced: 94
397 moves: 12	coalesceable: 12	coalesced: 12
398 moves: 218	coalesceable: 134	coalesced: 94
399 moves: 8	coalesceable: 8	coalesced: 8
400 moves: 124	coalesceable: 72	coalesced: 58
401 moves: 4	coalesceable: 4	coalesced: 4
402 moves: 77	coalesceable: 56	coalesced: 53
403 moves: 6	coalesceable: 6	coalesced: 6
404 moves: 110	coalesceable: 79	coalesced: 69
405 moves: 8	coalesceable: 8	coalesced: 8
406 moves: 407	coalesceable: 208	coalesced: 175
407 moves: 4	coalesceable: 4	coalesced: 4
408 moves: 56	coalesceable: 33	coalesced: 30
409 moves: 4	coalesceable: 4	coalesced: 4
410 moves: 8	coalesceable: 6	coalesced: 6
411 moves: 8	coalesceable: 8	coalesced: 8
412 moves: 163	coalesceable: 110	coalesced: 96
413 moves: 6	coalesceable: 6	coalesced: 6
414 moves: 114	coalesceable: 80	coalesced: 72
415 moves: 4	coalesceable: 4	coalesced: 4
416 moves: 6	coalesceable: 6	coalesced: 6
417 moves: 4	coalesceable: 4	coalesced: 4
418 moves: 6	coalesceable: 6	coalesced: 6
419 moves: 8	coalesceable: 8	coalesced: 8
420 moves: 128	coalesceable: 77	coalesced: 70
421 moves: 8	coalesceable: 8	coalesced: 8
422 moves: 111	coalesceable: 66	coalesced: 51
423 moves: 6	coalesceable: 6	coalesced: 6
424 moves: 427	coalesceable: 263	coalesced: 198
425 moves: 4	coalesceable: 4	coalesced: 4
426 moves: 5	coalesceable: 5	coalesced: 5
427 moves: 4	coalesceable: 4	coalesced: 4
428 moves: 272	coalesceable: 139	coalesced: 131
429 moves: 4	coalesceable: 4	coalesced: 4
430 moves: 69	coalesceable: 54	coalesced: 54
431 moves: 6	coalesceable: 6	coalesced: 6
432 moves: 78	coalesceable: 59	coalesced: 56
433 moves: 4	coalesceable: 4	coalesced: 4
434 moves: 21	coalesceable: 18	coalesced: 16
435 moves: 4	coalesceable: 4	coalesced: 4
436 moves: 164	coalesceable: 106	coalesced: 89
437 moves: 224	coalesceable: 137	coalesced: 113
438 moves: 217	coalesceable: 133	coalesced: 108
439 moves: 4	coalesceable: 4	coalesced: 4
440 moves: 45	coalesceable: 26	coalesced: 24
441 moves: 6	coalesceable: 6	coalesced: 6
442 moves: 152	coalesceable: 102	coalesced: 97
443 moves: 6	coalesceable: 6	coalesced: 6
444 moves: 847	coalesceable: 556	coalesced: 502
445 moves: 6	coalesceable: 6	coalesced: 6
446 moves: 30	coalesceable: 21	coalesced: 16
447 moves: 4	coalesceable: 4	coalesced: 4
448 moves: 7	coalesceable: 7	coalesced: 7
449 moves: 6	coalesceable: 6	coalesced: 6
450 moves: 30	coalesceable: 17	coalesced: 16
451 moves: 10	coalesceable: 10	coalesced: 10
452 moves: 2844	coalesceable: 1470	coalesced: 781
453 moves: 10	coalesceable: 10	coalesced: 10
454 moves: 2803	coalesceable: 1454	coalesced: 770
455 moves: 4	coalesceable: 4	coalesced: 4
456 moves: 150	coalesceable: 86	coalesced: 76
457 moves: 4	coalesceable: 4	coalesced: 4
458 moves: 4	coalesceable: 4	coalesced: 4
459 moves: 8	coalesceable: 8	coalesced: 8
460 moves: 99	coalesceable: 63	coalesced: 57
461 moves: 8	coalesceable: 8	coalesced: 8
462 moves: 72	coalesceable: 48	coalesced: 44
463 moves: 10	coalesceable: 10	coalesced: 10
464 moves: 195	coalesceable: 104	coalesced: 68
465 moves: 8	coalesceable: 8	coalesced: 8
466 moves: 74	coalesceable: 47	coalesced: 43
467 moves: 6	coalesceable: 6	coalesced: 6
468 moves: 58	coalesceable: 40	coalesced: 33
469 moves: 6	coalesceable: 6	coalesced: 6
470 moves: 634	coalesceable: 440	coalesced: 316
471 moves: 6	coalesceable: 6	coalesced: 6
472 moves: 15	coalesceable: 15	coalesced: 15
473 moves: 4	coalesceable: 4	coalesced: 4
474 moves: 321	coalesceable: 204	coalesced: 200
475 moves: 8	coalesceable: 8	coalesced: 8
476 moves: 107	coalesceable: 65	coalesced: 65
477 moves: 10	coalesceable: 10	coalesced: 10
478 moves: 514	coalesceable: 292	coalesced: 271
479 moves: 4	coalesceable: 4	coalesced: 4
480 moves: 26	coalesceable: 19	coalesced: 17
481 moves: 8	coalesceable: 8	coalesced: 8
482 moves: 256	coalesceable: 149	coalesced: 130
483 moves: 8	coalesceable: 8	coalesced: 8
484 moves: 789	coalesceable: 475	coalesced: 427
485 moves: 6	coalesceable: 6	coalesced: 6
486 moves: 37	coalesceable: 23	coalesced: 22
487 moves: 4	coalesceable: 4	coalesced: 4
488 moves: 201	coalesceable: 119	coalesced: 113
489 moves: 6	coalesceable: 6	coalesced: 6
490 moves: 220	coalesceable: 158	coalesced: 129
491 moves: 4	coalesceable: 4	coalesced: 4
492 moves: 477	coalesceable: 295	coalesced: 290
493 moves: 6	coalesceable: 6	coalesced: 6
494 moves: 16	coalesceable: 9	coalesced: 6
495 moves: 6	coalesceable: 6	coalesced: 6
496 moves: 42	coalesceable: 26	coalesced: 25
497 moves: 4	coalesceable: 4	coalesced: 4
498 moves: 208	coalesceable: 121	coalesced: 117
499 moves: 4	coalesceable: 4	coalesced: 4
500 moves: 419	coalesceable: 260	coalesced: 230
501 moves: 4	coalesceable: 4	coalesced: 4
502 moves: 21	coalesceable: 14	coalesced: 13
503 moves: 6	coalesceable: 6	coalesced: 6
504 moves: 188	coalesceable: 117	coalesced: 112
505 moves: 6	coalesceable: 6	coalesced: 6
506 moves: 161	coalesceable: 117	coalesced: 95
507 moves: 4	coalesceable: 4	coalesced: 4
508 moves: 156	coalesceable: 103	coalesced: 98
509 moves: 4	coalesceable: 4	coalesced: 4
510 moves: 138	coalesceable: 92	coalesced: 88
511 moves: 4	coalesceable: 4	coalesced: 4
512 moves: 4	coalesceable: 4	coalesced: 4
513 moves: 4	coalesceable: 4	coalesced: 4
514 moves: 100	coalesceable: 64	coalesced: 61
515 moves: 6	coalesceable: 6	coalesced: 6
516 moves: 7	coalesceable: 7	coalesced: 7
517 moves: 10	coalesceable: 10	coalesced: 10
518 moves: 70	coalesceable: 61	coalesced: 55
519 moves: 4	coalesceable: 4	coalesced: 4
520 moves: 174	coalesceable: 110	coalesced: 105
521 moves: 4	coalesceable: 4	coalesced: 4
522 moves: 23	coalesceable: 15	coalesced: 14
523 moves: 9	coalesceable: 9	coalesced: 9
524 moves: 6	coalesceable: 6	coalesced: 6
525 moves: 232	coalesceable: 126	coalesced: 117
526 moves: 37	coalesceable: 23	coalesced: 20
527 moves: 4	coalesceable: 4	coalesced: 4
528 moves: 25	coalesceable: 16	coalesced: 14
529 moves: 10	coalesceable: 10	coalesced: 10
530 moves: 224	coalesceable: 128	coalesced: 94
531 moves: 8	coalesceable: 8	coalesced: 8
532 moves: 282	coalesceable: 163	coalesced: 151
533 moves: 8	coalesceable: 8	coalesced: 8
534 moves: 52	coalesceable: 37	coalesced: 31
535 moves: 6	coalesceable: 6	coalesced: 6
536 moves: 8	coalesceable: 8	coalesced: 6
537 moves: 6	coalesceable: 6	coalesced: 6
538 moves: 11	coalesceable: 11	coalesced: 9
539 moves: 10	coalesceable: 10	coalesced: 10
540 moves: 405	coalesceable: 209	coalesced: 162
541 moves: 10	coalesceable: 10	coalesced: 10
542 moves: 1186	coalesceable: 706	coalesced: 410
543 moves: 10	coalesceable: 10	coalesced: 10
544 moves: 96	coalesceable: 62	coalesced: 53
545 moves: 6	coalesceable: 6	coalesced: 6
546 moves: 24	coalesceable: 16	coalesced: 13
547 moves: 4	coalesceable: 4	coalesced: 4
548 moves: 36	coalesceable: 24	coalesced: 23
549 moves: 6	coalesceable: 6	coalesced: 6
550 moves: 24	coalesceable: 16	coalesced: 13
551 moves: 4	coalesceable: 4	coalesced: 4
552 moves: 147	coalesceable: 73	coalesced: 54
553 moves: 4	coalesceable: 4	coalesced: 4
554 moves: 89	coalesceable: 54	coalesced: 47
555 moves: 4	coalesceable: 4	coalesced: 4
556 moves: 22	coalesceable: 14	coalesced: 13
557 moves: 6	coalesceable: 6	coalesced: 6
558 moves: 40	coalesceable: 23	coalesced: 19
559 moves: 8	coalesceable: 8	coalesced: 8
560 moves: 64	coalesceable: 35	coalesced: 33
561 moves: 6	coalesceable: 6	coalesced: 6
562 moves: 24	coalesceable: 16	coalesced: 13
563 moves: 4	coalesceable: 4	coalesced: 4
564 moves: 59	coalesceable: 34	coalesced: 31
565 moves: 4	coalesceable: 4	coalesced: 4
566 moves: 252	coalesceable: 137	coalesced: 115
567 moves: 4	coalesceable: 4	coalesced: 4
568 moves: 18	coalesceable: 10	coalesced: 10
569 moves: 6	coalesceable: 6	coalesced: 6
570 moves: 148	coalesceable: 60	coalesced: 56
571 moves: 6	coalesceable: 6	coalesced: 6
572 moves: 112	coalesceable: 76	coalesced: 72
573 moves: 4	coalesceable: 4	coalesced: 4
574 moves: 6	coalesceable: 6	coalesced: 6
575 moves: 4	coalesceable: 4	coalesced: 4
576 moves: 6	coalesceable: 6	coalesced: 6
577 moves: 4	coalesceable: 4	coalesced: 4
578 moves: 6	coalesceable: 6	coalesced: 6
579 moves: 4	coalesceable: 4	coalesced: 4
580 moves: 6	coalesceable: 6	coalesced: 6
581 moves: 4	coalesceable: 4	coalesced: 4
582 moves: 6	coalesceable: 6	coalesced: 6
583 moves: 4	coalesceable: 4	coalesced: 4
584 moves: 6	coalesceable: 6	coalesced: 6
585 moves: 8	coalesceable: 8	coalesced: 8
586 moves: 96	coalesceable: 69	coalesced: 66
587 moves: 6	coalesceable: 6	coalesced: 6
588 moves: 12	coalesceable: 12	coalesced: 12
589 moves: 6	coalesceable: 6	coalesced: 6
590 moves: 76	coalesceable: 44	coalesced: 42
591 moves: 4	coalesceable: 4	coalesced: 4
592 moves: 25	coalesceable: 19	coalesced: 19
593 moves: 6	coalesceable: 6	coalesced: 6
594 moves: 86	coalesceable: 55	coalesced: 53
595 moves: 6	coalesceable: 6	coalesced: 6
596 moves: 77	coalesceable: 49	coalesced: 44
597 moves: 4	coalesceable: 4	coalesced: 4
598 moves: 21	coalesceable: 14	coalesced: 13
599 moves: 4	coalesceable: 4	coalesced: 4
600 moves: 21	coalesceable: 14	coalesced: 13
601 moves: 10	coalesceable: 10	coalesced: 8
602 moves: 3049	coalesceable: 1593	coalesced: 1296
603 moves: 4	coalesceable: 4	coalesced: 4
604 moves: 10	coalesceable: 9	coalesced: 9
605 moves: 6	coalesceable: 6	coalesced: 6
606 moves: 40	coalesceable: 25	coalesced: 24
607 moves: 18	coalesceable: 18	coalesced: 18
608 moves: 91	coalesceable: 53	coalesced: 37
609 moves: 4	coalesceable: 4	coalesced: 4
610 moves: 18	coalesceable: 16	coalesced: 16
611 moves: 4	coalesceable: 4	coalesced: 4
612 moves: 158	coalesceable: 90	coalesced: 87
613 moves: 4	coalesceable: 4	coalesced: 4
614 moves: 111	coalesceable: 80	coalesced: 77
615 moves: 4	coalesceable: 4	coalesced: 4
616 moves: 30	coalesceable: 19	coalesced: 18
617 moves: 4	coalesceable: 4	coalesced: 4
618 moves: 17	coalesceable: 15	coalesced: 15
619 moves: 4	coalesceable: 4	coalesced: 4
620 moves: 12	coalesceable: 11	coalesced: 11
621 moves: 4	coalesceable: 4	coalesced: 4
622 moves: 69	coalesceable: 40	coalesced: 39
623 moves: 6	coalesceable: 6	coalesced: 6
624 moves: 3	coalesceable: 3	coalesced: 2
625 moves: 6	coalesceable: 6	coalesced: 6
626 moves: 37	coalesceable: 22	coalesced: 21
627 moves: 6	coalesceable: 6	coalesced: 6
628 moves: 3	coalesceable: 3	coalesced: 3
629 moves: 6	coalesceable: 6	coalesced: 6
630 moves: 37	coalesceable: 22	coalesced: 21
631 moves: 4	coalesceable: 4	coalesced: 4
632 moves: 55	coalesceable: 35	coalesced: 31
633 moves: 6	coalesceable: 6	coalesced: 6
634 moves: 23	coalesceable: 21	coalesced: 21
635 moves: 4	coalesceable: 4	coalesced: 4
636 moves: 25	coalesceable: 17	coalesced: 16
637 moves: 4	coalesceable: 4	coalesced: 4
638 moves: 77	coalesceable: 51	coalesced: 48
639 moves: 6	coalesceable: 6	coalesced: 6
640 moves: 20	coalesceable: 18	coalesced: 14
641 moves: 38	coalesceable: 25	coalesced: 24
642 moves: 79	coalesceable: 50	coalesced: 47
643 moves: 6	coalesceable: 6	coalesced: 6
644 moves: 85	coalesceable: 57	coalesced: 54
645 moves: 4	coalesceable: 4	coalesced: 4
646 moves: 40	coalesceable: 25	coalesced: 24
647 moves: 6	coalesceable: 6	coalesced: 6
648 moves: 26	coalesceable: 19	coalesced: 19
649 moves: 4	coalesceable: 4	coalesced: 4
650 moves: 21	coalesceable: 14	coalesced: 13
651 moves: 4	coalesceable: 4	coalesced: 4
652 moves: 53	coalesceable: 34	coalesced: 32
653 moves: 167	coalesceable: 107	coalesced: 107
654 moves: 37	coalesceable: 26	coalesced: 25
655 moves: 6	coalesceable: 6	coalesced: 6
656 moves: 34	coalesceable: 23	coalesced: 21
657 moves: 4	coalesceable: 4	coalesced: 4
658 moves: 5	coalesceable: 5	coalesced: 5
659 moves: 38	coalesceable: 25	coalesced: 24
660 moves: 110	coalesceable: 74	coalesced: 72
661 moves: 6	coalesceable: 6	coalesced: 6
662 moves: 34	coalesceable: 23	coalesced: 21
663 moves: 32	coalesceable: 22	coalesced: 22
664 moves: 102	coalesceable: 69	coalesced: 67
665 moves: 6	coalesceable: 6	coalesced: 6
666 moves: 34	coalesceable: 23	coalesced: 21
667 moves: 4	coalesceable: 4	coalesced: 4
668 moves: 5	coalesceable: 5	coalesced: 5
669 moves: 4	coalesceable: 4	coalesced: 4
670 moves: 21	coalesceable: 14	coalesced: 13
671 moves: 4	coalesceable: 4	coalesced: 4
672 moves: 132	coalesceable: 89	coalesced: 80
673 moves: 4	coalesceable: 4	coalesced: 4
674 moves: 88	coalesceable: 59	coalesced: 56
675 moves: 4	coalesceable: 4	coalesced: 4
676 moves: 29	coalesceable: 23	coalesced: 21
677 moves: 4	coalesceable: 4	coalesced: 4
678 moves: 49	coalesceable: 37	coalesced: 37
679 moves: 4	coalesceable: 4	coalesced: 4
680 moves: 5	coalesceable: 5	coalesced: 5
681 moves: 4	coalesceable: 4	coalesced: 4
682 moves: 49	coalesceable: 37	coalesced: 37
683 moves: 4	coalesceable: 4	coalesced: 4
684 moves: 5	coalesceable: 5	coalesced: 5
685 moves: 4	coalesceable: 4	coalesced: 4
686 moves: 5	coalesceable: 5	coalesced: 5
687 moves: 4	coalesceable: 4	coalesced: 4
688 moves: 5	coalesceable: 5	coalesced: 5
689 moves: 4	coalesceable: 4	coalesced: 4
690 moves: 5	coalesceable: 5	coalesced: 5
691 moves: 4	coalesceable: 4	coalesced: 4
692 moves: 5	coalesceable: 5	coalesced: 5
693 moves: 4	coalesceable: 4	coalesced: 4
694 moves: 5	coalesceable: 5	coalesced: 5
695 moves: 4	coalesceable: 4	coalesced: 4
696 moves: 49	coalesceable: 29	coalesced: 28
697 moves: 4	coalesceable: 4	coalesced: 4
698 moves: 116	coalesceable: 73	coalesced: 65
699 moves: 8	coalesceable: 8	coalesced: 8
700 moves: 99	coalesceable: 51	coalesced: 48
701 moves: 4	coalesceable: 4	coalesced: 4
702 moves: 266	coalesceable: 170	coalesced: 166
703 moves: 6	coalesceable: 6	coalesced: 6
704 moves: 503	coalesceable: 392	coalesced: 384
705 moves: 125	coalesceable: 50	coalesced: 45
706 moves: 4	coalesceable: 4	coalesced: 4
707 moves: 210	coalesceable: 128	coalesced: 124
708 moves: 6	coalesceable: 6	coalesced: 6
709 moves: 14	coalesceable: 12	coalesced: 12
710 moves: 6	coalesceable: 6	coalesced: 6
711 moves: 35	coalesceable: 25	coalesced: 22
712 moves: 38	coalesceable: 28	coalesced: 23
713 moves: 4	coalesceable: 4	coalesced: 4
714 moves: 302	coalesceable: 186	coalesced: 181

runtime: 11m14s,    gctime: 1.0s,     systime: 6.2s.
        external oracle real: 11m20s
        external oracle size: 569362
     apply colour (par) eval: runtime: 11m28s,    gctime: 41.6s,     systime: 42.7s.
     apply colour (par) real: 5m16s
     apply colour (par) size: 2183303
           check colour eval: runtime: 30.8s,    gctime: 1.6s,     systime: 0.77314s.
           check colour real: 31.5s
           check colour size: 2184019
          word_to_stack eval: runtime: 6m24s,    gctime: 7.8s,     systime: 7.7s.
          word_to_stack real: 6m32s
          word_to_stack size: 1708852
          stack_rawcall eval: runtime: 3m47s,    gctime: 3.3s,     systime: 4.5s.
          stack_rawcall real: 3m51s
          stack_rawcall size: 1695515
      stack_alloc (par) eval: runtime: 5m32s,    gctime: 4.3s,     systime: 15.9s.
      stack_alloc (par) real: 2m04s
      stack_alloc (par) size: 1711964
expand stack_remove_def eval: runtime: 0.07623s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.07627s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 6m54s,    gctime: 5.9s,     systime: 12.9s.
     stack_remove (par) real: 2m08s
     stack_remove (par) size: 2813880
      stack_names (par) eval: runtime: 3m52s,    gctime: 5.6s,     systime: 6.3s.
      stack_names (par) real: 1m25s
      stack_names (par) size: 2907898
     stack_to_lab (par) eval: runtime: 8m25s,    gctime: 36.2s,     systime: 15.0s.
     stack_to_lab (par) real: 3m22s
     stack_to_lab (par) size: 3548641
          lab_to_target eval: runtime: 18m50s,    gctime: 1m46s,     systime: 21.6s.
          lab_to_target real: 19m12s
          lab_to_target size: 5501916
                      export: runtime: 1.3s,    gctime: 0.00000s,     systime: 0.03663s.
Saved theorem _____ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 2h05m21s to build
cc grep.S /root/regression/cakeml-1635/basis/basis_ffi.o  -o cake_grep
Linking /root/regression/cakeml-1635/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 47.7s,    gctime: 1.1s,     systime: 1.1s.
                to_flat real: 48.8s
                to_flat size: 91230
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.37255s,    gctime: 0.00000s,     systime: 0.00330s.
                to_clos real: 0.37574s
                to_clos size: 34782
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 8.6s,    gctime: 0.27665s,     systime: 0.04321s.
                 to_bvl real: 8.6s
                 to_bvl size: 56508
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 1m25s,    gctime: 0.63273s,     systime: 0.67973s.
                 to_bvi real: 1m26s
                 to_bvi size: 64384
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 20.7s,    gctime: 0.90798s,     systime: 0.28316s.
                to_data real: 21.0s
                to_data size: 112704
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 28.8s,    gctime: 1.0s,     systime: 0.32347s.
           data_to_word real: 29.1s
           data_to_word size: 388693
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m03s,    gctime: 5.1s,     systime: 8.1s.
 inst,ssa,two-reg (par) real: 1m09s
 inst,ssa,two-reg (par) size: 1202030
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 1m18s,    gctime: 23.8s,     systime: 5.0s.
        get_clash (par) real: 43.9s
        get_clash (par) size: 1871370
        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: 960	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 12	coalesced: 12
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: 4375	coalesceable: 2573	coalesced: 2573
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: 10	coalesceable: 6	coalesced: 6
138 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 5	coalesceable: 3	coalesced: 3
146 moves: 4	coalesceable: 4	coalesced: 4
147 moves: 9	coalesceable: 9	coalesced: 8
148 moves: 8	coalesceable: 8	coalesced: 8
149 moves: 124	coalesceable: 72	coalesced: 58
150 moves: 6	coalesceable: 6	coalesced: 6
151 moves: 23	coalesceable: 15	coalesced: 11
152 moves: 6	coalesceable: 6	coalesced: 6
153 moves: 23	coalesceable: 15	coalesced: 11
154 moves: 6	coalesceable: 6	coalesced: 6
155 moves: 30	coalesceable: 19	coalesced: 16
156 moves: 6	coalesceable: 6	coalesced: 6
157 moves: 29	coalesceable: 21	coalesced: 17
158 moves: 6	coalesceable: 6	coalesced: 6
159 moves: 24	coalesceable: 16	coalesced: 13
160 moves: 6	coalesceable: 6	coalesced: 6
161 moves: 24	coalesceable: 16	coalesced: 13
162 moves: 6	coalesceable: 6	coalesced: 6
163 moves: 30	coalesceable: 22	coalesced: 19
164 moves: 4	coalesceable: 4	coalesced: 4
165 moves: 25	coalesceable: 18	coalesced: 16
166 moves: 4	coalesceable: 4	coalesced: 4
167 moves: 3	coalesceable: 3	coalesced: 3
168 moves: 6	coalesceable: 6	coalesced: 6
169 moves: 21	coalesceable: 19	coalesced: 19
170 moves: 8	coalesceable: 8	coalesced: 8
171 moves: 22	coalesceable: 20	coalesced: 20
172 moves: 12	coalesceable: 12	coalesced: 12
173 moves: 218	coalesceable: 134	coalesced: 94
174 moves: 8	coalesceable: 8	coalesced: 8
175 moves: 163	coalesceable: 110	coalesced: 96
176 moves: 6	coalesceable: 6	coalesced: 6
177 moves: 114	coalesceable: 80	coalesced: 72
178 moves: 4	coalesceable: 4	coalesced: 4
179 moves: 6	coalesceable: 6	coalesced: 6
180 moves: 8	coalesceable: 8	coalesced: 8
181 moves: 128	coalesceable: 77	coalesced: 70
182 moves: 8	coalesceable: 8	coalesced: 8
183 moves: 111	coalesceable: 66	coalesced: 51
184 moves: 6	coalesceable: 6	coalesced: 6
185 moves: 427	coalesceable: 263	coalesced: 198
186 moves: 4	coalesceable: 4	coalesced: 4
187 moves: 5	coalesceable: 5	coalesced: 5
188 moves: 4	coalesceable: 4	coalesced: 4
189 moves: 64	coalesceable: 47	coalesced: 47

runtime: 19.7s,    gctime: 0.05420s,     systime: 0.17975s.
        external oracle real: 19.8s
        external oracle size: 134303
     apply colour (par) eval: runtime: 2m35s,    gctime: 5.5s,     systime: 18.7s.
     apply colour (par) real: 1m49s
     apply colour (par) size: 594449
           check colour eval: runtime: 2.0s,    gctime: 0.35306s,     systime: 0.08991s.
           check colour real: 2.1s
           check colour size: 594640
          word_to_stack eval: runtime: 2m00s,    gctime: 3.2s,     systime: 1.7s.
          word_to_stack real: 2m02s
          word_to_stack size: 488695
          stack_rawcall eval: runtime: 1m04s,    gctime: 1.3s,     systime: 0.90944s.
          stack_rawcall real: 1m05s
          stack_rawcall size: 482597
      stack_alloc (par) eval: runtime: 1m29s,    gctime: 1.5s,     systime: 7.7s.
      stack_alloc (par) real: 49.1s
      stack_alloc (par) size: 483879
expand stack_remove_def eval: runtime: 0.08367s,    gctime: 0.00000s,     systime: 0.00335s.
expand stack_remove_def real: 0.08706s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m04s,    gctime: 2.6s,     systime: 8.9s.
     stack_remove (par) real: 1m18s
     stack_remove (par) size: 828886
      stack_names (par) eval: runtime: 1m01s,    gctime: 1.6s,     systime: 2.9s.
      stack_names (par) real: 32.3s
      stack_names (par) size: 855449
     stack_to_lab (par) eval: runtime: 2m05s,    gctime: 3.3s,     systime: 7.4s.
     stack_to_lab (par) real: 1m06s
     stack_to_lab (par) size: 1038464
          lab_to_target eval: runtime: 7m01s,    gctime: 18.9s,     systime: 10.3s.
          lab_to_target real: 7m11s
          lab_to_target size: 1736663
                      export: runtime: 0.81599s,    gctime: 0.10464s,     systime: 0.02679s.
Saved theorem _____ "hello_compiled"
Exporting theory "helloCompile" ... done.
Theory "helloCompile" took 28m04s to build
cc hello.S /root/regression/cakeml-1635/basis/basis_ffi.o  -o cake_hello
Linking /root/regression/cakeml-1635/examples/compilation/x64/helloErrCompileScript.uo to produce theory-builder executable
/root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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 (...) |
     (...) => ... ... |
     ... => ... |
     ...
/root/regression/cakeml-1635/compiler/compilationLib.sml:711: 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: 47.5s,    gctime: 0.97835s,     systime: 0.98057s.
                to_flat real: 48.5s
                to_flat size: 92261
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.39027s,    gctime: 0.00000s,     systime: 0.00001s.
                to_clos real: 0.39024s
                to_clos size: 35437
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 8.2s,    gctime: 0.24939s,     systime: 0.04673s.
                 to_bvl real: 8.2s
                 to_bvl size: 58153
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
                 to_bvi eval: runtime: 1m27s,    gctime: 0.60220s,     systime: 0.74319s.
                 to_bvi real: 1m28s
                 to_bvi size: 65979
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
                to_data eval: runtime: 20.7s,    gctime: 0.88591s,     systime: 0.27670s.
                to_data real: 21.0s
                to_data size: 114735
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 28.9s,    gctime: 1.0s,     systime: 0.25005s.
           data_to_word real: 29.1s
           data_to_word size: 392905
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m01s,    gctime: 4.8s,     systime: 6.2s.
 inst,ssa,two-reg (par) real: 1m07s
 inst,ssa,two-reg (par) size: 1209945
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 1m19s,    gctime: 22.4s,     systime: 5.9s.
        get_clash (par) real: 41.9s
        get_clash (par) size: 1882211
        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: 960	coalesceable: 2	coalesced: 2
118 moves: 17	coalesceable: 12	coalesced: 12
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: 4375	coalesceable: 2573	coalesced: 2573
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: 10	coalesceable: 6	coalesced: 6
140 moves: 60	coalesceable: 41	coalesced: 40
141 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 5	coalesceable: 3	coalesced: 3
149 moves: 4	coalesceable: 4	coalesced: 4
150 moves: 69	coalesceable: 44	coalesced: 38
151 moves: 4	coalesceable: 4	coalesced: 4
152 moves: 3	coalesceable: 3	coalesced: 3
153 moves: 4	coalesceable: 4	coalesced: 4
154 moves: 9	coalesceable: 9	coalesced: 8
155 moves: 8	coalesceable: 8	coalesced: 8
156 moves: 124	coalesceable: 72	coalesced: 58
157 moves: 6	coalesceable: 6	coalesced: 6
158 moves: 23	coalesceable: 15	coalesced: 11
159 moves: 6	coalesceable: 6	coalesced: 6
160 moves: 23	coalesceable: 15	coalesced: 11
161 moves: 6	coalesceable: 6	coalesced: 6
162 moves: 30	coalesceable: 19	coalesced: 16
163 moves: 6	coalesceable: 6	coalesced: 6
164 moves: 29	coalesceable: 21	coalesced: 17
165 moves: 6	coalesceable: 6	coalesced: 6
166 moves: 24	coalesceable: 16	coalesced: 13
167 moves: 6	coalesceable: 6	coalesced: 6
168 moves: 24	coalesceable: 16	coalesced: 13
169 moves: 6	coalesceable: 6	coalesced: 6
170 moves: 30	coalesceable: 22	coalesced: 19
171 moves: 4	coalesceable: 4	coalesced: 4
172 moves: 25	coalesceable: 18	coalesced: 16
173 moves: 4	coalesceable: 4	coalesced: 4
174 moves: 3	coalesceable: 3	coalesced: 3
175 moves: 6	coalesceable: 6	coalesced: 6
176 moves: 21	coalesceable: 19	coalesced: 19
177 moves: 8	coalesceable: 8	coalesced: 8
178 moves: 22	coalesceable: 20	coalesced: 20
179 moves: 12	coalesceable: 12	coalesced: 12
180 moves: 218	coalesceable: 134	coalesced: 94
181 moves: 8	coalesceable: 8	coalesced: 8
182 moves: 163	coalesceable: 110	coalesced: 96
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 114	coalesceable: 80	coalesced: 72
185 moves: 4	coalesceable: 4	coalesced: 4
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 8	coalesceable: 8	coalesced: 8
188 moves: 128	coalesceable: 77	coalesced: 70
189 moves: 8	coalesceable: 8	coalesced: 8
190 moves: 111	coalesceable: 66	coalesced: 51
191 moves: 6	coalesceable: 6	coalesced: 6
192 moves: 427	coalesceable: 263	coalesced: 198
193 moves: 4	coalesceable: 4	coalesced: 4
194 moves: 5	coalesceable: 5	coalesced: 5
195 moves: 4	coalesceable: 4	coalesced: 4
196 moves: 71	coalesceable: 51	coalesced: 51

runtime: 18.6s,    gctime: 0.06248s,     systime: 0.29009s.
        external oracle real: 18.9s
        external oracle size: 135446
     apply colour (par) eval: runtime: 2m32s,    gctime: 6.2s,     systime: 10.0s.
     apply colour (par) real: 1m39s
     apply colour (par) size: 599534
           check colour eval: runtime: 1.7s,    gctime: 0.00000s,     systime: 0.00009s.
           check colour real: 1.7s
           check colour size: 599732
          word_to_stack eval: runtime: 2m02s,    gctime: 3.9s,     systime: 2.3s.
          word_to_stack real: 2m04s
          word_to_stack size: 492392
          stack_rawcall eval: runtime: 1m04s,    gctime: 1.2s,     systime: 0.50325s.
          stack_rawcall real: 1m05s
          stack_rawcall size: 486205
      stack_alloc (par) eval: runtime: 1m27s,    gctime: 1.6s,     systime: 4.1s.
      stack_alloc (par) real: 45.2s
      stack_alloc (par) size: 487547
expand stack_remove_def eval: runtime: 0.07762s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.07766s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m04s,    gctime: 3.0s,     systime: 8.9s.
     stack_remove (par) real: 1m17s
     stack_remove (par) size: 834357
      stack_names (par) eval: runtime: 1m04s,    gctime: 2.0s,     systime: 7.7s.
      stack_names (par) real: 36.5s
      stack_names (par) size: 861142
     stack_to_lab (par) eval: runtime: 2m06s,    gctime: 3.8s,     systime: 4.8s.
     stack_to_lab (par) real: 1m05s
     stack_to_lab (par) size: 1045559
          lab_to_target eval: runtime: 7m09s,    gctime: 26.0s,     systime: 4.7s.
          lab_to_target real: 7m14s
          lab_to_target size: 1749099
                      export: runtime: 0.91272s,    gctime: 0.19738s,     systime: 0.02648s.
Saved theorem _____ "helloErr_compiled"
Exporting theory "helloErrCompile" ... Run out of store - interrupting threads

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