Job 1874

CakeML:4c966fba47c4550a982b3512dc6a08cc1ee4f7da
  Translate new mlmap functions [Apr 12 08:48:57]
#881 (mlmap-additions)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix [Apr 20 08:36:39]
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
  Fix some overlong lines [Apr 20 03:46:17]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 26 05:20:38 Claimed job
Apr 26 05:20:42 Building HOL
Apr 26 05:30:21 Starting developers
Apr 26 05:30:25 Finished developers                                               4s 140MB
Apr 26 05:30:25 Starting developers/bin
Apr 26 05:31:01 Finished developers/bin                                          35s   1GB
Apr 26 05:31:01 Starting semantics/ffi
Apr 26 05:31:10 Finished semantics/ffi                                            9s 246MB
Apr 26 05:31:10 Starting semantics
Apr 26 05:33:20 Finished semantics                                             2m09s   1GB
Apr 26 05:33:20 Starting semantics/proofs
Apr 26 05:37:29 Finished semantics/proofs                                      4m08s   2GB
Apr 26 05:37:29 Starting semantics/alt_semantics
Apr 26 05:37:53 Finished semantics/alt_semantics                                 23s 534MB
Apr 26 05:37:53 Starting semantics/alt_semantics/proofs
Apr 26 05:40:57 Finished semantics/alt_semantics/proofs                        3m03s   1GB
Apr 26 05:40:57 Starting basis/pure
Apr 26 05:44:37 Finished basis/pure                                            3m40s 891MB
Apr 26 05:44:38 Starting translator
Apr 26 05:47:39 Finished translator                                            3m01s   1GB
Apr 26 05:47:39 Starting compiler/parsing
Apr 26 05:48:56 Finished compiler/parsing                                      1m16s   2GB
Apr 26 05:48:56 Starting characteristic
Apr 26 05:55:14 Finished characteristic                                        6m17s   2GB
Apr 26 05:55:14 Starting translator/monadic
Apr 26 05:57:10 Finished translator/monadic                                    1m56s   1GB
Apr 26 05:57:10 Starting basis
Apr 26 06:44:02 Finished basis                                                46m50s  13GB
Apr 26 06:44:02 Starting compiler/inference
Apr 26 06:45:31 Finished compiler/inference                                    1m29s   1GB
Apr 26 06:45:31 Starting compiler/backend/reg_alloc
Apr 26 06:47:15 Finished compiler/backend/reg_alloc                            1m43s   1GB
Apr 26 06:47:15 Starting compiler/backend/gc
Apr 26 06:51:38 Finished compiler/backend/gc                                   4m23s   2GB
Apr 26 06:51:39 Starting compiler/backend
Apr 26 06:57:18 Finished compiler/backend                                      5m39s   2GB
Apr 26 06:57:18 Starting compiler/encoders/asm
Apr 26 06:57:48 Finished compiler/encoders/asm                                   30s 747MB
Apr 26 06:57:49 Starting compiler/encoders/x64
Apr 26 06:58:57 Finished compiler/encoders/x64                                 1m08s 865MB
Apr 26 06:58:57 Starting compiler/encoders/arm7
Apr 26 07:01:05 Finished compiler/encoders/arm7                                2m07s   1GB
Apr 26 07:01:05 Starting compiler/encoders/arm8
Apr 26 07:01:47 Finished compiler/encoders/arm8                                  42s 841MB
Apr 26 07:01:47 Starting compiler/encoders/arm8_asl
Apr 26 09:12:42 Finished compiler/encoders/arm8_asl                         2h10m52s  33GB
Apr 26 09:12:42 Starting compiler/encoders/mips
Apr 26 09:14:14 Finished compiler/encoders/mips                                1m31s   1GB
Apr 26 09:14:14 Starting compiler/encoders/riscv
Apr 26 09:16:03 Finished compiler/encoders/riscv                               1m48s   1GB
Apr 26 09:16:03 Starting compiler/encoders/ag32
Apr 26 09:16:24 Finished compiler/encoders/ag32                                  21s 668MB
Apr 26 09:16:25 Starting compiler/backend/x64
Apr 26 09:16:46 Finished compiler/backend/x64                                    21s   1GB
Apr 26 09:16:47 Starting compiler/backend/arm7
Apr 26 09:17:11 Finished compiler/backend/arm7                                   24s   1GB
Apr 26 09:17:11 Starting compiler/backend/arm8
Apr 26 09:17:32 Finished compiler/backend/arm8                                   21s   1GB
Apr 26 09:17:32 Starting compiler/backend/mips
Apr 26 09:17:54 Finished compiler/backend/mips                                   21s   1GB
Apr 26 09:17:55 Starting compiler/backend/riscv
Apr 26 09:18:18 Finished compiler/backend/riscv                                  22s   1GB
Apr 26 09:18:18 Starting compiler/backend/ag32
Apr 26 09:19:45 Finished compiler/backend/ag32                                 1m27s   1GB
Apr 26 09:19:45 Starting compiler/parsing/proofs
Apr 26 09:23:31 Finished compiler/parsing/proofs                               3m46s   1GB
Apr 26 09:23:31 Starting compiler/inference/proofs
Apr 26 09:26:07 Finished compiler/inference/proofs                             2m35s   1GB
Apr 26 09:26:07 Starting compiler/backend/semantics
Apr 26 09:54:42 Finished compiler/backend/semantics                           28m34s   2GB
Apr 26 09:54:42 Starting compiler/backend/reg_alloc/proofs
Apr 26 09:58:16 Finished compiler/backend/reg_alloc/proofs                     3m33s 995MB
Apr 26 09:58:16 Starting compiler/backend/proofs
Apr 26 10:49:09 Finished compiler/backend/proofs                              50m50s  16GB
Apr 26 10:49:10 Starting compiler/backend/serialiser
Apr 26 10:50:49 Finished compiler/backend/serialiser                           1m38s   2GB
Apr 26 10:50:49 Starting compiler/encoders/x64/proofs
Apr 26 11:00:15 Finished compiler/encoders/x64/proofs                          9m25s   5GB
Apr 26 11:00:15 Starting compiler/encoders/arm7/proofs
Apr 26 11:13:35 Finished compiler/encoders/arm7/proofs                        13m20s   4GB
Apr 26 11:13:36 Starting compiler/encoders/arm8/proofs
Apr 26 11:20:28 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
Apr 26 11:20:28 Starting compiler/encoders/arm8_asl/proofs
Apr 26 12:11:28 Finished compiler/encoders/arm8_asl/proofs                    50m58s  11GB
Apr 26 12:11:28 Starting compiler/encoders/mips/proofs
Apr 26 12:21:30 Finished compiler/encoders/mips/proofs                        10m01s   2GB
Apr 26 12:21:30 Starting compiler/encoders/riscv/proofs
Apr 26 12:30:15 Finished compiler/encoders/riscv/proofs                        8m45s   1GB
Apr 26 12:30:15 Starting compiler/encoders/ag32/proofs
Apr 26 12:32:50 Finished compiler/encoders/ag32/proofs                         2m34s 780MB
Apr 26 12:32:50 Starting compiler/backend/x64/proofs
Apr 26 12:33:18 Finished compiler/backend/x64/proofs                             28s   1GB
Apr 26 12:33:19 Starting compiler/backend/arm7/proofs
Apr 26 12:33:49 Finished compiler/backend/arm7/proofs                            29s   1GB
Apr 26 12:33:49 Starting compiler/backend/arm8/proofs
Apr 26 12:34:17 Finished compiler/backend/arm8/proofs                            28s   1GB
Apr 26 12:34:17 Starting compiler/backend/arm8_asl
Apr 26 12:34:40 Finished compiler/backend/arm8_asl                               22s   1GB
Apr 26 12:34:40 Starting compiler/backend/mips/proofs
Apr 26 12:35:10 Finished compiler/backend/mips/proofs                            29s   1GB
Apr 26 12:35:10 Starting compiler/backend/riscv/proofs
Apr 26 12:35:39 Finished compiler/backend/riscv/proofs                           28s   1GB
Apr 26 12:35:39 Starting compiler/backend/ag32/proofs
Apr 26 12:48:58 Finished compiler/backend/ag32/proofs                         13m19s   2GB
Apr 26 12:48:58 Starting compiler/proofs
Apr 26 12:51:22 Finished compiler/proofs                                       2m23s   3GB
Apr 26 12:51:23 Starting candle/set-theory
Apr 26 12:51:57 Finished candle/set-theory                                       34s   1GB
Apr 26 12:51:57 Starting candle/syntax-lib
Apr 26 12:52:11 Finished candle/syntax-lib                                       14s 650MB
Apr 26 12:52:11 Starting candle/standard/syntax
Apr 26 12:54:14 Finished candle/standard/syntax                                2m02s   1GB
Apr 26 12:54:14 Starting candle/standard/semantics
Apr 26 12:56:04 Finished candle/standard/semantics                             1m50s   1GB
Apr 26 12:56:04 Starting candle/standard/monadic
Apr 26 12:58:00 Finished candle/standard/monadic                               1m55s   1GB
Apr 26 12:58:00 Starting candle/standard/ml_kernel
Apr 26 13:04:02 Finished candle/standard/ml_kernel                             6m01s   3GB
Apr 26 13:04:02 Starting candle/overloading/syntax
Apr 26 13:07:15 Finished candle/overloading/syntax                             3m12s   1GB
Apr 26 13:07:15 Starting candle/overloading/semantics
Apr 26 13:19:21 Finished candle/overloading/semantics                         12m05s   2GB
Apr 26 13:19:21 Starting candle/overloading/monadic
Apr 26 13:21:52 Finished candle/overloading/monadic                            2m30s   2GB
Apr 26 13:21:52 Starting candle/overloading/ml_kernel
Apr 26 13:29:03 Finished candle/overloading/ml_kernel                          7m11s   3GB
Apr 26 13:29:03 Starting candle/overloading/ml_checker
Apr 26 13:31:29 Finished candle/overloading/ml_checker                         2m26s   3GB
Apr 26 13:31:30 Starting candle/prover
Apr 26 13:39:46 Finished candle/prover                                         8m16s   3GB
Apr 26 13:39:46 Starting pancake
Apr 26 13:43:30 Finished pancake                                               3m43s   3GB
Apr 26 13:43:30 Starting pancake/ffi
Apr 26 13:43:30 Finished pancake/ffi                                              0s  35MB
Apr 26 13:43:30 Starting pancake/semantics
Apr 26 13:45:59 Finished pancake/semantics                                     2m28s   1GB
Apr 26 13:45:59 Starting pancake/proofs
Apr 26 13:57:55 Finished pancake/proofs                                       11m56s   6GB
Apr 26 13:57:55 Starting characteristic/examples
Apr 26 13:59:18 Finished characteristic/examples                               1m22s   3GB
Apr 26 13:59:18 Starting tutorial/solutions
Apr 26 14:15:39 Finished tutorial/solutions                                   16m20s   8GB
Apr 26 14:15:39 Starting translator/monadic/examples
Apr 26 14:19:31 Finished translator/monadic/examples                           3m50s   2GB
Apr 26 14:19:31 Starting examples
Apr 26 14:29:08 Finished examples                                              9m37s   4GB
Apr 26 14:29:08 Starting examples/compilation/x64
Apr 26 16:01:04 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
/home/cug/hk324/cml-regression/cakeml-1874/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml  
Linking /home/cug/hk324/cml-regression/cakeml-1874/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-a161807cb4e0ea25b8781f3307a590b78703da6f/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cug/hk324/cml-regression/cakeml-1874/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: 11.7s,    gctime: 0.62750s,     systime: 0.03540s.
                to_flat real: 11.7s
                to_flat size: 81058
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.33046s,    gctime: 0.02782s,     systime: 0.00000s.
                to_clos real: 0.33049s
                to_clos size: 47193
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 5.1s,    gctime: 0.26461s,     systime: 0.01996s.
                 to_bvl real: 5.1s
                 to_bvl size: 79642
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 36.1s,    gctime: 0.92267s,     systime: 0.04267s.
                 to_bvi real: 36.1s
                 to_bvi size: 85205
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 12.5s,    gctime: 0.96633s,     systime: 0.07577s.
                to_data real: 12.5s
                to_data size: 134492
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 15.5s,    gctime: 1.3s,     systime: 0.05199s.
           data_to_word real: 15.6s
           data_to_word size: 408905
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m08s,    gctime: 7.5s,     systime: 0.75328s.
 inst,ssa,two-reg (par) real: 34.8s
 inst,ssa,two-reg (par) size: 1297263
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 46.6s,    gctime: 11.0s,     systime: 1.8s.
        get_clash (par) real: 19.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: 8.6s,    gctime: 0.01104s,     systime: 0.03597s.
        external oracle real: 8.7s
        external oracle size: 148063
     apply colour (par) eval: runtime: 1m16s,    gctime: 2.0s,     systime: 0.63450s.
     apply colour (par) real: 42.2s
     apply colour (par) size: 653969
           check colour eval: runtime: 1.3s,    gctime: 0.18838s,     systime: 0.01597s.
           check colour real: 1.3s
           check colour size: 654242
          word_to_stack eval: runtime: 52.4s,    gctime: 1.0s,     systime: 0.10777s.
          word_to_stack real: 52.5s
          word_to_stack size: 545672
          stack_rawcall eval: runtime: 34.0s,    gctime: 0.40103s,     systime: 0.05976s.
          stack_rawcall real: 34.1s
          stack_rawcall size: 531147
      stack_alloc (par) eval: runtime: 45.9s,    gctime: 0.54902s,     systime: 0.08402s.
      stack_alloc (par) real: 21.1s
      stack_alloc (par) size: 533137
