Job 1887

CakeML:de55558c0ff9912b7dc6c9fe2b229b8a90584e15
  Fix non-merged file [May 03 16:13:08]
#865 (Iced_cake)
Merging into:d49028c882e2061b0b85fe1f775e9d1c157b9b23
  Merge pull request #882 from mktnk3/time_to_pan_cleanup [May 02 07:00:59]
HOL:9ef7738eaecdb725492f0929f6b270d1f4e63a40
  Teach Holmake and Parse.sml about the tmux terminal [Apr 28 21:56:05]
Machine:oven3

May 04 13:37:31 Claimed job
May 04 13:37:36 Reusing HOL
May 04 13:38:31 Starting developers
May 04 13:38:41 Finished developers                                              10s  83MB
May 04 13:38:41 Starting developers/bin
May 04 13:38:55 Finished developers/bin                                          13s   1GB
May 04 13:38:55 Starting semantics/ffi
May 04 13:39:23 Finished semantics/ffi                                           27s 252MB
May 04 13:39:23 Starting semantics
May 04 13:44:21 Finished semantics                                             4m57s   1GB
May 04 13:44:21 Starting semantics/proofs
May 04 13:59:53 Finished semantics/proofs                                     15m31s   1GB
May 04 13:59:53 Starting semantics/alt_semantics
May 04 14:00:51 Finished semantics/alt_semantics                                 57s 542MB
May 04 14:00:51 Starting semantics/alt_semantics/proofs
May 04 14:26:17 Finished semantics/alt_semantics/proofs                       25m26s   1GB
May 04 14:26:18 Starting basis/pure
May 04 14:28:35 Finished basis/pure                                            2m17s   1GB
May 04 14:28:36 Starting translator
May 04 14:36:29 Finished translator                                            7m53s   1GB
May 04 14:36:29 Starting compiler/parsing
May 04 14:39:28 Finished compiler/parsing                                      2m57s   5GB
May 04 14:39:28 Starting characteristic
May 04 14:54:12 Finished characteristic                                       14m43s   2GB
May 04 14:54:12 Starting translator/monadic
May 04 14:58:16 Finished translator/monadic                                    4m04s   1GB
May 04 14:58:17 Starting basis
May 04 16:51:47 Finished basis                                              1h53m30s   9GB
May 04 16:51:47 Starting compiler/inference
May 04 16:55:02 Finished compiler/inference                                    3m14s   1GB
May 04 16:55:02 Starting compiler/backend/reg_alloc
May 04 16:58:17 Finished compiler/backend/reg_alloc                            3m15s   1GB
May 04 16:58:18 Starting compiler/backend/gc
May 04 17:07:01 Finished compiler/backend/gc                                   8m42s   2GB
May 04 17:07:01 Starting compiler/backend
May 04 17:18:50 Finished compiler/backend                                     11m49s   2GB
May 04 17:18:50 Starting compiler/encoders/asm
May 04 17:19:57 Finished compiler/encoders/asm                                 1m06s 989MB
May 04 17:19:57 Starting compiler/encoders/x64
May 04 17:21:04 Finished compiler/encoders/x64                                 1m06s   1GB
May 04 17:21:04 Starting compiler/encoders/arm7
May 04 17:23:10 Finished compiler/encoders/arm7                                2m05s   1GB
May 04 17:23:10 Starting compiler/encoders/arm8
May 04 17:23:49 Finished compiler/encoders/arm8                                  38s   1GB
May 04 17:23:49 Starting compiler/encoders/arm8_asl
May 04 17:31:23 Finished compiler/encoders/arm8_asl                            7m33s   1GB
May 04 17:31:23 Starting compiler/encoders/mips
May 04 17:32:10 Finished compiler/encoders/mips                                  46s   1GB
May 04 17:32:10 Starting compiler/encoders/riscv
May 04 17:32:55 Finished compiler/encoders/riscv                                 44s 901MB
May 04 17:32:55 Starting compiler/encoders/ag32
May 04 17:33:44 Finished compiler/encoders/ag32                                  48s 654MB
May 04 17:33:44 Starting compiler/backend/x64
May 04 17:34:33 Finished compiler/backend/x64                                    48s   1GB
May 04 17:34:33 Starting compiler/backend/arm7
May 04 17:35:25 Finished compiler/backend/arm7                                   51s   1GB
May 04 17:35:26 Starting compiler/backend/arm8
May 04 17:36:15 Finished compiler/backend/arm8                                   49s   1GB
May 04 17:36:15 Starting compiler/backend/mips
May 04 17:37:06 Finished compiler/backend/mips                                   50s   1GB
May 04 17:37:06 Starting compiler/backend/riscv
May 04 17:37:53 Finished compiler/backend/riscv                                  47s   1GB
May 04 17:37:54 Starting compiler/backend/ag32
May 04 17:40:50 Finished compiler/backend/ag32                                 2m56s   1GB
May 04 17:40:50 Starting compiler/parsing/proofs
May 04 17:49:31 Finished compiler/parsing/proofs                               8m40s   1GB
May 04 17:49:31 Starting compiler/inference/proofs
May 04 17:55:41 Finished compiler/inference/proofs                             6m09s   1GB
May 04 17:55:41 Starting compiler/backend/semantics
May 04 19:07:48 Finished compiler/backend/semantics                         1h12m06s   3GB
May 04 19:07:48 Starting compiler/backend/reg_alloc/proofs
May 04 19:15:54 Finished compiler/backend/reg_alloc/proofs                     8m04s   1GB
May 04 19:15:54 Starting compiler/backend/proofs
May 04 21:10:06 Finished compiler/backend/proofs                            1h54m12s  15GB
May 04 21:10:07 Starting compiler/backend/serialiser
May 04 21:13:40 Finished compiler/backend/serialiser                           3m32s   2GB
May 04 21:13:40 Starting compiler/encoders/x64/proofs
May 04 21:35:13 Finished compiler/encoders/x64/proofs                         21m33s   4GB
May 04 21:35:14 Starting compiler/encoders/arm7/proofs
May 04 22:04:40 Finished compiler/encoders/arm7/proofs                        29m25s   3GB
May 04 22:04:40 Starting compiler/encoders/arm8/proofs
May 04 22:20:04 Finished compiler/encoders/arm8/proofs                        15m22s   1GB
May 04 22:20:04 Starting compiler/encoders/arm8_asl/proofs
May 04 22:57:00 Finished compiler/encoders/arm8_asl/proofs                    36m56s   1GB
May 04 22:57:01 Starting compiler/encoders/mips/proofs
May 04 23:19:37 Finished compiler/encoders/mips/proofs                        22m36s   2GB
May 04 23:19:37 Starting compiler/encoders/riscv/proofs
May 04 23:39:30 Finished compiler/encoders/riscv/proofs                       19m52s   1GB
May 04 23:39:30 Starting compiler/encoders/ag32/proofs
May 04 23:45:12 Finished compiler/encoders/ag32/proofs                         5m41s   1GB
May 04 23:45:13 Starting compiler/backend/x64/proofs
May 04 23:46:17 Finished compiler/backend/x64/proofs                           1m04s   1GB
May 04 23:46:17 Starting compiler/backend/arm7/proofs
May 04 23:47:26 Finished compiler/backend/arm7/proofs                          1m08s   1GB
May 04 23:47:26 Starting compiler/backend/arm8/proofs
May 04 23:48:30 Finished compiler/backend/arm8/proofs                          1m03s   1GB
May 04 23:48:30 Starting compiler/backend/arm8_asl
May 04 23:49:20 Finished compiler/backend/arm8_asl                               49s   1GB
May 04 23:49:20 Starting compiler/backend/mips/proofs
May 04 23:50:21 Finished compiler/backend/mips/proofs                          1m01s   1GB
May 04 23:50:22 Starting compiler/backend/riscv/proofs
May 04 23:51:25 Finished compiler/backend/riscv/proofs                         1m03s   1GB
May 04 23:51:25 Starting compiler/backend/ag32/proofs
May 05 00:22:52 Finished compiler/backend/ag32/proofs                         31m27s   2GB
May 05 00:22:52 Starting compiler/proofs
May 05 00:27:42 Finished compiler/proofs                                       4m49s   3GB
May 05 00:27:42 Starting candle/set-theory
May 05 00:28:53 Finished candle/set-theory                                     1m10s   1GB
May 05 00:28:54 Starting candle/syntax-lib
May 05 00:29:22 Finished candle/syntax-lib                                       28s 655MB
May 05 00:29:22 Starting candle/standard/syntax
May 05 00:33:59 Finished candle/standard/syntax                                4m36s   1GB
May 05 00:33:59 Starting candle/standard/semantics
May 05 00:38:04 Finished candle/standard/semantics                             4m04s   1GB
May 05 00:38:04 Starting candle/standard/monadic
May 05 00:42:21 Finished candle/standard/monadic                               4m16s   1GB
May 05 00:42:21 Starting candle/standard/ml_kernel
May 05 00:56:48 Finished candle/standard/ml_kernel                            14m26s   3GB
May 05 00:56:48 Starting candle/overloading/syntax
May 05 01:04:10 Finished candle/overloading/syntax                             7m22s   1GB
May 05 01:04:11 Starting candle/overloading/semantics
May 05 01:32:06 Finished candle/overloading/semantics                         27m54s   2GB
May 05 01:32:06 Starting candle/overloading/monadic
May 05 01:37:49 Finished candle/overloading/monadic                            5m43s   1GB
May 05 01:37:49 Starting candle/overloading/ml_kernel
May 05 01:53:35 Finished candle/overloading/ml_kernel                         15m45s   3GB
May 05 01:53:35 Starting candle/overloading/ml_checker
May 05 01:58:52 Finished candle/overloading/ml_checker                         5m16s   3GB
May 05 01:58:52 Starting candle/prover
May 05 02:25:40 Finished candle/prover                                        26m47s   3GB
May 05 02:25:40 Starting pancake
May 05 02:33:16 Finished pancake                                               7m35s   3GB
May 05 02:33:16 Starting pancake/ffi
May 05 02:33:17 Finished pancake/ffi                                              0s  29MB
May 05 02:33:17 Starting pancake/semantics
May 05 02:39:12 Finished pancake/semantics                                     5m55s   1GB
May 05 02:39:12 Starting pancake/proofs
May 05 03:06:29 Finished pancake/proofs                                       27m16s   6GB
May 05 03:06:29 Starting characteristic/examples
May 05 03:09:33 Finished characteristic/examples                               3m03s   2GB
May 05 03:09:33 Starting tutorial/solutions
May 05 03:48:46 Finished tutorial/solutions                                   39m13s   7GB
May 05 03:48:47 Starting translator/monadic/examples
May 05 03:56:13 Finished translator/monadic/examples                           7m25s   2GB
May 05 03:56:13 Starting examples
May 05 04:16:04 Finished examples                                             19m51s   4GB
May 05 04:16:05 Starting examples/compilation/x64
May 05 07:32:21 FAILED: examples/compilation/x64
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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/hol88[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
Scanned 75 directories
/root/regression/cakeml-1887/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-1887/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/root/regression/HOL-9ef7738eaecdb725492f0929f6b270d1f4e63a40/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-1887/compiler/compilationLib.sml:714: 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: 28.9s,    gctime: 0.68555s,     systime: 0.78648s.
                to_flat real: 29.6s
                to_flat size: 81058
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.65825s,    gctime: 0.00000s,     systime: 0.00008s.
                to_clos real: 0.65809s
                to_clos size: 47193
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 11.2s,    gctime: 0.27104s,     systime: 0.05664s.
                 to_bvl real: 11.3s
                 to_bvl size: 79642
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 1m35s,    gctime: 0.52125s,     systime: 0.83878s.
                 to_bvi real: 1m36s
                 to_bvi size: 85205
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 25.1s,    gctime: 0.96442s,     systime: 0.24995s.
                to_data real: 25.3s
                to_data size: 134492
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 31.3s,    gctime: 1.2s,     systime: 0.41662s.
           data_to_word real: 31.7s
           data_to_word size: 408905
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m19s,    gctime: 5.1s,     systime: 7.7s.
 inst,ssa,two-reg (par) real: 1m10s
 inst,ssa,two-reg (par) size: 1297263
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 1m28s,    gctime: 22.8s,     systime: 8.8s.
        get_clash (par) real: 43.7s
        get_clash (par) size: 2011329
        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: 80	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: 72	coalesceable: 44	coalesced: 43
136 moves: 17	coalesceable: 11	coalesced: 11
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 4375	coalesceable: 2573	coalesced: 2573
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: 10	coalesceable: 6	coalesced: 6
158 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
170 moves: 17	coalesceable: 11	coalesced: 11
171 moves: 17	coalesceable: 11	coalesced: 11
172 moves: 17	coalesceable: 11	coalesced: 11
173 moves: 5	coalesceable: 3	coalesced: 3
174 moves: 6	coalesceable: 6	coalesced: 6
175 moves: 29	coalesceable: 19	coalesced: 13
176 moves: 4	coalesceable: 4	coalesced: 4
177 moves: 7	coalesceable: 7	coalesced: 7
178 moves: 4	coalesceable: 4	coalesced: 4
179 moves: 9	coalesceable: 9	coalesced: 8
180 moves: 8	coalesceable: 8	coalesced: 8
181 moves: 124	coalesceable: 72	coalesced: 58
182 moves: 6	coalesceable: 6	coalesced: 6
183 moves: 62	coalesceable: 31	coalesced: 29
184 moves: 4	coalesceable: 4	coalesced: 4
185 moves: 48	coalesceable: 23	coalesced: 21
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 23	coalesceable: 15	coalesced: 11
188 moves: 6	coalesceable: 6	coalesced: 6
189 moves: 23	coalesceable: 15	coalesced: 11
190 moves: 6	coalesceable: 6	coalesced: 6
191 moves: 30	coalesceable: 19	coalesced: 16
192 moves: 6	coalesceable: 6	coalesced: 6
193 moves: 29	coalesceable: 21	coalesced: 17
194 moves: 6	coalesceable: 6	coalesced: 6
195 moves: 24	coalesceable: 16	coalesced: 13
196 moves: 6	coalesceable: 6	coalesced: 6
197 moves: 24	coalesceable: 16	coalesced: 13
198 moves: 6	coalesceable: 6	coalesced: 6
199 moves: 30	coalesceable: 22	coalesced: 19
200 moves: 6	coalesceable: 6	coalesced: 6
201 moves: 30	coalesceable: 22	coalesced: 19
202 moves: 6	coalesceable: 6	coalesced: 6
203 moves: 62	coalesceable: 31	coalesced: 29
204 moves: 4	coalesceable: 4	coalesced: 4
205 moves: 3	coalesceable: 3	coalesced: 3
206 moves: 4	coalesceable: 4	coalesced: 4
207 moves: 43	coalesceable: 29	coalesced: 25
208 moves: 4	coalesceable: 4	coalesced: 4
209 moves: 3	coalesceable: 3	coalesced: 3
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 18	coalesceable: 16	coalesced: 16
212 moves: 4	coalesceable: 4	coalesced: 4
213 moves: 25	coalesceable: 18	coalesced: 16
214 moves: 4	coalesceable: 4	coalesced: 4
215 moves: 3	coalesceable: 3	coalesced: 3
216 moves: 6	coalesceable: 6	coalesced: 6
217 moves: 36	coalesceable: 23	coalesced: 17
218 moves: 6	coalesceable: 6	coalesced: 6
219 moves: 21	coalesceable: 19	coalesced: 19
220 moves: 8	coalesceable: 8	coalesced: 8
221 moves: 22	coalesceable: 20	coalesced: 20
222 moves: 12	coalesceable: 12	coalesced: 12
223 moves: 218	coalesceable: 134	coalesced: 94
224 moves: 8	coalesceable: 8	coalesced: 8
225 moves: 124	coalesceable: 72	coalesced: 58
226 moves: 4	coalesceable: 4	coalesced: 4
227 moves: 77	coalesceable: 56	coalesced: 53
228 moves: 6	coalesceable: 6	coalesced: 6
229 moves: 110	coalesceable: 79	coalesced: 69
230 moves: 8	coalesceable: 8	coalesced: 8
231 moves: 407	coalesceable: 208	coalesced: 175
232 moves: 4	coalesceable: 4	coalesced: 4
233 moves: 56	coalesceable: 33	coalesced: 30
234 moves: 4	coalesceable: 4	coalesced: 4
235 moves: 8	coalesceable: 6	coalesced: 6
236 moves: 8	coalesceable: 8	coalesced: 8
237 moves: 163	coalesceable: 110	coalesced: 96
238 moves: 6	coalesceable: 6	coalesced: 6
239 moves: 114	coalesceable: 80	coalesced: 72
240 moves: 4	coalesceable: 4	coalesced: 4
241 moves: 6	coalesceable: 6	coalesced: 6
242 moves: 4	coalesceable: 4	coalesced: 4
243 moves: 6	coalesceable: 6	coalesced: 6
244 moves: 8	coalesceable: 8	coalesced: 8
245 moves: 128	coalesceable: 77	coalesced: 70
246 moves: 8	coalesceable: 8	coalesced: 8
247 moves: 111	coalesceable: 66	coalesced: 51
248 moves: 6	coalesceable: 6	coalesced: 6
249 moves: 50	coalesceable: 38	coalesced: 35
250 moves: 6	coalesceable: 6	coalesced: 6
251 moves: 427	coalesceable: 263	coalesced: 198
252 moves: 4	coalesceable: 4	coalesced: 4
253 moves: 5	coalesceable: 5	coalesced: 5
254 moves: 4	coalesceable: 4	coalesced: 4
255 moves: 272	coalesceable: 139	coalesced: 131
256 moves: 4	coalesceable: 4	coalesced: 4
257 moves: 69	coalesceable: 54	coalesced: 54
258 moves: 6	coalesceable: 6	coalesced: 6
259 moves: 54	coalesceable: 41	coalesced: 38
260 moves: 4	coalesceable: 4	coalesced: 4
261 moves: 21	coalesceable: 18	coalesced: 16
262 moves: 4	coalesceable: 4	coalesced: 4
263 moves: 15	coalesceable: 12	coalesced: 12
264 moves: 25	coalesceable: 21	coalesced: 21
265 moves: 24	coalesceable: 15	coalesced: 15
266 moves: 4	coalesceable: 4	coalesced: 4
267 moves: 34	coalesceable: 19	coalesced: 17
268 moves: 4	coalesceable: 4	coalesced: 4
269 moves: 16	coalesceable: 11	coalesced: 10
270 moves: 4	coalesceable: 4	coalesced: 4
271 moves: 11	coalesceable: 7	coalesced: 7

runtime: 17.8s,    gctime: 0.03313s,     systime: 0.46308s.
        external oracle real: 18.2s
        external oracle size: 148063
     apply colour (par) eval: runtime: 2m43s,    gctime: 3.9s,     systime: 12.6s.
     apply colour (par) real: 1m39s
     apply colour (par) size: 653969
           check colour eval: runtime: 2.0s,    gctime: 0.00000s,     systime: 0.07989s.
           check colour real: 2.1s
           check colour size: 654242
          word_to_stack eval: runtime: 1m52s,    gctime: 2.0s,     systime: 1.7s.
          word_to_stack real: 1m54s
          word_to_stack size: 545672
          stack_rawcall eval: runtime: 1m09s,    gctime: 0.88068s,     systime: 0.98271s.
          stack_rawcall real: 1m10s
          stack_rawcall size: 531147
      stack_alloc (par) eval: runtime: 1m39s,    gctime: 1.2s,     systime: 7.2s.
      stack_alloc (par) real: 48.6s
      stack_alloc (par) size: 533137
expand stack_remove_def eval: runtime: 0.07576s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.07581s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m13s,    gctime: 1.6s,     systime: 5.3s.
     stack_remove (par) real: 1m13s
     stack_remove (par) size: 904703
      stack_names (par) eval: runtime: 1m08s,    gctime: 1.3s,     systime: 3.6s.
      stack_names (par) real: 34.3s
      stack_names (par) size: 933448
     stack_to_lab (par) eval: runtime: 2m16s,    gctime: 2.3s,     systime: 2.1s.
     stack_to_lab (par) real: 1m02s
     stack_to_lab (par) size: 1137272
          lab_to_target eval: runtime: 8m37s,    gctime: 13.0s,     systime: 5.1s.
          lab_to_target real: 8m42s
          lab_to_target size: 1892860
                      export: runtime: 0.93886s,    gctime: 0.13040s,     systime: 0.05330s.
Saved theorem _______ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 30m37s to build
Linking /root/regression/cakeml-1887/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/root/regression/HOL-9ef7738eaecdb725492f0929f6b270d1f4e63a40/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-1887/compiler/compilationLib.sml:714: 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: 31.4s,    gctime: 0.64514s,     systime: 0.72301s.
                to_flat real: 32.1s
                to_flat size: 128212
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 1.6s,    gctime: 0.14673s,     systime: 0.02671s.
                to_clos real: 1.6s
                to_clos size: 69111
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 15.0s,    gctime: 0.42616s,     systime: 0.11345s.
                 to_bvl real: 15.2s
                 to_bvl size: 123714
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 1m55s,    gctime: 0.72842s,     systime: 0.96568s.
                 to_bvi real: 1m56s
                 to_bvi size: 123389
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 29.8s,    gctime: 1.1s,     systime: 0.34670s.
                to_data real: 30.2s
                to_data size: 194553
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 39.8s,    gctime: 1.2s,     systime: 0.43999s.
           data_to_word real: 40.3s
           data_to_word size: 545668
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 3m12s,    gctime: 8.5s,     systime: 4.9s.
 inst,ssa,two-reg (par) real: 1m11s
 inst,ssa,two-reg (par) size: 1647340
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 2m36s,    gctime: 25.0s,     systime: 11.3s.
        get_clash (par) real: 50.2s
        get_clash (par) size: 2576805
        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: 112	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: 2	coalesceable: 2	coalesced: 2
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: 72	coalesceable: 44	coalesced: 43
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 17	coalesceable: 11	coalesced: 11
153 moves: 4375	coalesceable: 2573	coalesced: 2573
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: 17	coalesceable: 11	coalesced: 11
171 moves: 17	coalesceable: 11	coalesced: 11
172 moves: 10	coalesceable: 6	coalesced: 6
173 moves: 60	coalesceable: 41	coalesced: 40
174 moves: 60	coalesceable: 41	coalesced: 40
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: 17	coalesceable: 11	coalesced: 11
187 moves: 17	coalesceable: 11	coalesced: 11
188 moves: 2	coalesceable: 2	coalesced: 2
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: 17	coalesceable: 11	coalesced: 11
205 moves: 17	coalesceable: 11	coalesced: 11
206 moves: 114	coalesceable: 84	coalesced: 84
207 moves: 17	coalesceable: 11	coalesced: 11
208 moves: 17	coalesceable: 11	coalesced: 11
209 moves: 5	coalesceable: 3	coalesced: 3
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 6	coalesceable: 6	coalesced: 6
212 moves: 4	coalesceable: 4	coalesced: 4
213 moves: 6	coalesceable: 6	coalesced: 6
214 moves: 6	coalesceable: 6	coalesced: 6
215 moves: 29	coalesceable: 19	coalesced: 13
216 moves: 6	coalesceable: 6	coalesced: 6
217 moves: 32	coalesceable: 23	coalesced: 18
218 moves: 4	coalesceable: 4	coalesced: 4
219 moves: 5	coalesceable: 5	coalesced: 3
220 moves: 6	coalesceable: 6	coalesced: 6
221 moves: 36	coalesceable: 25	coalesced: 24
222 moves: 4	coalesceable: 4	coalesced: 4
223 moves: 5	coalesceable: 5	coalesced: 3
224 moves: 4	coalesceable: 4	coalesced: 4
225 moves: 7	coalesceable: 7	coalesced: 7
226 moves: 4	coalesceable: 4	coalesced: 4
227 moves: 7	coalesceable: 7	coalesced: 7
228 moves: 4	coalesceable: 4	coalesced: 4
229 moves: 12	coalesceable: 11	coalesced: 10
230 moves: 6	coalesceable: 6	coalesced: 6
231 moves: 86	coalesceable: 57	coalesced: 51
232 moves: 6	coalesceable: 6	coalesced: 6
233 moves: 76	coalesceable: 47	coalesced: 43
234 moves: 4	coalesceable: 4	coalesced: 4
235 moves: 9	coalesceable: 9	coalesced: 8
236 moves: 8	coalesceable: 8	coalesced: 8
237 moves: 124	coalesceable: 72	coalesced: 58
238 moves: 6	coalesceable: 6	coalesced: 6
239 moves: 62	coalesceable: 31	coalesced: 29
240 moves: 4	coalesceable: 4	coalesced: 4
241 moves: 48	coalesceable: 23	coalesced: 21
242 moves: 6	coalesceable: 6	coalesced: 6
243 moves: 23	coalesceable: 15	coalesced: 11
244 moves: 6	coalesceable: 6	coalesced: 6
245 moves: 23	coalesceable: 15	coalesced: 11
246 moves: 6	coalesceable: 6	coalesced: 6
247 moves: 30	coalesceable: 19	coalesced: 16
248 moves: 6	coalesceable: 6	coalesced: 6
249 moves: 29	coalesceable: 21	coalesced: 17
250 moves: 6	coalesceable: 6	coalesced: 6
251 moves: 24	coalesceable: 16	coalesced: 13
252 moves: 6	coalesceable: 6	coalesced: 6
253 moves: 24	coalesceable: 16	coalesced: 13
254 moves: 6	coalesceable: 6	coalesced: 6
255 moves: 30	coalesceable: 22	coalesced: 19
256 moves: 6	coalesceable: 6	coalesced: 6
257 moves: 30	coalesceable: 22	coalesced: 19
258 moves: 6	coalesceable: 6	coalesced: 6
259 moves: 62	coalesceable: 31	coalesced: 29
260 moves: 4	coalesceable: 4	coalesced: 4
261 moves: 162	coalesceable: 108	coalesced: 98
262 moves: 8	coalesceable: 8	coalesced: 8
263 moves: 317	coalesceable: 197	coalesced: 159
264 moves: 6	coalesceable: 6	coalesced: 6
265 moves: 209	coalesceable: 115	coalesced: 93
266 moves: 4	coalesceable: 4	coalesced: 4
267 moves: 5	coalesceable: 5	coalesced: 5
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: 54	coalesceable: 41	coalesced: 38
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: 71	coalesceable: 46	coalesced: 33
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: 95	coalesceable: 68	coalesced: 55
351 moves: 6	coalesceable: 6	coalesced: 6
352 moves: 99	coalesceable: 62	coalesced: 56
353 moves: 6	coalesceable: 6	coalesced: 6
354 moves: 278	coalesceable: 125	coalesced: 110
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: 911	coalesceable: 384	coalesced: 339
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: 1581	coalesceable: 749	coalesced: 608
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: 20.4s,    gctime: 0.04101s,     systime: 0.43961s.
        external oracle real: 20.9s
        external oracle size: 195137
     apply colour (par) eval: runtime: 3m50s,    gctime: 6.7s,     systime: 5.8s.
     apply colour (par) real: 1m42s
     apply colour (par) size: 838432
           check colour eval: runtime: 4.6s,    gctime: 0.28407s,     systime: 0.12992s.
           check colour real: 4.7s
           check colour size: 838810
          word_to_stack eval: runtime: 2m30s,    gctime: 4.4s,     systime: 1.1s.
          word_to_stack real: 2m31s
          word_to_stack size: 685501
          stack_rawcall eval: runtime: 1m30s,    gctime: 2.1s,     systime: 0.64249s.
          stack_rawcall real: 1m30s
          stack_rawcall size: 665633
      stack_alloc (par) eval: runtime: 2m26s,    gctime: 13.5s,     systime: 8.8s.
      stack_alloc (par) real: 1m04s
      stack_alloc (par) size: 669518
expand stack_remove_def eval: runtime: 0.09034s,    gctime: 0.00000s,     systime: 0.01335s.
expand stack_remove_def real: 0.10374s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m58s,    gctime: 2.4s,     systime: 5.3s.
     stack_remove (par) real: 1m14s
     stack_remove (par) size: 1118551
      stack_names (par) eval: runtime: 1m30s,    gctime: 2.1s,     systime: 3.2s.
      stack_names (par) real: 34.5s
      stack_names (par) size: 1154903
     stack_to_lab (par) eval: runtime: 3m04s,    gctime: 4.8s,     systime: 4.2s.
     stack_to_lab (par) real: 1m08s
     stack_to_lab (par) size: 1418892
          lab_to_target eval: runtime: 12m09s,    gctime: 1m36s,     systime: 14.0s.
          lab_to_target real: 12m23s
          lab_to_target size: 2390476
                      export: runtime: 0.87941s,    gctime: 0.00000s,     systime: 0.00664s.
Saved theorem _______ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 41m55s to build
Linking /root/regression/cakeml-1887/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/root/regression/HOL-9ef7738eaecdb725492f0929f6b270d1f4e63a40/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-1887/compiler/compilationLib.sml:714: 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: 29.2s,    gctime: 1.1s,     systime: 0.25278s.
                to_flat real: 29.4s
                to_flat size: 75681
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.68532s,    gctime: 0.11230s,     systime: 0.00676s.
                to_clos real: 0.69213s
                to_clos size: 44318
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 10.6s,    gctime: 0.40884s,     systime: 0.05623s.
                 to_bvl real: 10.6s
                 to_bvl size: 70278
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 1m31s,    gctime: 1.3s,     systime: 0.56235s.
                 to_bvi real: 1m31s
                 to_bvi size: 77188
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 25.2s,    gctime: 1.3s,     systime: 0.28978s.
                to_data real: 25.5s
                to_data size: 126469
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 30.6s,    gctime: 1.3s,     systime: 0.17651s.
           data_to_word real: 30.8s
           data_to_word size: 390464
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m27s,    gctime: 20.2s,     systime: 4.1s.
 inst,ssa,two-reg (par) real: 1m22s
 inst,ssa,two-reg (par) size: 1265369
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 1m02s,    gctime: 10.4s,     systime: 6.3s.
        get_clash (par) real: 27.7s
        get_clash (par) size: 1967049
        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: 74	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: 72	coalesceable: 44	coalesced: 43
135 moves: 17	coalesceable: 11	coalesced: 11
136 moves: 4375	coalesceable: 2573	coalesced: 2573
137 moves: 17	coalesceable: 11	coalesced: 11
138 moves: 17	coalesceable: 11	coalesced: 11
139 moves: 17	coalesceable: 11	coalesced: 11
140 moves: 17	coalesceable: 11	coalesced: 11
141 moves: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 17	coalesceable: 11	coalesced: 11
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 17	coalesceable: 11	coalesced: 11
148 moves: 17	coalesceable: 11	coalesced: 11
149 moves: 17	coalesceable: 11	coalesced: 11
150 moves: 17	coalesceable: 11	coalesced: 11
151 moves: 17	coalesceable: 11	coalesced: 11
152 moves: 10	coalesceable: 6	coalesced: 6
153 moves: 60	coalesceable: 41	coalesced: 40
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: 2	coalesceable: 2	coalesced: 2
160 moves: 17	coalesceable: 11	coalesced: 11
161 moves: 5	coalesceable: 3	coalesced: 3
162 moves: 6	coalesceable: 6	coalesced: 6
163 moves: 29	coalesceable: 19	coalesced: 13
164 moves: 4	coalesceable: 4	coalesced: 4
165 moves: 7	coalesceable: 7	coalesced: 7
166 moves: 4	coalesceable: 4	coalesced: 4
167 moves: 9	coalesceable: 9	coalesced: 8
168 moves: 8	coalesceable: 8	coalesced: 8
169 moves: 124	coalesceable: 72	coalesced: 58
170 moves: 6	coalesceable: 6	coalesced: 6
171 moves: 62	coalesceable: 31	coalesced: 29
172 moves: 8	coalesceable: 8	coalesced: 8
173 moves: 180	coalesceable: 93	coalesced: 89
174 moves: 6	coalesceable: 6	coalesced: 6
175 moves: 7	coalesceable: 7	coalesced: 4
176 moves: 6	coalesceable: 6	coalesced: 6
177 moves: 23	coalesceable: 15	coalesced: 11
178 moves: 6	coalesceable: 6	coalesced: 6
179 moves: 23	coalesceable: 15	coalesced: 11
180 moves: 6	coalesceable: 6	coalesced: 6
181 moves: 30	coalesceable: 19	coalesced: 16
182 moves: 6	coalesceable: 6	coalesced: 6
183 moves: 29	coalesceable: 21	coalesced: 17
184 moves: 6	coalesceable: 6	coalesced: 6
185 moves: 24	coalesceable: 16	coalesced: 13
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 24	coalesceable: 16	coalesced: 13
188 moves: 6	coalesceable: 6	coalesced: 6
189 moves: 30	coalesceable: 22	coalesced: 19
190 moves: 4	coalesceable: 4	coalesced: 4
191 moves: 3	coalesceable: 3	coalesced: 3
192 moves: 4	coalesceable: 4	coalesced: 4
193 moves: 25	coalesceable: 18	coalesced: 16
194 moves: 4	coalesceable: 4	coalesced: 4
195 moves: 3	coalesceable: 3	coalesced: 3
196 moves: 6	coalesceable: 6	coalesced: 6
197 moves: 36	coalesceable: 23	coalesced: 17
198 moves: 6	coalesceable: 6	coalesced: 6
199 moves: 21	coalesceable: 19	coalesced: 19
200 moves: 8	coalesceable: 8	coalesced: 8
201 moves: 22	coalesceable: 20	coalesced: 20
202 moves: 12	coalesceable: 12	coalesced: 12
203 moves: 218	coalesceable: 134	coalesced: 94
204 moves: 8	coalesceable: 8	coalesced: 8
205 moves: 124	coalesceable: 72	coalesced: 58
206 moves: 4	coalesceable: 4	coalesced: 4
207 moves: 77	coalesceable: 56	coalesced: 53
208 moves: 6	coalesceable: 6	coalesced: 6
209 moves: 110	coalesceable: 79	coalesced: 69
210 moves: 8	coalesceable: 8	coalesced: 8
211 moves: 407	coalesceable: 208	coalesced: 175
212 moves: 4	coalesceable: 4	coalesced: 4
213 moves: 56	coalesceable: 33	coalesced: 30
214 moves: 4	coalesceable: 4	coalesced: 4
215 moves: 8	coalesceable: 6	coalesced: 6
216 moves: 8	coalesceable: 8	coalesced: 8
217 moves: 163	coalesceable: 110	coalesced: 96
218 moves: 6	coalesceable: 6	coalesced: 6
219 moves: 114	coalesceable: 80	coalesced: 72
220 moves: 4	coalesceable: 4	coalesced: 4
221 moves: 6	coalesceable: 6	coalesced: 6
222 moves: 8	coalesceable: 8	coalesced: 8
223 moves: 128	coalesceable: 77	coalesced: 70
224 moves: 8	coalesceable: 8	coalesced: 8
225 moves: 111	coalesceable: 66	coalesced: 51
226 moves: 6	coalesceable: 6	coalesced: 6
227 moves: 50	coalesceable: 38	coalesced: 35
228 moves: 6	coalesceable: 6	coalesced: 6
229 moves: 427	coalesceable: 263	coalesced: 198
230 moves: 4	coalesceable: 4	coalesced: 4
231 moves: 5	coalesceable: 5	coalesced: 5
232 moves: 4	coalesceable: 4	coalesced: 4
233 moves: 36	coalesceable: 21	coalesced: 19

runtime: 18.2s,    gctime: 0.04221s,     systime: 0.20652s.
        external oracle real: 18.4s
        external oracle size: 143336
     apply colour (par) eval: runtime: 2m36s,    gctime: 4.5s,     systime: 4.5s.
     apply colour (par) real: 1m33s
     apply colour (par) size: 633178
           check colour eval: runtime: 2.0s,    gctime: 0.22999s,     systime: 0.03318s.
           check colour real: 2.1s
           check colour size: 633413
          word_to_stack eval: runtime: 1m51s,    gctime: 2.4s,     systime: 1.4s.
          word_to_stack real: 1m52s
          word_to_stack size: 529655
          stack_rawcall eval: runtime: 1m07s,    gctime: 0.96862s,     systime: 0.51336s.
          stack_rawcall real: 1m08s
          stack_rawcall size: 515854
      stack_alloc (par) eval: runtime: 1m33s,    gctime: 1.2s,     systime: 3.4s.
      stack_alloc (par) real: 46.2s
      stack_alloc (par) size: 517544
expand stack_remove_def eval: runtime: 0.07404s,    gctime: 0.00000s,     systime: 0.00002s.
expand stack_remove_def real: 0.07412s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m10s,    gctime: 1.9s,     systime: 4.8s.
     stack_remove (par) real: 1m14s
     stack_remove (par) size: 879421
      stack_names (par) eval: runtime: 1m04s,    gctime: 1.6s,     systime: 1.4s.
      stack_names (par) real: 31.9s
      stack_names (par) size: 907306
     stack_to_lab (par) eval: runtime: 2m13s,    gctime: 3.4s,     systime: 2.9s.
     stack_to_lab (par) real: 1m04s
     stack_to_lab (par) size: 1103767
          lab_to_target eval: runtime: 8m54s,    gctime: 47.8s,     systime: 8.5s.
          lab_to_target real: 9m03s
          lab_to_target size: 1831446
                      export: runtime: 7.8s,    gctime: 7.0s,     systime: 0.53017s.
Saved theorem _______ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 29m53s to build
cc cat.S /root/regression/cakeml-1887/basis/basis_ffi.o  -o cake_cat
cc diff.S /root/regression/cakeml-1887/basis/basis_ffi.o  -o cake_diff
cc echo.S /root/regression/cakeml-1887/basis/basis_ffi.o  -o cake_echo
Linking /root/regression/cakeml-1887/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/root/regression/HOL-9ef7738eaecdb725492f0929f6b270d1f4e63a40/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-1887/compiler/compilationLib.sml:714: 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: 54.2s,    gctime: 1.3s,     systime: 1.6s.
                to_flat real: 55.7s
                to_flat size: 359797
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 6.1s,    gctime: 0.41789s,     systime: 0.07677s.
                to_clos real: 6.2s
                to_clos size: 165794
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 38.6s,    gctime: 0.93944s,     systime: 0.26994s.
                 to_bvl real: 38.8s
                 to_bvl size: 292435
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 4m12s,    gctime: 1.2s,     systime: 3.6s.
                 to_bvi real: 4m16s
                 to_bvi size: 255802
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 1m02s,    gctime: 2.3s,     systime: 0.95330s.
                to_data real: 1m03s
                to_data size: 469789
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 2m16s,    gctime: 3.4s,     systime: 2.1s.
           data_to_word real: 2m18s
           data_to_word size: 1554448
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 22m35s,    gctime: 1m58s,     systime: 40.9s.
 inst,ssa,two-reg (par) real: 17m21s
 inst,ssa,two-reg (par) size: 4922846
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 9m10s,    gctime: 1m03s,     systime: 37.4s.
        get_clash (par) real: 2m27s
        get_clash (par) size: 7506304
        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: 358	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: 72	coalesceable: 44	coalesced: 43
158 moves: 17	coalesceable: 11	coalesced: 11
159 moves: 17	coalesceable: 11	coalesced: 11
160 moves: 4375	coalesceable: 2573	coalesced: 2573
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: 17	coalesceable: 11	coalesced: 11
179 moves: 10	coalesceable: 6	coalesced: 6
180 moves: 60	coalesceable: 41	coalesced: 40
181 moves: 60	coalesceable: 41	coalesced: 40
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: 17	coalesceable: 11	coalesced: 11
192 moves: 2	coalesceable: 2	coalesced: 2
193 moves: 17	coalesceable: 11	coalesced: 11
194 moves: 573	coalesceable: 374	coalesced: 314
195 moves: 2	coalesceable: 2	coalesced: 2
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: 2	coalesceable: 2	coalesced: 2
201 moves: 2	coalesceable: 2	coalesced: 2
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: 17	coalesceable: 11	coalesced: 11
208 moves: 2	coalesceable: 2	coalesced: 2
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: 17	coalesceable: 11	coalesced: 11
222 moves: 51	coalesceable: 31	coalesced: 31
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: 17	coalesceable: 11	coalesced: 11
228 moves: 16	coalesceable: 11	coalesced: 11
229 moves: 17	coalesceable: 11	coalesced: 11
230 moves: 17	coalesceable: 11	coalesced: 11
231 moves: 24	coalesceable: 16	coalesced: 16
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: 17	coalesceable: 11	coalesced: 11
242 moves: 2312	coalesceable: 1286	coalesced: 1286
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: 17	coalesceable: 11	coalesced: 11
249 moves: 74	coalesceable: 49	coalesced: 43
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: 17	coalesceable: 11	coalesced: 11
273 moves: 5885	coalesceable: 3532	coalesced: 3033
274 moves: 11474	coalesceable: 7187	coalesced: 6357
275 moves: 10448	coalesceable: 6311	coalesced: 5527
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: 17	coalesceable: 11	coalesced: 11
287 moves: 102	coalesceable: 58	coalesced: 58
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: 17	coalesceable: 11	coalesced: 11
294 moves: 2705	coalesceable: 1486	coalesced: 1387
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: 17	coalesceable: 11	coalesced: 11
300 moves: 158	coalesceable: 117	coalesced: 117
301 moves: 17	coalesceable: 11	coalesced: 11
302 moves: 17	coalesceable: 11	coalesced: 11
303 moves: 17	coalesceable: 11	coalesced: 11
304 moves: 17	coalesceable: 11	coalesced: 11
305 moves: 5	coalesceable: 3	coalesced: 3
306 moves: 4	coalesceable: 4	coalesced: 4
307 moves: 6	coalesceable: 6	coalesced: 6
308 moves: 4	coalesceable: 4	coalesced: 4
309 moves: 6	coalesceable: 6	coalesced: 6
310 moves: 8	coalesceable: 8	coalesced: 8
311 moves: 46	coalesceable: 34	coalesced: 33
312 moves: 4	coalesceable: 4	coalesced: 4
313 moves: 3	coalesceable: 3	coalesced: 3
314 moves: 6	coalesceable: 6	coalesced: 6
315 moves: 3	coalesceable: 3	coalesced: 2
316 moves: 8	coalesceable: 8	coalesced: 8
317 moves: 99	coalesceable: 63	coalesced: 50
318 moves: 6	coalesceable: 6	coalesced: 6
319 moves: 7	coalesceable: 7	coalesced: 4
320 moves: 6	coalesceable: 6	coalesced: 6
321 moves: 29	coalesceable: 19	coalesced: 13
322 moves: 8	coalesceable: 8	coalesced: 8
323 moves: 103	coalesceable: 64	coalesced: 59
324 moves: 4	coalesceable: 4	coalesced: 4
325 moves: 7	coalesceable: 7	coalesced: 7
326 moves: 6	coalesceable: 6	coalesced: 6
327 moves: 49	coalesceable: 36	coalesced: 34
328 moves: 6	coalesceable: 6	coalesced: 6
329 moves: 32	coalesceable: 23	coalesced: 18
330 moves: 4	coalesceable: 4	coalesced: 4
331 moves: 5	coalesceable: 5	coalesced: 3
332 moves: 4	coalesceable: 4	coalesced: 4
333 moves: 7	coalesceable: 7	coalesced: 7
334 moves: 6	coalesceable: 6	coalesced: 6
335 moves: 86	coalesceable: 57	coalesced: 51
336 moves: 6	coalesceable: 6	coalesced: 6
337 moves: 76	coalesceable: 47	coalesced: 43
338 moves: 6	coalesceable: 6	coalesced: 6
339 moves: 42	coalesceable: 27	coalesced: 25
340 moves: 4	coalesceable: 4	coalesced: 4
341 moves: 94	coalesceable: 57	coalesced: 56
342 moves: 6	coalesceable: 6	coalesced: 6
343 moves: 49	coalesceable: 37	coalesced: 35
344 moves: 4	coalesceable: 4	coalesced: 4
345 moves: 40	coalesceable: 25	coalesced: 24
346 moves: 6	coalesceable: 6	coalesced: 6
347 moves: 79	coalesceable: 57	coalesced: 54
348 moves: 6	coalesceable: 6	coalesced: 6
349 moves: 42	coalesceable: 27	coalesced: 26
350 moves: 4	coalesceable: 4	coalesced: 4
351 moves: 12	coalesceable: 11	coalesced: 9
352 moves: 4	coalesceable: 4	coalesced: 4
353 moves: 9	coalesceable: 9	coalesced: 8
354 moves: 4	coalesceable: 4	coalesced: 4
355 moves: 29	coalesceable: 12	coalesced: 11
356 moves: 8	coalesceable: 8	coalesced: 8
357 moves: 124	coalesceable: 72	coalesced: 58
358 moves: 6	coalesceable: 6	coalesced: 6
359 moves: 62	coalesceable: 31	coalesced: 29
360 moves: 4	coalesceable: 4	coalesced: 4
361 moves: 48	coalesceable: 23	coalesced: 21
362 moves: 6	coalesceable: 6	coalesced: 6
363 moves: 23	coalesceable: 15	coalesced: 11
364 moves: 6	coalesceable: 6	coalesced: 6
365 moves: 23	coalesceable: 15	coalesced: 11
366 moves: 6	coalesceable: 6	coalesced: 6
367 moves: 30	coalesceable: 19	coalesced: 16
368 moves: 6	coalesceable: 6	coalesced: 6
369 moves: 29	coalesceable: 21	coalesced: 17
370 moves: 6	coalesceable: 6	coalesced: 6
371 moves: 24	coalesceable: 16	coalesced: 13
372 moves: 6	coalesceable: 6	coalesced: 6
373 moves: 24	coalesceable: 16	coalesced: 13
374 moves: 6	coalesceable: 6	coalesced: 6
375 moves: 30	coalesceable: 22	coalesced: 19
376 moves: 6	coalesceable: 6	coalesced: 6
377 moves: 30	coalesceable: 22	coalesced: 19
378 moves: 6	coalesceable: 6	coalesced: 6
379 moves: 62	coalesceable: 31	coalesced: 29
380 moves: 4	coalesceable: 4	coalesced: 4
381 moves: 3	coalesceable: 3	coalesced: 3
382 moves: 4	coalesceable: 4	coalesced: 4
383 moves: 43	coalesceable: 29	coalesced: 25
384 moves: 4	coalesceable: 4	coalesced: 4
385 moves: 25	coalesceable: 18	coalesced: 16
386 moves: 4	coalesceable: 4	coalesced: 4
387 moves: 3	coalesceable: 3	coalesced: 3
388 moves: 6	coalesceable: 6	coalesced: 6
389 moves: 36	coalesceable: 23	coalesced: 17
390 moves: 6	coalesceable: 6	coalesced: 6
391 moves: 21	coalesceable: 19	coalesced: 19
392 moves: 4	coalesceable: 4	coalesced: 4
393 moves: 9	coalesceable: 9	coalesced: 8
394 moves: 8	coalesceable: 8	coalesced: 8
395 moves: 22	coalesceable: 20	coalesced: 20
396 moves: 12	coalesceable: 12	coalesced: 12
397 moves: 218	coalesceable: 134	coalesced: 94
398 moves: 12	coalesceable: 12	coalesced: 12
399 moves: 218	coalesceable: 134	coalesced: 94
400 moves: 8	coalesceable: 8	coalesced: 8
401 moves: 124	coalesceable: 72	coalesced: 58
402 moves: 4	coalesceable: 4	coalesced: 4
403 moves: 77	coalesceable: 56	coalesced: 53
404 moves: 6	coalesceable: 6	coalesced: 6
405 moves: 110	coalesceable: 79	coalesced: 69
406 moves: 8	coalesceable: 8	coalesced: 8
407 moves: 407	coalesceable: 208	coalesced: 175
408 moves: 4	coalesceable: 4	coalesced: 4
409 moves: 56	coalesceable: 33	coalesced: 30
410 moves: 4	coalesceable: 4	coalesced: 4
411 moves: 8	coalesceable: 6	coalesced: 6
412 moves: 8	coalesceable: 8	coalesced: 8
413 moves: 163	coalesceable: 110	coalesced: 96
414 moves: 6	coalesceable: 6	coalesced: 6
415 moves: 114	coalesceable: 80	coalesced: 72
416 moves: 4	coalesceable: 4	coalesced: 4
417 moves: 6	coalesceable: 6	coalesced: 6
418 moves: 4	coalesceable: 4	coalesced: 4
419 moves: 6	coalesceable: 6	coalesced: 6
420 moves: 8	coalesceable: 8	coalesced: 8
421 moves: 128	coalesceable: 77	coalesced: 70
422 moves: 8	coalesceable: 8	coalesced: 8
423 moves: 111	coalesceable: 66	coalesced: 51
424 moves: 6	coalesceable: 6	coalesced: 6
425 moves: 427	coalesceable: 263	coalesced: 198
426 moves: 4	coalesceable: 4	coalesced: 4
427 moves: 5	coalesceable: 5	coalesced: 5
428 moves: 4	coalesceable: 4	coalesced: 4
429 moves: 272	coalesceable: 139	coalesced: 131
430 moves: 4	coalesceable: 4	coalesced: 4
431 moves: 69	coalesceable: 54	coalesced: 54
432 moves: 6	coalesceable: 6	coalesced: 6
433 moves: 54	coalesceable: 41	coalesced: 38
434 moves: 4	coalesceable: 4	coalesced: 4
435 moves: 21	coalesceable: 18	coalesced: 16
436 moves: 4	coalesceable: 4	coalesced: 4
437 moves: 164	coalesceable: 106	coalesced: 89
438 moves: 224	coalesceable: 137	coalesced: 113
439 moves: 217	coalesceable: 133	coalesced: 108
440 moves: 4	coalesceable: 4	coalesced: 4
441 moves: 45	coalesceable: 26	coalesced: 24
442 moves: 6	coalesceable: 6	coalesced: 6
443 moves: 116	coalesceable: 78	coalesced: 73
444 moves: 6	coalesceable: 6	coalesced: 6
445 moves: 703	coalesceable: 460	coalesced: 413
446 moves: 6	coalesceable: 6	coalesced: 6
447 moves: 30	coalesceable: 21	coalesced: 16
448 moves: 4	coalesceable: 4	coalesced: 4
449 moves: 7	coalesceable: 7	coalesced: 7
450 moves: 6	coalesceable: 6	coalesced: 6
451 moves: 30	coalesceable: 17	coalesced: 16
452 moves: 10	coalesceable: 10	coalesced: 10
453 moves: 2844	coalesceable: 1470	coalesced: 781
454 moves: 10	coalesceable: 10	coalesced: 10
455 moves: 2803	coalesceable: 1454	coalesced: 770
456 moves: 4	coalesceable: 4	coalesced: 4
457 moves: 150	coalesceable: 86	coalesced: 76
458 moves: 4	coalesceable: 4	coalesced: 4
459 moves: 4	coalesceable: 4	coalesced: 4
460 moves: 8	coalesceable: 8	coalesced: 8
461 moves: 99	coalesceable: 63	coalesced: 57
462 moves: 8	coalesceable: 8	coalesced: 8
463 moves: 72	coalesceable: 48	coalesced: 44
464 moves: 10	coalesceable: 10	coalesced: 10
465 moves: 195	coalesceable: 104	coalesced: 68
466 moves: 8	coalesceable: 8	coalesced: 8
467 moves: 74	coalesceable: 47	coalesced: 43
468 moves: 6	coalesceable: 6	coalesced: 6
469 moves: 58	coalesceable: 40	coalesced: 33
470 moves: 6	coalesceable: 6	coalesced: 6
471 moves: 634	coalesceable: 440	coalesced: 316
472 moves: 6	coalesceable: 6	coalesced: 6
473 moves: 15	coalesceable: 15	coalesced: 15
474 moves: 4	coalesceable: 4	coalesced: 4
475 moves: 321	coalesceable: 204	coalesced: 200
476 moves: 8	coalesceable: 8	coalesced: 8
477 moves: 107	coalesceable: 65	coalesced: 65
478 moves: 10	coalesceable: 10	coalesced: 10
479 moves: 514	coalesceable: 292	coalesced: 271
480 moves: 4	coalesceable: 4	coalesced: 4
481 moves: 26	coalesceable: 19	coalesced: 17
482 moves: 8	coalesceable: 8	coalesced: 8
483 moves: 256	coalesceable: 149	coalesced: 130
484 moves: 8	coalesceable: 8	coalesced: 8
485 moves: 789	coalesceable: 475	coalesced: 427
486 moves: 6	coalesceable: 6	coalesced: 6
487 moves: 37	coalesceable: 23	coalesced: 22
488 moves: 4	coalesceable: 4	coalesced: 4
489 moves: 159	coalesceable: 91	coalesced: 90
490 moves: 6	coalesceable: 6	coalesced: 6
491 moves: 220	coalesceable: 158	coalesced: 129
492 moves: 4	coalesceable: 4	coalesced: 4
493 moves: 477	coalesceable: 295	coalesced: 290
494 moves: 6	coalesceable: 6	coalesced: 6
495 moves: 16	coalesceable: 9	coalesced: 6
496 moves: 6	coalesceable: 6	coalesced: 6
497 moves: 42	coalesceable: 26	coalesced: 25
498 moves: 4	coalesceable: 4	coalesced: 4
499 moves: 208	coalesceable: 121	coalesced: 117
500 moves: 4	coalesceable: 4	coalesced: 4
501 moves: 419	coalesceable: 260	coalesced: 230
502 moves: 4	coalesceable: 4	coalesced: 4
503 moves: 21	coalesceable: 14	coalesced: 13
504 moves: 6	coalesceable: 6	coalesced: 6
505 moves: 188	coalesceable: 117	coalesced: 112
506 moves: 6	coalesceable: 6	coalesced: 6
507 moves: 161	coalesceable: 117	coalesced: 95
508 moves: 4	coalesceable: 4	coalesced: 4
509 moves: 156	coalesceable: 103	coalesced: 98
510 moves: 4	coalesceable: 4	coalesced: 4
511 moves: 138	coalesceable: 92	coalesced: 88
512 moves: 4	coalesceable: 4	coalesced: 4
513 moves: 4	coalesceable: 4	coalesced: 4
514 moves: 4	coalesceable: 4	coalesced: 4
515 moves: 100	coalesceable: 64	coalesced: 61
516 moves: 6	coalesceable: 6	coalesced: 6
517 moves: 7	coalesceable: 7	coalesced: 7
518 moves: 10	coalesceable: 10	coalesced: 10
519 moves: 70	coalesceable: 61	coalesced: 55
520 moves: 4	coalesceable: 4	coalesced: 4
521 moves: 144	coalesceable: 89	coalesced: 86
522 moves: 4	coalesceable: 4	coalesced: 4
523 moves: 23	coalesceable: 15	coalesced: 14
524 moves: 9	coalesceable: 9	coalesced: 9
525 moves: 6	coalesceable: 6	coalesced: 6
526 moves: 232	coalesceable: 126	coalesced: 117
527 moves: 37	coalesceable: 23	coalesced: 20
528 moves: 4	coalesceable: 4	coalesced: 4
529 moves: 25	coalesceable: 16	coalesced: 14
530 moves: 10	coalesceable: 10	coalesced: 10
531 moves: 224	coalesceable: 128	coalesced: 94
532 moves: 8	coalesceable: 8	coalesced: 8
533 moves: 249	coalesceable: 143	coalesced: 129
534 moves: 8	coalesceable: 8	coalesced: 8
535 moves: 52	coalesceable: 37	coalesced: 31
536 moves: 6	coalesceable: 6	coalesced: 6
537 moves: 8	coalesceable: 8	coalesced: 6
538 moves: 6	coalesceable: 6	coalesced: 6
539 moves: 11	coalesceable: 11	coalesced: 9
540 moves: 10	coalesceable: 10	coalesced: 10
541 moves: 405	coalesceable: 209	coalesced: 162
542 moves: 10	coalesceable: 10	coalesced: 10
543 moves: 1186	coalesceable: 706	coalesced: 410
544 moves: 10	coalesceable: 10	coalesced: 10
545 moves: 96	coalesceable: 62	coalesced: 53
546 moves: 6	coalesceable: 6	coalesced: 6
547 moves: 24	coalesceable: 16	coalesced: 13
548 moves: 4	coalesceable: 4	coalesced: 4
549 moves: 36	coalesceable: 24	coalesced: 23
550 moves: 6	coalesceable: 6	coalesced: 6
551 moves: 24	coalesceable: 16	coalesced: 13
552 moves: 4	coalesceable: 4	coalesced: 4
553 moves: 147	coalesceable: 73	coalesced: 54
554 moves: 4	coalesceable: 4	coalesced: 4
555 moves: 89	coalesceable: 54	coalesced: 47
556 moves: 4	coalesceable: 4	coalesced: 4
557 moves: 22	coalesceable: 14	coalesced: 13
558 moves: 6	coalesceable: 6	coalesced: 6
559 moves: 40	coalesceable: 23	coalesced: 19
560 moves: 8	coalesceable: 8	coalesced: 8
561 moves: 64	coalesceable: 35	coalesced: 33
562 moves: 6	coalesceable: 6	coalesced: 6
563 moves: 24	coalesceable: 16	coalesced: 13
564 moves: 4	coalesceable: 4	coalesced: 4
565 moves: 59	coalesceable: 34	coalesced: 31
566 moves: 4	coalesceable: 4	coalesced: 4
567 moves: 252	coalesceable: 137	coalesced: 115
568 moves: 4	coalesceable: 4	coalesced: 4
569 moves: 18	coalesceable: 10	coalesced: 10
570 moves: 6	coalesceable: 6	coalesced: 6
571 moves: 148	coalesceable: 60	coalesced: 56
572 moves: 6	coalesceable: 6	coalesced: 6
573 moves: 112	coalesceable: 76	coalesced: 72
574 moves: 4	coalesceable: 4	coalesced: 4
575 moves: 6	coalesceable: 6	coalesced: 6
576 moves: 4	coalesceable: 4	coalesced: 4
577 moves: 6	coalesceable: 6	coalesced: 6
578 moves: 4	coalesceable: 4	coalesced: 4
579 moves: 6	coalesceable: 6	coalesced: 6
580 moves: 4	coalesceable: 4	coalesced: 4
581 moves: 6	coalesceable: 6	coalesced: 6
582 moves: 4	coalesceable: 4	coalesced: 4
583 moves: 6	coalesceable: 6	coalesced: 6
584 moves: 4	coalesceable: 4	coalesced: 4
585 moves: 6	coalesceable: 6	coalesced: 6
586 moves: 8	coalesceable: 8	coalesced: 8
587 moves: 96	coalesceable: 69	coalesced: 66
588 moves: 6	coalesceable: 6	coalesced: 6
589 moves: 12	coalesceable: 12	coalesced: 12
590 moves: 6	coalesceable: 6	coalesced: 6
591 moves: 76	coalesceable: 44	coalesced: 42
592 moves: 4	coalesceable: 4	coalesced: 4
593 moves: 25	coalesceable: 19	coalesced: 19
594 moves: 6	coalesceable: 6	coalesced: 6
595 moves: 86	coalesceable: 55	coalesced: 53
596 moves: 6	coalesceable: 6	coalesced: 6
597 moves: 77	coalesceable: 49	coalesced: 44
598 moves: 4	coalesceable: 4	coalesced: 4
599 moves: 21	coalesceable: 14	coalesced: 13
600 moves: 4	coalesceable: 4	coalesced: 4
601 moves: 21	coalesceable: 14	coalesced: 13
602 moves: 10	coalesceable: 10	coalesced: 8
603 moves: 3049	coalesceable: 1593	coalesced: 1296
604 moves: 4	coalesceable: 4	coalesced: 4
605 moves: 10	coalesceable: 9	coalesced: 9
606 moves: 6	coalesceable: 6	coalesced: 6
607 moves: 40	coalesceable: 25	coalesced: 24
608 moves: 18	coalesceable: 18	coalesced: 18
609 moves: 91	coalesceable: 53	coalesced: 37
610 moves: 4	coalesceable: 4	coalesced: 4
611 moves: 18	coalesceable: 16	coalesced: 16
612 moves: 4	coalesceable: 4	coalesced: 4
613 moves: 158	coalesceable: 90	coalesced: 87
614 moves: 4	coalesceable: 4	coalesced: 4
615 moves: 111	coalesceable: 80	coalesced: 77
616 moves: 4	coalesceable: 4	coalesced: 4
617 moves: 30	coalesceable: 19	coalesced: 18
618 moves: 4	coalesceable: 4	coalesced: 4
619 moves: 17	coalesceable: 15	coalesced: 15
620 moves: 4	coalesceable: 4	coalesced: 4
621 moves: 12	coalesceable: 11	coalesced: 11
622 moves: 4	coalesceable: 4	coalesced: 4
623 moves: 69	coalesceable: 40	coalesced: 39
624 moves: 6	coalesceable: 6	coalesced: 6
625 moves: 3	coalesceable: 3	coalesced: 2
626 moves: 6	coalesceable: 6	coalesced: 6
627 moves: 37	coalesceable: 22	coalesced: 21
628 moves: 6	coalesceable: 6	coalesced: 6
629 moves: 3	coalesceable: 3	coalesced: 3
630 moves: 6	coalesceable: 6	coalesced: 6
631 moves: 37	coalesceable: 22	coalesced: 21
632 moves: 4	coalesceable: 4	coalesced: 4
633 moves: 55	coalesceable: 35	coalesced: 31
634 moves: 6	coalesceable: 6	coalesced: 6
635 moves: 23	coalesceable: 21	coalesced: 21
636 moves: 4	coalesceable: 4	coalesced: 4
637 moves: 25	coalesceable: 17	coalesced: 16
638 moves: 4	coalesceable: 4	coalesced: 4
639 moves: 77	coalesceable: 51	coalesced: 48
640 moves: 6	coalesceable: 6	coalesced: 6
641 moves: 20	coalesceable: 18	coalesced: 14
642 moves: 38	coalesceable: 25	coalesced: 24
643 moves: 79	coalesceable: 50	coalesced: 47
644 moves: 6	coalesceable: 6	coalesced: 6
645 moves: 85	coalesceable: 57	coalesced: 54
646 moves: 4	coalesceable: 4	coalesced: 4
647 moves: 40	coalesceable: 25	coalesced: 24
648 moves: 6	coalesceable: 6	coalesced: 6
649 moves: 26	coalesceable: 19	coalesced: 19
650 moves: 4	coalesceable: 4	coalesced: 4
651 moves: 21	coalesceable: 14	coalesced: 13
652 moves: 4	coalesceable: 4	coalesced: 4
653 moves: 53	coalesceable: 34	coalesced: 32
654 moves: 167	coalesceable: 107	coalesced: 107
655 moves: 37	coalesceable: 26	coalesced: 25
656 moves: 6	coalesceable: 6	coalesced: 6
657 moves: 34	coalesceable: 23	coalesced: 21
658 moves: 4	coalesceable: 4	coalesced: 4
659 moves: 5	coalesceable: 5	coalesced: 5
660 moves: 38	coalesceable: 25	coalesced: 24
661 moves: 110	coalesceable: 74	coalesced: 72
662 moves: 6	coalesceable: 6	coalesced: 6
663 moves: 34	coalesceable: 23	coalesced: 21
664 moves: 32	coalesceable: 22	coalesced: 22
665 moves: 102	coalesceable: 69	coalesced: 67
666 moves: 6	coalesceable: 6	coalesced: 6
667 moves: 34	coalesceable: 23	coalesced: 21
668 moves: 4	coalesceable: 4	coalesced: 4
669 moves: 5	coalesceable: 5	coalesced: 5
670 moves: 4	coalesceable: 4	coalesced: 4
671 moves: 21	coalesceable: 14	coalesced: 13
672 moves: 4	coalesceable: 4	coalesced: 4
673 moves: 132	coalesceable: 89	coalesced: 80
674 moves: 4	coalesceable: 4	coalesced: 4
675 moves: 88	coalesceable: 59	coalesced: 56
676 moves: 4	coalesceable: 4	coalesced: 4
677 moves: 5	coalesceable: 5	coalesced: 5
678 moves: 4	coalesceable: 4	coalesced: 4
679 moves: 49	coalesceable: 37	coalesced: 37
680 moves: 4	coalesceable: 4	coalesced: 4
681 moves: 5	coalesceable: 5	coalesced: 5
682 moves: 4	coalesceable: 4	coalesced: 4
683 moves: 49	coalesceable: 37	coalesced: 37
684 moves: 4	coalesceable: 4	coalesced: 4
685 moves: 5	coalesceable: 5	coalesced: 5
686 moves: 4	coalesceable: 4	coalesced: 4
687 moves: 5	coalesceable: 5	coalesced: 5
688 moves: 4	coalesceable: 4	coalesced: 4
689 moves: 5	coalesceable: 5	coalesced: 5
690 moves: 4	coalesceable: 4	coalesced: 4
691 moves: 5	coalesceable: 5	coalesced: 5
692 moves: 4	coalesceable: 4	coalesced: 4
693 moves: 5	coalesceable: 5	coalesced: 5
694 moves: 4	coalesceable: 4	coalesced: 4
695 moves: 5	coalesceable: 5	coalesced: 5
696 moves: 4	coalesceable: 4	coalesced: 4
697 moves: 49	coalesceable: 29	coalesced: 28
698 moves: 4	coalesceable: 4	coalesced: 4
699 moves: 116	coalesceable: 73	coalesced: 65
700 moves: 8	coalesceable: 8	coalesced: 8
701 moves: 99	coalesceable: 51	coalesced: 48
702 moves: 4	coalesceable: 4	coalesced: 4
703 moves: 266	coalesceable: 170	coalesced: 166
704 moves: 6	coalesceable: 6	coalesced: 6
705 moves: 503	coalesceable: 392	coalesced: 384
706 moves: 125	coalesceable: 50	coalesced: 45
707 moves: 4	coalesceable: 4	coalesced: 4
708 moves: 210	coalesceable: 128	coalesced: 124
709 moves: 6	coalesceable: 6	coalesced: 6
710 moves: 14	coalesceable: 12	coalesced: 12
711 moves: 6	coalesceable: 6	coalesced: 6
712 moves: 35	coalesceable: 25	coalesced: 22
713 moves: 38	coalesceable: 28	coalesced: 23
714 moves: 4	coalesceable: 4	coalesced: 4
715 moves: 302	coalesceable: 186	coalesced: 181

runtime: 11m01s,    gctime: 0.29342s,     systime: 9.7s.
        external oracle real: 11m10s
        external oracle size: 568447
     apply colour (par) eval: runtime: 11m30s,    gctime: 16.9s,     systime: 26.8s.
     apply colour (par) real: 4m56s
     apply colour (par) size: 2183011
           check colour eval: runtime: 30.6s,    gctime: 1.1s,     systime: 0.73323s.
           check colour real: 31.3s
           check colour size: 2183728
          word_to_stack eval: runtime: 5m39s,    gctime: 7.7s,     systime: 7.5s.
          word_to_stack real: 5m47s
          word_to_stack size: 1747952
          stack_rawcall eval: runtime: 3m51s,    gctime: 3.9s,     systime: 5.1s.
          stack_rawcall real: 3m56s
          stack_rawcall size: 1711785
      stack_alloc (par) eval: runtime: 5m41s,    gctime: 5.2s,     systime: 8.8s.
      stack_alloc (par) real: 2m04s
      stack_alloc (par) size: 1728228
expand stack_remove_def eval: runtime: 0.09174s,    gctime: 0.00000s,     systime: 0.01995s.
expand stack_remove_def real: 0.11174s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 7m20s,    gctime: 8.7s,     systime: 9.0s.
     stack_remove (par) real: 2m22s
     stack_remove (par) size: 2831103
      stack_names (par) eval: runtime: 4m23s,    gctime: 29.8s,     systime: 13.3s.
      stack_names (par) real: 1m54s
      stack_names (par) size: 2924762
     stack_to_lab (par) eval: runtime: 7m45s,    gctime: 10.5s,     systime: 11.9s.
     stack_to_lab (par) real: 2m50s
     stack_to_lab (par) size: 3565326
          lab_to_target eval: runtime: 22m31s,    gctime: 2m25s,     systime: 28.7s.
          lab_to_target real: 23m00s
          lab_to_target size: 5510811
                      export: runtime: 1.9s,    gctime: 0.00000s,     systime: 0.63349s.
Saved theorem _______ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 2h06m05s to build
cc grep.S /root/regression/cakeml-1887/basis/basis_ffi.o  -o cake_grep
Linking /root/regression/cakeml-1887/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/root/regression/HOL-9ef7738eaecdb725492f0929f6b270d1f4e63a40/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-1887/compiler/compilationLib.sml:714: 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: 28.7s,    gctime: 0.74175s,     systime: 0.80345s.
                to_flat real: 29.5s
                to_flat size: 64253
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.39391s,    gctime: 0.00000s,     systime: 0.00009s.
                to_clos real: 0.39398s
                to_clos size: 37214
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 9.4s,    gctime: 0.22154s,     systime: 0.10986s.
                 to_bvl real: 9.5s
                 to_bvl size: 57030
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 1m25s,    gctime: 0.53201s,     systime: 0.54982s.
                 to_bvi real: 1m26s
                 to_bvi size: 65832
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 24.1s,    gctime: 1.1s,     systime: 0.27588s.
                to_data real: 24.4s
                to_data size: 114783
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 28.5s,    gctime: 0.78889s,     systime: 0.33014s.
           data_to_word real: 28.8s
           data_to_word size: 365448
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 2m01s,    gctime: 5.0s,     systime: 3.8s.
 inst,ssa,two-reg (par) real: 1m03s
 inst,ssa,two-reg (par) size: 1212078
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 59.2s,    gctime: 18.4s,     systime: 3.1s.
        get_clash (par) real: 33.7s
        get_clash (par) size: 1886023
        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: 74	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: 72	coalesceable: 44	coalesced: 43
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: 17	coalesceable: 11	coalesced: 11
142 moves: 17	coalesceable: 11	coalesced: 11
143 moves: 17	coalesceable: 11	coalesced: 11
144 moves: 17	coalesceable: 11	coalesced: 11
145 moves: 2	coalesceable: 2	coalesced: 2
146 moves: 17	coalesceable: 11	coalesced: 11
147 moves: 5	coalesceable: 3	coalesced: 3
148 moves: 4	coalesceable: 4	coalesced: 4
149 moves: 9	coalesceable: 9	coalesced: 8
150 moves: 8	coalesceable: 8	coalesced: 8
151 moves: 124	coalesceable: 72	coalesced: 58
152 moves: 6	coalesceable: 6	coalesced: 6
153 moves: 23	coalesceable: 15	coalesced: 11
154 moves: 6	coalesceable: 6	coalesced: 6
155 moves: 23	coalesceable: 15	coalesced: 11
156 moves: 6	coalesceable: 6	coalesced: 6
157 moves: 30	coalesceable: 19	coalesced: 16
158 moves: 6	coalesceable: 6	coalesced: 6
159 moves: 29	coalesceable: 21	coalesced: 17
160 moves: 6	coalesceable: 6	coalesced: 6
161 moves: 24	coalesceable: 16	coalesced: 13
162 moves: 6	coalesceable: 6	coalesced: 6
163 moves: 24	coalesceable: 16	coalesced: 13
164 moves: 6	coalesceable: 6	coalesced: 6
165 moves: 30	coalesceable: 22	coalesced: 19
166 moves: 4	coalesceable: 4	coalesced: 4
167 moves: 25	coalesceable: 18	coalesced: 16
168 moves: 4	coalesceable: 4	coalesced: 4
169 moves: 3	coalesceable: 3	coalesced: 3
170 moves: 6	coalesceable: 6	coalesced: 6
171 moves: 21	coalesceable: 19	coalesced: 19
172 moves: 8	coalesceable: 8	coalesced: 8
173 moves: 22	coalesceable: 20	coalesced: 20
174 moves: 12	coalesceable: 12	coalesced: 12
175 moves: 218	coalesceable: 134	coalesced: 94
176 moves: 8	coalesceable: 8	coalesced: 8
177 moves: 163	coalesceable: 110	coalesced: 96
178 moves: 6	coalesceable: 6	coalesced: 6
179 moves: 114	coalesceable: 80	coalesced: 72
180 moves: 4	coalesceable: 4	coalesced: 4
181 moves: 6	coalesceable: 6	coalesced: 6
182 moves: 8	coalesceable: 8	coalesced: 8
183 moves: 128	coalesceable: 77	coalesced: 70
184 moves: 8	coalesceable: 8	coalesced: 8
185 moves: 111	coalesceable: 66	coalesced: 51
186 moves: 6	coalesceable: 6	coalesced: 6
187 moves: 427	coalesceable: 263	coalesced: 198
188 moves: 4	coalesceable: 4	coalesced: 4
189 moves: 5	coalesceable: 5	coalesced: 5
190 moves: 4	coalesceable: 4	coalesced: 4
191 moves: 64	coalesceable: 47	coalesced: 47

runtime: 18.0s,    gctime: 0.03184s,     systime: 0.17308s.
        external oracle real: 18.1s
        external oracle size: 135337
     apply colour (par) eval: runtime: 2m28s,    gctime: 3.9s,     systime: 5.1s.
     apply colour (par) real: 1m32s
     apply colour (par) size: 600401
           check colour eval: runtime: 1.9s,    gctime: 0.35547s,     systime: 0.01664s.
           check colour real: 1.9s
           check colour size: 600594
          word_to_stack eval: runtime: 1m46s,    gctime: 2.3s,     systime: 1.3s.
          word_to_stack real: 1m48s
          word_to_stack size: 504872
          stack_rawcall eval: runtime: 1m04s,    gctime: 1.0s,     systime: 0.83970s.
          stack_rawcall real: 1m05s
          stack_rawcall size: 492159
      stack_alloc (par) eval: runtime: 1m28s,    gctime: 1.2s,     systime: 3.5s.
      stack_alloc (par) real: 46.4s
      stack_alloc (par) size: 493462
expand stack_remove_def eval: runtime: 0.08372s,    gctime: 0.00000s,     systime: 0.02002s.
expand stack_remove_def real: 0.10379s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 2m02s,    gctime: 1.8s,     systime: 4.1s.
     stack_remove (par) real: 1m13s
     stack_remove (par) size: 841171
      stack_names (par) eval: runtime: 1m00s,    gctime: 1.4s,     systime: 1.2s.
      stack_names (par) real: 31.2s
      stack_names (par) size: 867870
     stack_to_lab (par) eval: runtime: 2m04s,    gctime: 2.6s,     systime: 4.0s.
     stack_to_lab (par) real: 1m05s
     stack_to_lab (par) size: 1053269
          lab_to_target eval: runtime: 7m46s,    gctime: 14.8s,     systime: 4.8s.
          lab_to_target real: 7m51s
          lab_to_target size: 1737600
                      export: runtime: 0.93296s,    gctime: 0.18371s,     systime: 0.05667s.
Saved theorem _______ "hello_compiled"
Exporting theory "helloCompile" ... Run out of store - interrupting threads

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