expand stack_remove_def eval: runtime: 0.03430s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03432s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m02s,    gctime: 0.81930s,     systime: 0.10813s.
     stack_remove (par) real: 33.4s
     stack_remove (par) size: 904703
      stack_names (par) eval: runtime: 32.6s,    gctime: 0.73487s,     systime: 0.06812s.
      stack_names (par) real: 15.3s
      stack_names (par) size: 933448
     stack_to_lab (par) eval: runtime: 1m06s,    gctime: 1.2s,     systime: 0.13978s.
     stack_to_lab (par) real: 30.5s
     stack_to_lab (par) size: 1137272
          lab_to_target eval: runtime: 3m54s,    gctime: 6.3s,     systime: 0.62791s.
          lab_to_target real: 3m55s
          lab_to_target size: 1892860
                      export: runtime: 0.50501s,    gctime: 0.06283s,     systime: 0.04400s.
Saved theorem _______ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 14m03s to build
Linking /home/cug/hk324/cml-regression/cakeml-1874/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-a161807cb4e0ea25b8781f3307a590b78703da6f/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cug/hk324/cml-regression/cakeml-1874/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: 13.0s,    gctime: 0.57947s,     systime: 0.05513s.
                to_flat real: 13.0s
                to_flat size: 128212
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.70351s,    gctime: 0.03196s,     systime: 0.00789s.
                to_clos real: 0.71138s
                to_clos size: 69111
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 6.8s,    gctime: 0.27105s,     systime: 0.01572s.
                 to_bvl real: 6.9s
                 to_bvl size: 123714
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 45.1s,    gctime: 0.57022s,     systime: 0.03865s.
                 to_bvi real: 45.2s
                 to_bvi size: 123389
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 14.4s,    gctime: 0.78269s,     systime: 0.07185s.
                to_data real: 14.5s
                to_data size: 194553
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 19.3s,    gctime: 1.0s,     systime: 0.08374s.
           data_to_word real: 19.4s
           data_to_word size: 545668
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m43s,    gctime: 8.6s,     systime: 1.1s.
 inst,ssa,two-reg (par) real: 38.1s
 inst,ssa,two-reg (par) size: 1647340
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 1m45s,    gctime: 14.5s,     systime: 2.5s.
        get_clash (par) real: 28.5s
        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: 8.6s,    gctime: 0.01093s,     systime: 0.00396s.
        external oracle real: 8.6s
        external oracle size: 195137
     apply colour (par) eval: runtime: 2m00s,    gctime: 3.0s,     systime: 0.50218s.
     apply colour (par) real: 46.8s
     apply colour (par) size: 838432
           check colour eval: runtime: 2.8s,    gctime: 0.12619s,     systime: 0.01193s.
           check colour real: 2.8s
           check colour size: 838810
          word_to_stack eval: runtime: 1m09s,    gctime: 1.6s,     systime: 0.15466s.
          word_to_stack real: 1m09s
          word_to_stack size: 685501
          stack_rawcall eval: runtime: 43.9s,    gctime: 0.75323s,     systime: 0.05556s.
          stack_rawcall real: 44.0s
          stack_rawcall size: 665633
      stack_alloc (par) eval: runtime: 1m04s,    gctime: 0.98067s,     systime: 0.12727s.
      stack_alloc (par) real: 23.2s
      stack_alloc (par) size: 669518
expand stack_remove_def eval: runtime: 0.03617s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03620s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m30s,    gctime: 2.0s,     systime: 0.26851s.
     stack_remove (par) real: 36.1s
     stack_remove (par) size: 1118551
      stack_names (par) eval: runtime: 50.9s,    gctime: 6.9s,     systime: 0.78774s.
      stack_names (par) real: 21.9s
      stack_names (par) size: 1154903
     stack_to_lab (par) eval: runtime: 1m30s,    gctime: 2.1s,     systime: 0.21233s.
     stack_to_lab (par) real: 31.8s
     stack_to_lab (par) size: 1418892
          lab_to_target eval: runtime: 5m18s,    gctime: 36.2s,     systime: 3.0s.
          lab_to_target real: 5m21s
          lab_to_target size: 2390476
                      export: runtime: 0.48136s,    gctime: 0.00000s,     systime: 0.00001s.
Saved theorem _______ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 20m02s to build
Linking /home/cug/hk324/cml-regression/cakeml-1874/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-a161807cb4e0ea25b8781f3307a590b78703da6f/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cug/hk324/cml-regression/cakeml-1874/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: 11.9s,    gctime: 0.55735s,     systime: 0.03542s.
                to_flat real: 11.9s
                to_flat size: 75681
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.31841s,    gctime: 0.05279s,     systime: 0.00743s.
                to_clos real: 0.32585s
                to_clos size: 44318
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 4.8s,    gctime: 0.20419s,     systime: 0.01187s.
                 to_bvl real: 4.8s
                 to_bvl size: 70278
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 35.4s,    gctime: 0.46452s,     systime: 0.03859s.
                 to_bvi real: 35.4s
                 to_bvi size: 77188
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 11.9s,    gctime: 0.61009s,     systime: 0.09971s.
                to_data real: 12.0s
                to_data size: 126469
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 14.3s,    gctime: 0.53584s,     systime: 0.03578s.
           data_to_word real: 14.3s
           data_to_word size: 390464
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 1m05s,    gctime: 8.1s,     systime: 0.86558s.
 inst,ssa,two-reg (par) real: 35.3s
 inst,ssa,two-reg (par) size: 1265369
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 32.3s,    gctime: 6.1s,     systime: 0.84618s.
        get_clash (par) real: 13.4s
        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: 8.7s,    gctime: 0.01871s,     systime: 0.03587s.
        external oracle real: 8.7s
        external oracle size: 143336
     apply colour (par) eval: runtime: 1m11s,    gctime: 2.0s,     systime: 0.31446s.
     apply colour (par) real: 41.3s
     apply colour (par) size: 633178
           check colour eval: runtime: 1.1s,    gctime: 0.08166s,     systime: 0.01602s.
           check colour real: 1.1s
           check colour size: 633413
          word_to_stack eval: runtime: 51.4s,    gctime: 1.1s,     systime: 0.10755s.
          word_to_stack real: 51.5s
          word_to_stack size: 529655
          stack_rawcall eval: runtime: 33.1s,    gctime: 0.52970s,     systime: 0.08760s.
          stack_rawcall real: 33.2s
          stack_rawcall size: 515854
      stack_alloc (par) eval: runtime: 44.8s,    gctime: 0.64499s,     systime: 0.07974s.
      stack_alloc (par) real: 21.5s
      stack_alloc (par) size: 517544
expand stack_remove_def eval: runtime: 0.03507s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03510s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 1m00s,    gctime: 1.1s,     systime: 0.12084s.
     stack_remove (par) real: 33.4s
     stack_remove (par) size: 879421
      stack_names (par) eval: runtime: 31.8s,    gctime: 0.94097s,     systime: 0.09596s.
      stack_names (par) real: 15.4s
      stack_names (par) size: 907306
     stack_to_lab (par) eval: runtime: 1m09s,    gctime: 6.9s,     systime: 0.58169s.
     stack_to_lab (par) real: 36.2s
     stack_to_lab (par) size: 1103767
          lab_to_target eval: runtime: 3m56s,    gctime: 22.7s,     systime: 2.0s.
          lab_to_target real: 3m58s
          lab_to_target size: 1831446
                      export: runtime: 0.54148s,    gctime: 0.12100s,     systime: 0.03604s.
Saved theorem _______ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 13m30s to build
cc cat.S /home/cug/hk324/cml-regression/cakeml-1874/basis/basis_ffi.o  -o cake_cat
cc diff.S /home/cug/hk324/cml-regression/cakeml-1874/basis/basis_ffi.o  -o cake_diff
cc echo.S /home/cug/hk324/cml-regression/cakeml-1874/basis/basis_ffi.o  -o cake_echo
Linking /home/cug/hk324/cml-regression/cakeml-1874/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-a161807cb4e0ea25b8781f3307a590b78703da6f/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cug/hk324/cml-regression/cakeml-1874/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: 22.9s,    gctime: 0.94552s,     systime: 0.06260s.
                to_flat real: 22.9s
                to_flat size: 359797
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 2.8s,    gctime: 0.20896s,     systime: 0.01200s.
                to_clos real: 2.8s
                to_clos size: 165794
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 17.9s,    gctime: 0.98799s,     systime: 0.04745s.
                 to_bvl real: 18.0s
                 to_bvl size: 292435
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 1m41s,    gctime: 2.9s,     systime: 0.09887s.
                 to_bvi real: 1m41s
                 to_bvi size: 255802
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 33.2s,    gctime: 4.4s,     systime: 0.15995s.
                to_data real: 33.4s
                to_data size: 469789
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 1m06s,    gctime: 4.7s,     systime: 1.0s.
           data_to_word real: 1m07s
           data_to_word size: 1554448
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 11m33s,    gctime: 54.7s,     systime: 7.9s.
 inst,ssa,two-reg (par) real: 8m07s
 inst,ssa,two-reg (par) size: 4922846
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 6m50s,    gctime: 43.0s,     systime: 8.2s.
        get_clash (par) real: 1m36s
        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: 6m12s,    gctime: 0.17290s,     systime: 0.01898s.
        external oracle real: 6m12s
        external oracle size: 568447
     apply colour (par) eval: runtime: 6m17s,    gctime: 20.2s,     systime: 2.8s.
     apply colour (par) real: 2m25s
     apply colour (par) size: 2183011
           check colour eval: runtime: 17.7s,    gctime: 1.0s,     systime: 0.14799s.
           check colour real: 17.8s
           check colour size: 2183728
          word_to_stack eval: runtime: 2m30s,    gctime: 4.2s,     systime: 0.47998s.
          word_to_stack real: 2m30s
          word_to_stack size: 1747952
          stack_rawcall eval: runtime: 1m51s,    gctime: 2.3s,     systime: 0.23596s.
          stack_rawcall real: 1m51s
          stack_rawcall size: 1711785
      stack_alloc (par) eval: runtime: 2m57s,    gctime: 10.5s,     systime: 0.96688s.
      stack_alloc (par) real: 1m04s
      stack_alloc (par) size: 1728228
expand stack_remove_def eval: runtime: 0.13335s,    gctime: 0.09780s,     systime: 0.01198s.
expand stack_remove_def real: 0.14534s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 3m56s,    gctime: 22.7s,     systime: 1.5s.
     stack_remove (par) real: 1m23s
     stack_remove (par) size: 2831103
      stack_names (par) eval: runtime: 2m01s,    gctime: 2.4s,     systime: 1.4s.
      stack_names (par) real: 39.0s
      stack_names (par) size: 2924762
     stack_to_lab (par) eval: runtime: 4m03s,    gctime: 4.8s,     systime: 0.54431s.
     stack_to_lab (par) real: 1m23s
     stack_to_lab (par) size: 3565326
          lab_to_target eval: runtime: 10m03s,    gctime: 47.3s,     systime: 3.8s.
          lab_to_target real: 10m06s
          lab_to_target size: 5510811
                      export: runtime: 0.82216s,    gctime: 0.06956s,     systime: 0.00798s.
Saved theorem _______ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 1h04m14s to build
cc grep.S /home/cug/hk324/cml-regression/cakeml-1874/basis/basis_ffi.o  -o cake_grep
Linking /home/cug/hk324/cml-regression/cakeml-1874/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-a161807cb4e0ea25b8781f3307a590b78703da6f/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
  case (BitsN.fromBitstring ([c'2, ...], 3), p) of
     (BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
     (BitsN.B (...), [...]) => Zfull_inst (p, ...) |
     (... ..., ...) => Zfull_inst (...) |
     (...) => ... ... |
     ... => ... |
     ...
/home/cug/hk324/cml-regression/cakeml-1874/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: 11.7s,    gctime: 0.43755s,     systime: 0.27155s.
                to_flat real: 12.0s
                to_flat size: 64253
Saved definition ____ "flat_conf_def"
Saved definition ____ "flat_prog_def"
                to_clos eval: runtime: 0.18047s,    gctime: 0.00000s,     systime: 0.00000s.
                to_clos real: 0.18043s
                to_clos size: 37214
Saved definition ____ "clos_prog_def"
                 to_bvl eval: runtime: 4.3s,    gctime: 0.11645s,     systime: 0.00795s.
                 to_bvl real: 4.3s
                 to_bvl size: 57030
Saved definition ____ "bvl_conf_def"
Saved definition ____ "bvl_prog_def"
Saved definition ____ "bvl_names_def"
                 to_bvi eval: runtime: 33.2s,    gctime: 0.25307s,     systime: 0.02287s.
                 to_bvi real: 33.2s
                 to_bvi size: 65832
Saved definition ____ "bvi_conf_def"
Saved definition ____ "bvi_prog_def"
Saved definition ____ "bvi_names_def"
                to_data eval: runtime: 11.6s,    gctime: 0.54382s,     systime: 0.06394s.
                to_data real: 11.6s
                to_data size: 114783
Saved theorem _______ "to_data_thm"
           data_to_word eval: runtime: 13.6s,    gctime: 0.57420s,     systime: 0.05179s.
           data_to_word real: 13.7s
           data_to_word size: 365448
Saved definition ____ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 55.9s,    gctime: 2.7s,     systime: 0.27972s.
 inst,ssa,two-reg (par) real: 29.3s
 inst,ssa,two-reg (par) size: 1212078
Saved definition ____ "clash_fn_def"
        get_clash (par) eval: runtime: 28.1s,    gctime: 9.8s,     systime: 0.97372s.
        get_clash (par) real: 16.1s
        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: 7.5s,    gctime: 0.01988s,     systime: 0.03591s.
        external oracle real: 7.6s
        external oracle size: 135337
     apply colour (par) eval: runtime: 1m07s,    gctime: 2.4s,     systime: 0.20373s.
     apply colour (par) real: 41.8s
     apply colour (par) size: 600401
           check colour eval: runtime: 0.86988s,    gctime: 0.00000s,     systime: 0.00000s.
           check colour real: 0.86965s
           check colour size: 600594
          word_to_stack eval: runtime: 49.2s,    gctime: 1.4s,     systime: 0.06356s.
          word_to_stack real: 49.2s
          word_to_stack size: 504872
          stack_rawcall eval: runtime: 31.5s,    gctime: 0.47102s,     systime: 0.04782s.
          stack_rawcall real: 31.5s
          stack_rawcall size: 492159
      stack_alloc (par) eval: runtime: 41.8s,    gctime: 0.68614s,     systime: 0.09211s.
      stack_alloc (par) real: 21.0s
      stack_alloc (par) size: 493462
expand stack_remove_def eval: runtime: 0.03603s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03605s
expand stack_remove_def size: 3014
     stack_remove (par) eval: runtime: 57.3s,    gctime: 1.2s,     systime: 0.05963s.
     stack_remove (par) real: 33.1s
     stack_remove (par) size: 841171
      stack_names (par) eval: runtime: 29.8s,    gctime: 0.77338s,     systime: 0.05603s.
      stack_names (par) real: 15.2s
      stack_names (par) size: 867870
     stack_to_lab (par) eval: runtime: 1m00s,    gctime: 1.5s,     systime: 0.11611s.
     stack_to_lab (par) real: 30.6s
     stack_to_lab (par) size: 1053269
          lab_to_target eval: runtime: 3m36s,    gctime: 9.4s,     systime: 0.55967s.
          lab_to_target real: 3m37s
          lab_to_target size: 1737600
                      export: runtime: 0.50537s,    gctime: 0.08865s,     systime: 0.03202s.
Saved theorem _______ "hello_compiled"
Exporting theory "helloCompile" ... Run out of store - interrupting threads

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