Job 2544

CakeML:0fc61fd96b69ad3c042929fe8a3cf0e6c7313caf
  Remove DoubleProofScript.sml [Aug 04 16:53:12]
#1032 (new-double-ffi)
Merging into:ae3e90d1273790ae01f404316c1d547a3053c15a
  Merge pull request #1034 from CakeML/set-module [Aug 09 11:01:51]
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

Aug 10 10:13:51 Claimed job
Aug 10 10:13:55 Reusing HOL
Aug 10 10:14:05 Starting developers
Aug 10 10:14:09 Finished developers                                               2s 216MB
Aug 10 10:14:10 Starting developers/bin
Aug 10 10:14:20 Finished developers/bin                                           9s   1GB
Aug 10 10:14:21 Starting compiler/proofs
Aug 10 12:07:37 Finished compiler/proofs                                    1h53m14s  34GB
Aug 10 12:07:38 Starting compiler/bootstrap/translation
Aug 10 20:57:20 Finished compiler/bootstrap/translation                     8h49m40s  62GB
Aug 10 20:57:20 Starting semantics/ffi
Aug 10 20:57:29 Finished semantics/ffi                                            7s 657MB
Aug 10 20:57:30 Starting semantics
Aug 10 20:57:31 Finished semantics                                                0s  68MB
Aug 10 20:57:32 Starting semantics/proofs
Aug 10 20:58:09 Finished semantics/proofs                                        35s   1GB
Aug 10 20:58:10 Starting semantics/alt_semantics
Aug 10 20:58:58 Finished semantics/alt_semantics                                 47s   1GB
Aug 10 20:58:59 Starting semantics/alt_semantics/proofs
Aug 10 21:10:12 Finished semantics/alt_semantics/proofs                       11m11s   5GB
Aug 10 21:10:13 Starting basis/pure
Aug 10 21:10:14 Finished basis/pure                                               0s  76MB
Aug 10 21:10:15 Starting translator
Aug 10 21:11:59 Finished translator                                            1m43s   3GB
Aug 10 21:12:00 Starting compiler/parsing
Aug 10 21:12:01 Finished compiler/parsing                                         0s  73MB
Aug 10 21:12:02 Starting characteristic
Aug 10 21:12:04 Finished characteristic                                           0s  89MB
Aug 10 21:12:04 Starting translator/monadic
Aug 10 21:12:06 Finished translator/monadic                                       0s 101MB
Aug 10 21:12:07 Starting basis
Aug 10 21:14:41 Finished basis                                                 2m32s   5GB
Aug 10 21:14:41 Starting compiler/inference
Aug 10 21:14:43 Finished compiler/inference                                       0s  94MB
Aug 10 21:14:44 Starting compiler/backend/reg_alloc
Aug 10 21:14:45 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 10 21:14:46 Starting compiler/backend/gc
Aug 10 21:14:48 Finished compiler/backend/gc                                      0s 138MB
Aug 10 21:14:49 Starting compiler/backend
Aug 10 21:15:09 Finished compiler/backend                                        19s   1GB
Aug 10 21:15:10 Starting compiler/encoders/asm
Aug 10 21:15:11 Finished compiler/encoders/asm                                    0s  90MB
Aug 10 21:15:12 Starting compiler/encoders/x64
Aug 10 21:15:14 Finished compiler/encoders/x64                                    0s 103MB
Aug 10 21:15:14 Starting compiler/encoders/arm7
Aug 10 21:15:16 Finished compiler/encoders/arm7                                   0s 103MB
Aug 10 21:15:17 Starting compiler/encoders/arm8
Aug 10 21:15:18 Finished compiler/encoders/arm8                                   0s 102MB
Aug 10 21:15:19 Starting compiler/encoders/arm8_asl
Aug 10 21:17:30 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Aug 10 21:17:31 Starting compiler/encoders/mips
Aug 10 21:17:32 Finished compiler/encoders/mips                                   0s 103MB
Aug 10 21:17:33 Starting compiler/encoders/riscv
Aug 10 21:17:35 Finished compiler/encoders/riscv                                  0s 102MB
Aug 10 21:17:36 Starting compiler/encoders/ag32
Aug 10 21:17:37 Finished compiler/encoders/ag32                                   0s  98MB
Aug 10 21:17:38 Starting compiler/backend/x64
Aug 10 21:17:40 Finished compiler/backend/x64                                     0s 137MB
Aug 10 21:17:41 Starting compiler/backend/arm7
Aug 10 21:17:42 Finished compiler/backend/arm7                                    0s 137MB
Aug 10 21:17:43 Starting compiler/backend/arm8
Aug 10 21:17:45 Finished compiler/backend/arm8                                    0s 137MB
Aug 10 21:17:46 Starting compiler/backend/mips
Aug 10 21:17:48 Finished compiler/backend/mips                                    0s 137MB
Aug 10 21:17:49 Starting compiler/backend/riscv
Aug 10 21:17:50 Finished compiler/backend/riscv                                   0s 137MB
Aug 10 21:17:51 Starting compiler/backend/ag32
Aug 10 21:19:11 Finished compiler/backend/ag32                                 1m18s   2GB
Aug 10 21:19:12 Starting compiler/parsing/proofs
Aug 10 21:19:13 Finished compiler/parsing/proofs                                  0s  78MB
Aug 10 21:19:14 Starting compiler/inference/proofs
Aug 10 21:19:16 Finished compiler/inference/proofs                                0s  95MB
Aug 10 21:19:17 Starting compiler/backend/semantics
Aug 10 21:23:07 Finished compiler/backend/semantics                            3m49s   5GB
Aug 10 21:23:08 Starting compiler/backend/reg_alloc/proofs
Aug 10 21:23:10 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Aug 10 21:23:11 Starting compiler/backend/proofs
Aug 10 21:24:16 Finished compiler/backend/proofs                               1m04s   4GB
Aug 10 21:24:16 Starting compiler/backend/serialiser
Aug 10 21:24:18 Finished compiler/backend/serialiser                              0s 147MB
Aug 10 21:24:19 Starting compiler/encoders/x64/proofs
Aug 10 21:33:49 Finished compiler/encoders/x64/proofs                          9m28s   5GB
Aug 10 21:33:50 Starting compiler/encoders/arm7/proofs
Aug 10 21:46:33 Finished compiler/encoders/arm7/proofs                        12m42s   8GB
Aug 10 21:46:34 Starting compiler/encoders/arm8/proofs
Aug 10 21:53:19 Finished compiler/encoders/arm8/proofs                         6m43s   5GB
Aug 10 21:53:19 Starting compiler/encoders/arm8_asl/proofs
Aug 10 22:07:13 Finished compiler/encoders/arm8_asl/proofs                    13m52s   4GB
Aug 10 22:07:14 Starting compiler/encoders/mips/proofs
Aug 10 22:17:27 Finished compiler/encoders/mips/proofs                        10m12s   7GB
Aug 10 22:17:28 Starting compiler/encoders/riscv/proofs
Aug 10 22:25:43 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Aug 10 22:25:44 Starting compiler/encoders/ag32/proofs
Aug 10 22:28:08 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Aug 10 22:28:08 Starting compiler/backend/x64/proofs
Aug 10 22:28:50 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 10 22:28:51 Starting compiler/backend/arm7/proofs
Aug 10 22:29:35 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 10 22:29:36 Starting compiler/backend/arm8/proofs
Aug 10 22:30:20 Finished compiler/backend/arm8/proofs                            42s   3GB
Aug 10 22:30:21 Starting compiler/backend/arm8_asl
Aug 10 22:30:51 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 10 22:30:52 Starting compiler/backend/mips/proofs
Aug 10 22:31:39 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 10 22:31:40 Starting compiler/backend/riscv/proofs
Aug 10 22:32:32 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 10 22:32:33 Starting compiler/backend/ag32/proofs
Aug 10 22:46:39 Finished compiler/backend/ag32/proofs                         14m05s   6GB
Aug 10 22:46:40 Starting compiler/backend/cv_compute
Aug 10 22:48:25 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 10 22:48:26 Starting cv_translator
Aug 10 23:07:50 Finished cv_translator                                        19m23s  10GB
Aug 10 23:07:51 Starting candle/set-theory
Aug 10 23:08:40 Finished candle/set-theory                                       47s   1GB
Aug 10 23:08:41 Starting candle/syntax-lib
Aug 10 23:08:42 Finished candle/syntax-lib                                        0s  75MB
Aug 10 23:08:43 Starting candle/standard/syntax
Aug 10 23:09:02 Finished candle/standard/syntax                                  17s   1GB
Aug 10 23:09:03 Starting candle/standard/semantics
Aug 10 23:11:43 Finished candle/standard/semantics                             2m39s   3GB
Aug 10 23:11:44 Starting candle/standard/monadic
Aug 10 23:11:46 Finished candle/standard/monadic                                  0s  99MB
Aug 10 23:11:47 Starting candle/standard/ml_kernel
Aug 10 23:13:47 Finished candle/standard/ml_kernel                             1m59s   5GB
Aug 10 23:13:48 Starting candle/overloading/syntax
Aug 10 23:17:26 Finished candle/overloading/syntax                             3m37s   2GB
Aug 10 23:17:27 Starting candle/overloading/semantics
Aug 10 23:29:01 Finished candle/overloading/semantics                         11m32s   7GB
Aug 10 23:29:02 Starting candle/overloading/monadic
Aug 10 23:31:37 Finished candle/overloading/monadic                            2m34s   3GB
Aug 10 23:31:38 Starting candle/overloading/ml_kernel
Aug 10 23:39:30 Finished candle/overloading/ml_kernel                          7m50s   7GB
Aug 10 23:39:31 Starting candle/overloading/ml_checker
Aug 10 23:42:09 Finished candle/overloading/ml_checker                         2m37s   7GB
Aug 10 23:42:10 Starting candle/prover
Aug 10 23:52:31 Finished candle/prover                                        10m20s   5GB
Aug 10 23:52:32 Starting pancake
Aug 10 23:53:39 Finished pancake                                               1m05s   1GB
Aug 10 23:53:39 Starting pancake/ffi
Aug 10 23:53:40 Finished pancake/ffi                                              0s  23MB
Aug 10 23:53:41 Starting pancake/semantics
Aug 10 23:56:26 Finished pancake/semantics                                     2m44s   3GB
Aug 10 23:56:27 Starting pancake/parser
Aug 10 23:57:04 Finished pancake/parser                                          35s   2GB
Aug 10 23:57:05 Starting pancake/proofs
Aug 11 00:28:41 Finished pancake/proofs                                       31m35s   9GB
Aug 11 00:28:42 Starting characteristic/examples
Aug 11 00:30:24 Finished characteristic/examples                               1m40s   6GB
Aug 11 00:30:25 Starting tutorial/solutions
Aug 11 00:33:11 Finished tutorial/solutions                                    2m44s   4GB
Aug 11 00:33:12 Starting translator/monadic/examples
Aug 11 00:37:14 Finished translator/monadic/examples                           4m01s   5GB
Aug 11 00:37:15 Starting examples
Aug 11 00:52:07 Finished examples                                             14m50s   9GB
Aug 11 00:52:08 Starting examples/compilation/x64
Aug 11 00:54:27 FAILED: examples/compilation/x64
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/examples
Scanned 87 directories
/scratch/cakeml/regression2/cakeml-2544/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml test_interpreterScript.sml wordcountCompileScript.sml  
Linking /scratch/cakeml/regression2/cakeml-2544/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
<<HOL message: Created theory "catCompile">>
Saved theorem _______ "cat_prog_cv_eq"
Num regs: 9 Alg: IRC
0 moves: 68	coalesceable: 52	coalesced: 44
1 moves: 17	coalesceable: 17	coalesced: 15
2 moves: 84	coalesceable: 60	coalesced: 45
3 moves: 24	coalesceable: 18	coalesced: 16
4 moves: 13	coalesceable: 13	coalesced: 11
5 moves: 147	coalesceable: 115	coalesced: 109
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: 14	coalesceable: 13	coalesced: 10
12 moves: 41	coalesceable: 37	coalesced: 32
13 moves: 29	coalesceable: 20	coalesced: 17
14 moves: 52	coalesceable: 45	coalesced: 39
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 9	coalesceable: 7	coalesced: 4
17 moves: 9	coalesceable: 6	coalesced: 6
18 moves: 19	coalesceable: 19	coalesced: 19
19 moves: 20	coalesceable: 20	coalesced: 19
20 moves: 17	coalesceable: 14	coalesced: 14
21 moves: 32	coalesceable: 27	coalesced: 23
22 moves: 38	coalesceable: 32	coalesced: 31
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 14	coalesceable: 14	coalesced: 12
25 moves: 30	coalesceable: 27	coalesced: 20
26 moves: 17	coalesceable: 17	coalesced: 12
27 moves: 17	coalesceable: 15	coalesced: 8
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 279	coalesceable: 232	coalesced: 232
31 moves: 25	coalesceable: 22	coalesced: 22
32 moves: 22	coalesceable: 21	coalesced: 21
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 86	coalesceable: 77	coalesced: 77
36 moves: 81	coalesceable: 78	coalesced: 78
37 moves: 57	coalesceable: 54	coalesced: 54
38 moves: 71	coalesceable: 68	coalesced: 68
39 moves: 27	coalesceable: 24	coalesced: 24
40 moves: 45	coalesceable: 42	coalesced: 42
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 20	coalesceable: 17	coalesced: 17
45 moves: 49	coalesceable: 46	coalesced: 46
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 21	coalesceable: 18	coalesced: 18
49 moves: 25	coalesceable: 22	coalesced: 22
50 moves: 13	coalesceable: 12	coalesced: 12
51 moves: 19	coalesceable: 16	coalesced: 16
52 moves: 23	coalesceable: 20	coalesced: 20
53 moves: 189	coalesceable: 113	coalesced: 102
54 moves: 84	coalesceable: 58	coalesced: 41
55 moves: 35	coalesceable: 20	coalesced: 19
56 moves: 32	coalesceable: 22	coalesced: 17
57 moves: 51	coalesceable: 37	coalesced: 32
58 moves: 69	coalesceable: 44	coalesced: 38
59 moves: 43	coalesceable: 33	coalesced: 28
60 moves: 68	coalesceable: 43	coalesced: 34
61 moves: 932	coalesceable: 601	coalesced: 404
62 moves: 1094	coalesceable: 685	coalesced: 415
63 moves: 1176	coalesceable: 723	coalesced: 433
64 moves: 1262	coalesceable: 763	coalesced: 447
65 moves: 1352	coalesceable: 805	coalesced: 406
66 moves: 1445	coalesceable: 848	coalesced: 415
67 moves: 1543	coalesceable: 894	coalesced: 456
68 moves: 1646	coalesceable: 941	coalesced: 480
69 moves: 1752	coalesceable: 987	coalesced: 502
70 moves: 1862	coalesceable: 1033	coalesced: 504
71 moves: 13	coalesceable: 12	coalesced: 12
72 moves: 15	coalesceable: 14	coalesced: 14
73 moves: 14	coalesceable: 13	coalesced: 12
74 moves: 17	coalesceable: 16	coalesced: 16
75 moves: 16	coalesceable: 15	coalesced: 14
76 moves: 15	coalesceable: 14	coalesced: 13
77 moves: 19	coalesceable: 18	coalesced: 18
78 moves: 18	coalesceable: 17	coalesced: 16
79 moves: 17	coalesceable: 16	coalesced: 15
80 moves: 16	coalesceable: 15	coalesced: 14
81 moves: 21	coalesceable: 20	coalesced: 20
82 moves: 20	coalesceable: 19	coalesced: 18
83 moves: 19	coalesceable: 18	coalesced: 17
84 moves: 18	coalesceable: 17	coalesced: 16
85 moves: 17	coalesceable: 16	coalesced: 15
86 moves: 23	coalesceable: 21	coalesced: 17
87 moves: 22	coalesceable: 20	coalesced: 16
88 moves: 21	coalesceable: 19	coalesced: 15
89 moves: 20	coalesceable: 18	coalesced: 14
90 moves: 19	coalesceable: 17	coalesced: 13
91 moves: 18	coalesceable: 16	coalesced: 12
92 moves: 25	coalesceable: 22	coalesced: 19
93 moves: 24	coalesceable: 21	coalesced: 18
94 moves: 23	coalesceable: 20	coalesced: 17
95 moves: 22	coalesceable: 19	coalesced: 16
96 moves: 21	coalesceable: 18	coalesced: 15
97 moves: 20	coalesceable: 17	coalesced: 14
98 moves: 19	coalesceable: 16	coalesced: 13
99 moves: 27	coalesceable: 22	coalesced: 16
100 moves: 26	coalesceable: 22	coalesced: 16
101 moves: 25	coalesceable: 21	coalesced: 15
102 moves: 24	coalesceable: 20	coalesced: 14
103 moves: 23	coalesceable: 19	coalesced: 13
104 moves: 22	coalesceable: 18	coalesced: 12
105 moves: 21	coalesceable: 17	coalesced: 11
106 moves: 20	coalesceable: 16	coalesced: 10
107 moves: 29	coalesceable: 22	coalesced: 18
108 moves: 28	coalesceable: 22	coalesced: 18
109 moves: 27	coalesceable: 22	coalesced: 17
110 moves: 26	coalesceable: 21	coalesced: 16
111 moves: 25	coalesceable: 20	coalesced: 15
112 moves: 24	coalesceable: 19	coalesced: 14
113 moves: 23	coalesceable: 18	coalesced: 13
114 moves: 22	coalesceable: 17	coalesced: 12
115 moves: 21	coalesceable: 16	coalesced: 11
116 moves: 63	coalesceable: 12	coalesced: 8
117 moves: 5	coalesceable: 3	coalesced: 3
118 moves: 5	coalesceable: 3	coalesced: 3
119 moves: 16	coalesceable: 11	coalesced: 11
120 moves: 16	coalesceable: 10	coalesced: 10
121 moves: 16	coalesceable: 10	coalesced: 10
122 moves: 16	coalesceable: 10	coalesced: 10
123 moves: 16	coalesceable: 10	coalesced: 10
124 moves: 16	coalesceable: 10	coalesced: 10
125 moves: 16	coalesceable: 10	coalesced: 10
126 moves: 16	coalesceable: 10	coalesced: 10
127 moves: 16	coalesceable: 10	coalesced: 10
128 moves: 16	coalesceable: 10	coalesced: 10
129 moves: 16	coalesceable: 10	coalesced: 10
130 moves: 16	coalesceable: 10	coalesced: 10
131 moves: 16	coalesceable: 10	coalesced: 10
132 moves: 16	coalesceable: 10	coalesced: 10
133 moves: 16	coalesceable: 10	coalesced: 10
134 moves: 16	coalesceable: 10	coalesced: 10
135 moves: 24	coalesceable: 16	coalesced: 15
136 moves: 16	coalesceable: 10	coalesced: 10
137 moves: 16	coalesceable: 10	coalesced: 10
138 moves: 16	coalesceable: 10	coalesced: 10
139 moves: 30	coalesceable: 19	coalesced: 17
140 moves: 16	coalesceable: 10	coalesced: 10
141 moves: 16	coalesceable: 10	coalesced: 10
142 moves: 16	coalesceable: 10	coalesced: 10
143 moves: 16	coalesceable: 10	coalesced: 10
144 moves: 16	coalesceable: 10	coalesced: 10
145 moves: 16	coalesceable: 10	coalesced: 10
146 moves: 16	coalesceable: 10	coalesced: 10
147 moves: 16	coalesceable: 10	coalesced: 10
148 moves: 16	coalesceable: 10	coalesced: 10
149 moves: 16	coalesceable: 10	coalesced: 10
150 moves: 16	coalesceable: 10	coalesced: 10
151 moves: 16	coalesceable: 10	coalesced: 10
152 moves: 16	coalesceable: 10	coalesced: 10
153 moves: 10	coalesceable: 6	coalesced: 6
154 moves: 16	coalesceable: 10	coalesced: 10
155 moves: 16	coalesceable: 10	coalesced: 10
156 moves: 16	coalesceable: 10	coalesced: 10
157 moves: 16	coalesceable: 10	coalesced: 10
158 moves: 10	coalesceable: 6	coalesced: 6
159 moves: 15	coalesceable: 11	coalesced: 10
160 moves: 16	coalesceable: 10	coalesced: 10
161 moves: 16	coalesceable: 10	coalesced: 10
162 moves: 16	coalesceable: 10	coalesced: 10
163 moves: 16	coalesceable: 10	coalesced: 10
164 moves: 16	coalesceable: 10	coalesced: 10
165 moves: 16	coalesceable: 10	coalesced: 10
166 moves: 16	coalesceable: 10	coalesced: 10
167 moves: 16	coalesceable: 10	coalesced: 10
168 moves: 16	coalesceable: 10	coalesced: 10
169 moves: 16	coalesceable: 10	coalesced: 10
170 moves: 2	coalesceable: 2	coalesced: 2
171 moves: 16	coalesceable: 10	coalesced: 10
172 moves: 16	coalesceable: 10	coalesced: 10
173 moves: 16	coalesceable: 10	coalesced: 10
174 moves: 5	coalesceable: 3	coalesced: 3
175 moves: 6	coalesceable: 6	coalesced: 6
176 moves: 25	coalesceable: 18	coalesced: 11
177 moves: 4	coalesceable: 4	coalesced: 4
178 moves: 6	coalesceable: 6	coalesced: 6
179 moves: 4	coalesceable: 4	coalesced: 4
180 moves: 8	coalesceable: 8	coalesced: 7
181 moves: 8	coalesceable: 8	coalesced: 8
182 moves: 123	coalesceable: 71	coalesced: 57
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 60	coalesceable: 28	coalesced: 26
185 moves: 4	coalesceable: 4	coalesced: 4
186 moves: 47	coalesceable: 21	coalesced: 19
187 moves: 6	coalesceable: 6	coalesced: 6
188 moves: 20	coalesceable: 13	coalesced: 9
189 moves: 6	coalesceable: 6	coalesced: 6
190 moves: 20	coalesceable: 13	coalesced: 9
191 moves: 6	coalesceable: 6	coalesced: 6
192 moves: 25	coalesceable: 15	coalesced: 12
193 moves: 6	coalesceable: 6	coalesced: 6
194 moves: 24	coalesceable: 17	coalesced: 13
195 moves: 6	coalesceable: 6	coalesced: 6
196 moves: 20	coalesceable: 15	coalesced: 12
197 moves: 6	coalesceable: 6	coalesced: 6
198 moves: 20	coalesceable: 15	coalesced: 12
199 moves: 6	coalesceable: 6	coalesced: 6
200 moves: 26	coalesceable: 21	coalesced: 18
201 moves: 6	coalesceable: 6	coalesced: 6
202 moves: 26	coalesceable: 21	coalesced: 18
203 moves: 6	coalesceable: 6	coalesced: 6
204 moves: 60	coalesceable: 28	coalesced: 26
205 moves: 4	coalesceable: 4	coalesced: 4
206 moves: 3	coalesceable: 3	coalesced: 3
207 moves: 4	coalesceable: 4	coalesced: 4
208 moves: 42	coalesceable: 28	coalesced: 26
209 moves: 4	coalesceable: 4	coalesced: 4
210 moves: 3	coalesceable: 3	coalesced: 3
211 moves: 4	coalesceable: 4	coalesced: 4
212 moves: 18	coalesceable: 16	coalesced: 16
213 moves: 4	coalesceable: 4	coalesced: 4
214 moves: 21	coalesceable: 14	coalesced: 12
215 moves: 4	coalesceable: 4	coalesced: 4
216 moves: 3	coalesceable: 3	coalesced: 3
217 moves: 6	coalesceable: 6	coalesced: 6
218 moves: 34	coalesceable: 22	coalesced: 15
219 moves: 6	coalesceable: 6	coalesced: 6
220 moves: 17	coalesceable: 15	coalesced: 15
221 moves: 8	coalesceable: 8	coalesced: 8
222 moves: 17	coalesceable: 15	coalesced: 15
223 moves: 12	coalesceable: 12	coalesced: 12
224 moves: 216	coalesceable: 133	coalesced: 84
225 moves: 8	coalesceable: 8	coalesced: 8
226 moves: 123	coalesceable: 71	coalesced: 57
227 moves: 4	coalesceable: 4	coalesced: 4
228 moves: 76	coalesceable: 55	coalesced: 52
229 moves: 6	coalesceable: 6	coalesced: 6
230 moves: 104	coalesceable: 73	coalesced: 63
231 moves: 8	coalesceable: 8	coalesced: 8
232 moves: 428	coalesceable: 228	coalesced: 178
233 moves: 4	coalesceable: 4	coalesced: 4
234 moves: 60	coalesceable: 38	coalesced: 35
235 moves: 4	coalesceable: 4	coalesced: 4
236 moves: 8	coalesceable: 6	coalesced: 6
237 moves: 8	coalesceable: 8	coalesced: 8
238 moves: 157	coalesceable: 104	coalesced: 87
239 moves: 6	coalesceable: 6	coalesced: 6
240 moves: 111	coalesceable: 77	coalesced: 69
241 moves: 4	coalesceable: 4	coalesced: 4
242 moves: 5	coalesceable: 5	coalesced: 5
243 moves: 4	coalesceable: 4	coalesced: 4
244 moves: 5	coalesceable: 5	coalesced: 5
245 moves: 8	coalesceable: 8	coalesced: 8
246 moves: 128	coalesceable: 77	coalesced: 70
247 moves: 8	coalesceable: 8	coalesced: 8
248 moves: 111	coalesceable: 66	coalesced: 51
249 moves: 6	coalesceable: 6	coalesced: 6
250 moves: 46	coalesceable: 34	coalesced: 31
251 moves: 6	coalesceable: 6	coalesced: 6
252 moves: 434	coalesceable: 270	coalesced: 198
253 moves: 4	coalesceable: 4	coalesced: 4
254 moves: 5	coalesceable: 5	coalesced: 5
255 moves: 4	coalesceable: 4	coalesced: 4
256 moves: 276	coalesceable: 140	coalesced: 132
257 moves: 4	coalesceable: 4	coalesced: 4
258 moves: 68	coalesceable: 53	coalesced: 53
259 moves: 6	coalesceable: 6	coalesced: 6
260 moves: 55	coalesceable: 42	coalesced: 39
261 moves: 4	coalesceable: 4	coalesced: 4
262 moves: 21	coalesceable: 18	coalesced: 16
263 moves: 4	coalesceable: 4	coalesced: 4
264 moves: 17	coalesceable: 14	coalesced: 14
265 moves: 22	coalesceable: 18	coalesced: 18
266 moves: 23	coalesceable: 14	coalesced: 14
267 moves: 4	coalesceable: 4	coalesced: 4
268 moves: 35	coalesceable: 20	coalesced: 18
269 moves: 4	coalesceable: 4	coalesced: 4
270 moves: 12	coalesceable: 8	coalesced: 7
271 moves: 4	coalesceable: 4	coalesced: 4
272 moves: 11	coalesceable: 7	coalesced: 7

Saved theorem _______ "temp_oracle_cv_eq"
Saved theorem _______ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 29.1s to build
Linking /scratch/cakeml/regression2/cakeml-2544/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
<<HOL message: Created theory "diffCompile">>
Saved theorem _______ "diff_prog_cv_eq"
Num regs: 9 Alg: IRC
0 moves: 68	coalesceable: 52	coalesced: 44
1 moves: 17	coalesceable: 17	coalesced: 15
2 moves: 84	coalesceable: 60	coalesced: 45
3 moves: 24	coalesceable: 18	coalesced: 16
4 moves: 13	coalesceable: 13	coalesced: 11
5 moves: 147	coalesceable: 115	coalesced: 109
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: 14	coalesceable: 13	coalesced: 10
12 moves: 41	coalesceable: 37	coalesced: 32
13 moves: 29	coalesceable: 20	coalesced: 17
14 moves: 52	coalesceable: 45	coalesced: 39
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 9	coalesceable: 7	coalesced: 4
17 moves: 9	coalesceable: 6	coalesced: 6
18 moves: 19	coalesceable: 19	coalesced: 19
19 moves: 20	coalesceable: 20	coalesced: 19
20 moves: 17	coalesceable: 14	coalesced: 14
21 moves: 32	coalesceable: 27	coalesced: 23
22 moves: 38	coalesceable: 32	coalesced: 31
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 14	coalesceable: 14	coalesced: 12
25 moves: 30	coalesceable: 27	coalesced: 20
26 moves: 17	coalesceable: 17	coalesced: 12
27 moves: 17	coalesceable: 15	coalesced: 8
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 279	coalesceable: 232	coalesced: 232
31 moves: 25	coalesceable: 22	coalesced: 22
32 moves: 22	coalesceable: 21	coalesced: 21
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 86	coalesceable: 77	coalesced: 77
36 moves: 81	coalesceable: 78	coalesced: 78
37 moves: 57	coalesceable: 54	coalesced: 54
38 moves: 71	coalesceable: 68	coalesced: 68
39 moves: 27	coalesceable: 24	coalesced: 24
40 moves: 45	coalesceable: 42	coalesced: 42
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 20	coalesceable: 17	coalesced: 17
45 moves: 49	coalesceable: 46	coalesced: 46
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 21	coalesceable: 18	coalesced: 18
49 moves: 25	coalesceable: 22	coalesced: 22
50 moves: 13	coalesceable: 12	coalesced: 12
51 moves: 19	coalesceable: 16	coalesced: 16
52 moves: 23	coalesceable: 20	coalesced: 20
53 moves: 189	coalesceable: 113	coalesced: 102
54 moves: 84	coalesceable: 58	coalesced: 41
55 moves: 35	coalesceable: 20	coalesced: 19
56 moves: 32	coalesceable: 22	coalesced: 17
57 moves: 51	coalesceable: 37	coalesced: 32
58 moves: 69	coalesceable: 44	coalesced: 38
59 moves: 43	coalesceable: 33	coalesced: 28
60 moves: 68	coalesceable: 43	coalesced: 34
61 moves: 932	coalesceable: 601	coalesced: 404
62 moves: 1094	coalesceable: 685	coalesced: 415
63 moves: 1176	coalesceable: 723	coalesced: 433
64 moves: 1262	coalesceable: 763	coalesced: 447
65 moves: 1352	coalesceable: 805	coalesced: 406
66 moves: 1445	coalesceable: 848	coalesced: 415
67 moves: 1543	coalesceable: 894	coalesced: 456
68 moves: 1646	coalesceable: 941	coalesced: 480
69 moves: 1752	coalesceable: 987	coalesced: 502
70 moves: 1862	coalesceable: 1033	coalesced: 504
71 moves: 13	coalesceable: 12	coalesced: 12
72 moves: 15	coalesceable: 14	coalesced: 14
73 moves: 14	coalesceable: 13	coalesced: 12
74 moves: 17	coalesceable: 16	coalesced: 16
75 moves: 16	coalesceable: 15	coalesced: 14
76 moves: 15	coalesceable: 14	coalesced: 13
77 moves: 19	coalesceable: 18	coalesced: 18
78 moves: 18	coalesceable: 17	coalesced: 16
79 moves: 17	coalesceable: 16	coalesced: 15
80 moves: 16	coalesceable: 15	coalesced: 14
81 moves: 21	coalesceable: 20	coalesced: 20
82 moves: 20	coalesceable: 19	coalesced: 18
83 moves: 19	coalesceable: 18	coalesced: 17
84 moves: 18	coalesceable: 17	coalesced: 16
85 moves: 17	coalesceable: 16	coalesced: 15
86 moves: 23	coalesceable: 21	coalesced: 17
87 moves: 22	coalesceable: 20	coalesced: 16
88 moves: 21	coalesceable: 19	coalesced: 15
89 moves: 20	coalesceable: 18	coalesced: 14
90 moves: 19	coalesceable: 17	coalesced: 13
91 moves: 18	coalesceable: 16	coalesced: 12
92 moves: 25	coalesceable: 22	coalesced: 19
93 moves: 24	coalesceable: 21	coalesced: 18
94 moves: 23	coalesceable: 20	coalesced: 17
95 moves: 22	coalesceable: 19	coalesced: 16
96 moves: 21	coalesceable: 18	coalesced: 15
97 moves: 20	coalesceable: 17	coalesced: 14
98 moves: 19	coalesceable: 16	coalesced: 13
99 moves: 27	coalesceable: 22	coalesced: 16
100 moves: 26	coalesceable: 22	coalesced: 16
101 moves: 25	coalesceable: 21	coalesced: 15
102 moves: 24	coalesceable: 20	coalesced: 14
103 moves: 23	coalesceable: 19	coalesced: 13
104 moves: 22	coalesceable: 18	coalesced: 12
105 moves: 21	coalesceable: 17	coalesced: 11
106 moves: 20	coalesceable: 16	coalesced: 10
107 moves: 29	coalesceable: 22	coalesced: 18
108 moves: 28	coalesceable: 22	coalesced: 18
109 moves: 27	coalesceable: 22	coalesced: 17
110 moves: 26	coalesceable: 21	coalesced: 16
111 moves: 25	coalesceable: 20	coalesced: 15
112 moves: 24	coalesceable: 19	coalesced: 14
113 moves: 23	coalesceable: 18	coalesced: 13
114 moves: 22	coalesceable: 17	coalesced: 12
115 moves: 21	coalesceable: 16	coalesced: 11
116 moves: 63	coalesceable: 12	coalesced: 8
117 moves: 5	coalesceable: 3	coalesced: 3
118 moves: 5	coalesceable: 3	coalesced: 3
119 moves: 16	coalesceable: 11	coalesced: 11
120 moves: 16	coalesceable: 10	coalesced: 10
121 moves: 16	coalesceable: 10	coalesced: 10
122 moves: 16	coalesceable: 10	coalesced: 10
123 moves: 16	coalesceable: 10	coalesced: 10
124 moves: 16	coalesceable: 10	coalesced: 10
125 moves: 16	coalesceable: 10	coalesced: 10
126 moves: 16	coalesceable: 10	coalesced: 10
127 moves: 16	coalesceable: 10	coalesced: 10
128 moves: 16	coalesceable: 10	coalesced: 10
129 moves: 16	coalesceable: 10	coalesced: 10
130 moves: 16	coalesceable: 10	coalesced: 10
131 moves: 16	coalesceable: 10	coalesced: 10
132 moves: 16	coalesceable: 10	coalesced: 10
133 moves: 16	coalesceable: 10	coalesced: 10
134 moves: 16	coalesceable: 10	coalesced: 10
135 moves: 16	coalesceable: 10	coalesced: 10
136 moves: 16	coalesceable: 10	coalesced: 10
137 moves: 16	coalesceable: 10	coalesced: 10
138 moves: 16	coalesceable: 10	coalesced: 10
139 moves: 16	coalesceable: 10	coalesced: 10
140 moves: 16	coalesceable: 10	coalesced: 10
141 moves: 16	coalesceable: 10	coalesced: 10
142 moves: 16	coalesceable: 10	coalesced: 10
143 moves: 16	coalesceable: 10	coalesced: 10
144 moves: 16	coalesceable: 10	coalesced: 10
145 moves: 2	coalesceable: 2	coalesced: 2
146 moves: 16	coalesceable: 10	coalesced: 10
147 moves: 16	coalesceable: 10	coalesced: 10
148 moves: 16	coalesceable: 10	coalesced: 10
149 moves: 16	coalesceable: 10	coalesced: 10
150 moves: 24	coalesceable: 16	coalesced: 15
151 moves: 16	coalesceable: 10	coalesced: 10
152 moves: 16	coalesceable: 10	coalesced: 10
153 moves: 30	coalesceable: 19	coalesced: 17
154 moves: 16	coalesceable: 10	coalesced: 10
155 moves: 16	coalesceable: 10	coalesced: 10
156 moves: 16	coalesceable: 10	coalesced: 10
157 moves: 16	coalesceable: 10	coalesced: 10
158 moves: 16	coalesceable: 10	coalesced: 10
159 moves: 16	coalesceable: 10	coalesced: 10
160 moves: 16	coalesceable: 10	coalesced: 10
161 moves: 16	coalesceable: 10	coalesced: 10
162 moves: 16	coalesceable: 10	coalesced: 10
163 moves: 16	coalesceable: 10	coalesced: 10
164 moves: 16	coalesceable: 10	coalesced: 10
165 moves: 16	coalesceable: 10	coalesced: 10
166 moves: 16	coalesceable: 10	coalesced: 10
167 moves: 16	coalesceable: 10	coalesced: 10
168 moves: 10	coalesceable: 6	coalesced: 6
169 moves: 16	coalesceable: 10	coalesced: 10
170 moves: 16	coalesceable: 10	coalesced: 10
171 moves: 16	coalesceable: 10	coalesced: 10
172 moves: 16	coalesceable: 10	coalesced: 10
173 moves: 10	coalesceable: 6	coalesced: 6
174 moves: 15	coalesceable: 11	coalesced: 10
175 moves: 15	coalesceable: 11	coalesced: 10
176 moves: 16	coalesceable: 10	coalesced: 10
177 moves: 16	coalesceable: 10	coalesced: 10
178 moves: 16	coalesceable: 10	coalesced: 10
179 moves: 16	coalesceable: 10	coalesced: 10
180 moves: 16	coalesceable: 10	coalesced: 10
181 moves: 16	coalesceable: 10	coalesced: 10
182 moves: 16	coalesceable: 10	coalesced: 10
183 moves: 16	coalesceable: 10	coalesced: 10
184 moves: 16	coalesceable: 10	coalesced: 10
185 moves: 16	coalesceable: 10	coalesced: 10
186 moves: 16	coalesceable: 10	coalesced: 10
187 moves: 16	coalesceable: 10	coalesced: 10
188 moves: 16	coalesceable: 10	coalesced: 10
189 moves: 2	coalesceable: 2	coalesced: 2
190 moves: 16	coalesceable: 10	coalesced: 10
191 moves: 16	coalesceable: 10	coalesced: 10
192 moves: 16	coalesceable: 10	coalesced: 10
193 moves: 16	coalesceable: 10	coalesced: 10
194 moves: 16	coalesceable: 10	coalesced: 10
195 moves: 16	coalesceable: 10	coalesced: 10
196 moves: 16	coalesceable: 10	coalesced: 10
197 moves: 16	coalesceable: 10	coalesced: 10
198 moves: 16	coalesceable: 10	coalesced: 10
199 moves: 16	coalesceable: 10	coalesced: 10
200 moves: 16	coalesceable: 10	coalesced: 10
201 moves: 16	coalesceable: 10	coalesced: 10
202 moves: 16	coalesceable: 10	coalesced: 10
203 moves: 16	coalesceable: 10	coalesced: 10
204 moves: 16	coalesceable: 10	coalesced: 10
205 moves: 16	coalesceable: 10	coalesced: 10
206 moves: 15	coalesceable: 11	coalesced: 10
207 moves: 16	coalesceable: 10	coalesced: 10
208 moves: 16	coalesceable: 10	coalesced: 10
209 moves: 5	coalesceable: 3	coalesced: 3
210 moves: 4	coalesceable: 4	coalesced: 4
211 moves: 5	coalesceable: 5	coalesced: 5
212 moves: 6	coalesceable: 6	coalesced: 6
213 moves: 25	coalesceable: 18	coalesced: 11
214 moves: 6	coalesceable: 6	coalesced: 6
215 moves: 29	coalesceable: 20	coalesced: 15
216 moves: 4	coalesceable: 4	coalesced: 4
217 moves: 5	coalesceable: 5	coalesced: 3
218 moves: 6	coalesceable: 6	coalesced: 6
219 moves: 33	coalesceable: 22	coalesced: 21
220 moves: 4	coalesceable: 4	coalesced: 4
221 moves: 5	coalesceable: 5	coalesced: 3
222 moves: 4	coalesceable: 4	coalesced: 4
223 moves: 6	coalesceable: 6	coalesced: 6
224 moves: 4	coalesceable: 4	coalesced: 4
225 moves: 6	coalesceable: 6	coalesced: 6
226 moves: 4	coalesceable: 4	coalesced: 4
227 moves: 8	coalesceable: 8	coalesced: 7
228 moves: 6	coalesceable: 6	coalesced: 6
229 moves: 79	coalesceable: 51	coalesced: 45
230 moves: 6	coalesceable: 6	coalesced: 6
231 moves: 68	coalesceable: 41	coalesced: 37
232 moves: 6	coalesceable: 6	coalesced: 6
233 moves: 135	coalesceable: 82	coalesced: 76
234 moves: 4	coalesceable: 4	coalesced: 4
235 moves: 8	coalesceable: 8	coalesced: 7
236 moves: 8	coalesceable: 8	coalesced: 8
237 moves: 123	coalesceable: 71	coalesced: 57
238 moves: 6	coalesceable: 6	coalesced: 6
239 moves: 60	coalesceable: 28	coalesced: 26
240 moves: 4	coalesceable: 4	coalesced: 4
241 moves: 47	coalesceable: 21	coalesced: 19
242 moves: 6	coalesceable: 6	coalesced: 6
243 moves: 20	coalesceable: 13	coalesced: 9
244 moves: 6	coalesceable: 6	coalesced: 6
245 moves: 20	coalesceable: 13	coalesced: 9
246 moves: 6	coalesceable: 6	coalesced: 6
247 moves: 25	coalesceable: 15	coalesced: 12
248 moves: 6	coalesceable: 6	coalesced: 6
249 moves: 24	coalesceable: 17	coalesced: 13
250 moves: 6	coalesceable: 6	coalesced: 6
251 moves: 20	coalesceable: 15	coalesced: 12
252 moves: 6	coalesceable: 6	coalesced: 6
253 moves: 20	coalesceable: 15	coalesced: 12
254 moves: 6	coalesceable: 6	coalesced: 6
255 moves: 26	coalesceable: 21	coalesced: 18
256 moves: 6	coalesceable: 6	coalesced: 6
257 moves: 26	coalesceable: 21	coalesced: 18
258 moves: 6	coalesceable: 6	coalesced: 6
259 moves: 60	coalesceable: 28	coalesced: 26
260 moves: 4	coalesceable: 4	coalesced: 4
261 moves: 161	coalesceable: 106	coalesced: 98
262 moves: 10	coalesceable: 10	coalesced: 10
263 moves: 349	coalesceable: 210	coalesced: 161
264 moves: 6	coalesceable: 6	coalesced: 6
265 moves: 206	coalesceable: 114	coalesced: 84
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: 42	coalesceable: 28	coalesced: 26
272 moves: 4	coalesceable: 4	coalesced: 4
273 moves: 21	coalesceable: 14	coalesced: 12
274 moves: 4	coalesceable: 4	coalesced: 4
275 moves: 3	coalesceable: 3	coalesced: 3
276 moves: 6	coalesceable: 6	coalesced: 6
277 moves: 34	coalesceable: 22	coalesced: 15
278 moves: 6	coalesceable: 6	coalesced: 6
279 moves: 17	coalesceable: 15	coalesced: 15
280 moves: 4	coalesceable: 4	coalesced: 4
281 moves: 8	coalesceable: 8	coalesced: 7
282 moves: 8	coalesceable: 8	coalesced: 8
283 moves: 17	coalesceable: 15	coalesced: 15
284 moves: 12	coalesceable: 12	coalesced: 12
285 moves: 216	coalesceable: 133	coalesced: 84
286 moves: 12	coalesceable: 12	coalesced: 12
287 moves: 216	coalesceable: 133	coalesced: 84
288 moves: 8	coalesceable: 8	coalesced: 8
289 moves: 123	coalesceable: 71	coalesced: 57
290 moves: 4	coalesceable: 4	coalesced: 4
291 moves: 76	coalesceable: 55	coalesced: 52
292 moves: 6	coalesceable: 6	coalesced: 6
293 moves: 104	coalesceable: 73	coalesced: 63
294 moves: 8	coalesceable: 8	coalesced: 8
295 moves: 428	coalesceable: 228	coalesced: 178
296 moves: 4	coalesceable: 4	coalesced: 4
297 moves: 60	coalesceable: 38	coalesced: 35
298 moves: 4	coalesceable: 4	coalesced: 4
299 moves: 8	coalesceable: 6	coalesced: 6
300 moves: 8	coalesceable: 8	coalesced: 8
301 moves: 157	coalesceable: 104	coalesced: 87
302 moves: 6	coalesceable: 6	coalesced: 6
303 moves: 111	coalesceable: 77	coalesced: 69
304 moves: 4	coalesceable: 4	coalesced: 4
305 moves: 5	coalesceable: 5	coalesced: 5
306 moves: 4	coalesceable: 4	coalesced: 4
307 moves: 5	coalesceable: 5	coalesced: 5
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: 434	coalesceable: 270	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: 13	coalesceable: 9	coalesced: 8
318 moves: 4	coalesceable: 4	coalesced: 4
319 moves: 276	coalesceable: 140	coalesced: 132
320 moves: 4	coalesceable: 4	coalesced: 4
321 moves: 68	coalesceable: 53	coalesced: 53
322 moves: 6	coalesceable: 6	coalesced: 6
323 moves: 55	coalesceable: 42	coalesced: 39
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: 105	coalesced: 89
328 moves: 222	coalesceable: 136	coalesced: 113
329 moves: 217	coalesceable: 131	coalesced: 107
330 moves: 4	coalesceable: 4	coalesced: 4
331 moves: 42	coalesceable: 23	coalesced: 21
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: 87	coalesceable: 53	coalesced: 53
339 moves: 12	coalesceable: 12	coalesced: 12
340 moves: 354	coalesceable: 160	coalesced: 98
341 moves: 8	coalesceable: 8	coalesced: 8
342 moves: 65	coalesceable: 44	coalesced: 37
343 moves: 6	coalesceable: 6	coalesced: 6
344 moves: 81	coalesceable: 49	coalesced: 40
345 moves: 6	coalesceable: 6	coalesced: 6
346 moves: 51	coalesceable: 26	coalesced: 21
347 moves: 6	coalesceable: 6	coalesced: 6
348 moves: 82	coalesceable: 55	coalesced: 51
349 moves: 8	coalesceable: 8	coalesced: 8
350 moves: 87	coalesceable: 62	coalesced: 45
351 moves: 6	coalesceable: 6	coalesced: 6
352 moves: 92	coalesceable: 56	coalesced: 51
353 moves: 6	coalesceable: 6	coalesced: 6
354 moves: 280	coalesceable: 127	coalesced: 112
355 moves: 6	coalesceable: 6	coalesced: 6
356 moves: 7	coalesceable: 7	coalesced: 7
357 moves: 10	coalesceable: 10	coalesced: 10
358 moves: 384	coalesceable: 147	coalesced: 124
359 moves: 6	coalesceable: 6	coalesced: 6
360 moves: 35	coalesceable: 25	coalesced: 20
361 moves: 10	coalesceable: 10	coalesced: 10
362 moves: 882	coalesceable: 395	coalesced: 337
363 moves: 32	coalesceable: 24	coalesced: 22
364 moves: 32	coalesceable: 24	coalesced: 22
365 moves: 12	coalesceable: 12	coalesced: 12
366 moves: 1498	coalesceable: 756	coalesced: 616
367 moves: 6	coalesceable: 6	coalesced: 6
368 moves: 685	coalesceable: 350	coalesced: 209
369 moves: 4	coalesceable: 4	coalesced: 4
370 moves: 72	coalesceable: 40	coalesced: 37
371 moves: 6	coalesceable: 6	coalesced: 6
372 moves: 186	coalesceable: 103	coalesced: 100
373 moves: 4	coalesceable: 4	coalesced: 4
374 moves: 44	coalesceable: 36	coalesced: 36

Saved theorem _______ "temp_oracle_cv_eq"
Saved theorem _______ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 35.5s to build
Linking /scratch/cakeml/regression2/cakeml-2544/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
<<HOL message: Created theory "echoCompile">>
Saved theorem _______ "echo_prog_cv_eq"
Num regs: 9 Alg: IRC
0 moves: 68	coalesceable: 52	coalesced: 44
1 moves: 17	coalesceable: 17	coalesced: 15
2 moves: 84	coalesceable: 60	coalesced: 45
3 moves: 24	coalesceable: 18	coalesced: 16
4 moves: 13	coalesceable: 13	coalesced: 11
5 moves: 147	coalesceable: 115	coalesced: 109
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: 14	coalesceable: 13	coalesced: 10
12 moves: 41	coalesceable: 37	coalesced: 32
13 moves: 29	coalesceable: 20	coalesced: 17
14 moves: 52	coalesceable: 45	coalesced: 39
15 moves: 0	coalesceable: 0	coalesced: 0
16 moves: 9	coalesceable: 7	coalesced: 4
17 moves: 9	coalesceable: 6	coalesced: 6
18 moves: 19	coalesceable: 19	coalesced: 19
19 moves: 20	coalesceable: 20	coalesced: 19
20 moves: 17	coalesceable: 14	coalesced: 14
21 moves: 32	coalesceable: 27	coalesced: 23
22 moves: 38	coalesceable: 32	coalesced: 31
23 moves: 0	coalesceable: 0	coalesced: 0
24 moves: 14	coalesceable: 14	coalesced: 12
25 moves: 30	coalesceable: 27	coalesced: 20
26 moves: 17	coalesceable: 17	coalesced: 12
27 moves: 17	coalesceable: 15	coalesced: 8
28 moves: 0	coalesceable: 0	coalesced: 0
29 moves: 0	coalesceable: 0	coalesced: 0
30 moves: 279	coalesceable: 232	coalesced: 232
31 moves: 25	coalesceable: 22	coalesced: 22
32 moves: 22	coalesceable: 21	coalesced: 21
33 moves: 16	coalesceable: 15	coalesced: 15
34 moves: 22	coalesceable: 19	coalesced: 19
35 moves: 86	coalesceable: 77	coalesced: 77
36 moves: 81	coalesceable: 78	coalesced: 78
37 moves: 57	coalesceable: 54	coalesced: 54
38 moves: 71	coalesceable: 68	coalesced: 68
39 moves: 27	coalesceable: 24	coalesced: 24
40 moves: 45	coalesceable: 42	coalesced: 42
41 moves: 7	coalesceable: 6	coalesced: 6
42 moves: 22	coalesceable: 19	coalesced: 19
43 moves: 12	coalesceable: 11	coalesced: 11
44 moves: 20	coalesceable: 17	coalesced: 17
45 moves: 49	coalesceable: 46	coalesced: 46
46 moves: 8	coalesceable: 7	coalesced: 7
47 moves: 11	coalesceable: 10	coalesced: 10
48 moves: 21	coalesceable: 18	coalesced: 18
49 moves: 25	coalesceable: 22	coalesced: 22
50 moves: 13	coalesceable: 12	coalesced: 12
51 moves: 19	coalesceable: 16	coalesced: 16
52 moves: 23	coalesceable: 20	coalesced: 20
53 moves: 189	coalesceable: 113	coalesced: 102
54 moves: 84	coalesceable: 58	coalesced: 41
55 moves: 35	coalesceable: 20	coalesced: 19
56 moves: 32	coalesceable: 22	coalesced: 17
57 moves: 51	coalesceable: 37	coalesced: 32
58 moves: 69	coalesceable: 44	coalesced: 38
59 moves: 43	coalesceable: 33	coalesced: 28
60 moves: 68	coalesceable: 43	coalesced: 34
61 moves: 932	coalesceable: 601	coalesced: 404
62 moves: 1094	coalesceable: 685	coalesced: 415
63 moves: 1176	coalesceable: 723	coalesced: 433
64 moves: 1262	coalesceable: 763	coalesced: 447
65 moves: 1352	coalesceable: 805	coalesced: 406
66 moves: 1445	coalesceable: 848	coalesced: 415
67 moves: 1543	coalesceable: 894	coalesced: 456
68 moves: 1646	coalesceable: 941	coalesced: 480
69 moves: 1752	coalesceable: 987	coalesced: 502
70 moves: 1862	coalesceable: 1033	coalesced: 504
71 moves: 13	coalesceable: 12	coalesced: 12
72 moves: 15	coalesceable: 14	coalesced: 14
73 moves: 14	coalesceable: 13	coalesced: 12
74 moves: 17	coalesceable: 16	coalesced: 16
75 moves: 16	coalesceable: 15	coalesced: 14
76 moves: 15	coalesceable: 14	coalesced: 13
77 moves: 19	coalesceable: 18	coalesced: 18
78 moves: 18	coalesceable: 17	coalesced: 16
79 moves: 17	coalesceable: 16	coalesced: 15
80 moves: 16	coalesceable: 15	coalesced: 14
81 moves: 21	coalesceable: 20	coalesced: 20
82 moves: 20	coalesceable: 19	coalesced: 18
83 moves: 19	coalesceable: 18	coalesced: 17
84 moves: 18	coalesceable: 17	coalesced: 16
85 moves: 17	coalesceable: 16	coalesced: 15
86 moves: 23	coalesceable: 21	coalesced: 17
87 moves: 22	coalesceable: 20	coalesced: 16
88 moves: 21	coalesceable: 19	coalesced: 15
89 moves: 20	coalesceable: 18	coalesced: 14
90 moves: 19	coalesceable: 17	coalesced: 13
91 moves: 18	coalesceable: 16	coalesced: 12
92 moves: 25	coalesceable: 22	coalesced: 19
93 moves: 24	coalesceable: 21	coalesced: 18
94 moves: 23	coalesceable: 20	coalesced: 17
95 moves: 22	coalesceable: 19	coalesced: 16
96 moves: 21	coalesceable: 18	coalesced: 15
97 moves: 20	coalesceable: 17	coalesced: 14
98 moves: 19	coalesceable: 16	coalesced: 13
99 moves: 27	coalesceable: 22	coalesced: 16
100 moves: 26	coalesceable: 22	coalesced: 16
101 moves: 25	coalesceable: 21	coalesced: 15
102 moves: 24	coalesceable: 20	coalesced: 14
103 moves: 23	coalesceable: 19	coalesced: 13
104 moves: 22	coalesceable: 18	coalesced: 12
105 moves: 21	coalesceable: 17	coalesced: 11
106 moves: 20	coalesceable: 16	coalesced: 10
107 moves: 29	coalesceable: 22	coalesced: 18
108 moves: 28	coalesceable: 22	coalesced: 18
109 moves: 27	coalesceable: 22	coalesced: 17
110 moves: 26	coalesceable: 21	coalesced: 16
111 moves: 25	coalesceable: 20	coalesced: 15
112 moves: 24	coalesceable: 19	coalesced: 14
113 moves: 23	coalesceable: 18	coalesced: 13
114 moves: 22	coalesceable: 17	coalesced: 12
115 moves: 21	coalesceable: 16	coalesced: 11
116 moves: 63	coalesceable: 12	coalesced: 8
117 moves: 5	coalesceable: 3	coalesced: 3
118 moves: 5	coalesceable: 3	coalesced: 3
119 moves: 16	coalesceable: 11	coalesced: 11
120 moves: 16	coalesceable: 10	coalesced: 10
121 moves: 16	coalesceable: 10	coalesced: 10
122 moves: 16	coalesceable: 10	coalesced: 10
123 moves: 16	coalesceable: 10	coalesced: 10
124 moves: 16	coalesceable: 10	coalesced: 10
125 moves: 16	coalesceable: 10	coalesced: 10
126 moves: 16	coalesceable: 10	coalesced: 10
127 moves: 16	coalesceable: 10	coalesced: 10
128 moves: 16	coalesceable: 10	coalesced: 10
129 moves: 16	coalesceable: 10	coalesced: 10
130 moves: 16	coalesceable: 10	coalesced: 10
131 moves: 16	coalesceable: 10	coalesced: 10
132 moves: 16	coalesceable: 10	coalesced: 10
133 moves: 16	coalesceable: 10	coalesced: 10
134 moves: 24	coalesceable: 16	coalesced: 15
135 moves: 16	coalesceable: 10	coalesced: 10
136 moves: 30	coalesceable: 19	coalesced: 17
137 moves: 16	coalesceable: 10	coalesced: 10
138 moves: 16	coalesceable: 10	coalesced: 10
139 moves: 16	coalesceable: 10	coalesced: 10
140 moves: 16	coalesceable: 10	coalesced: 10
141 moves: 16	coalesceable: 10	coalesced: 10
142 moves: 16	coalesceable: 10	coalesced: 10
143 moves: 16	coalesceable: 10	coalesced: 10
144 moves: 16	coalesceable: 10	coalesced: 10
145 moves: 16	coalesceable: 10	coalesced: 10
146 moves: 16	coalesceable: 10	coalesced: 10
147 moves: 16	coalesceable: 10	coalesced: 10
148 moves: 16	coalesceable: 10	coalesced: 10
149 moves: 10	coalesceable: 6	coalesced: 6
150 moves: 16	coalesceable: 10	coalesced: 10
151 moves: 16	coalesceable: 10	coalesced: 10
152 moves: 16	coalesceable: 10	coalesced: 10
153 moves: 10	coalesceable: 6	coalesced: 6
154 moves: 15	coalesceable: 11	coalesced: 10
155 moves: 16	coalesceable: 10	coalesced: 10
156 moves: 16	coalesceable: 10	coalesced: 10
157 moves: 16	coalesceable: 10	coalesced: 10
158 moves: 16	coalesceable: 10	coalesced: 10
159 moves: 16	coalesceable: 10	coalesced: 10
160 moves: 2	coalesceable: 2	coalesced: 2
161 moves: 16	coalesceable: 10	coalesced: 10
162 moves: 5	coalesceable: 3	coalesced: 3
163 moves: 6	coalesceable: 6	coalesced: 6
164 moves: 25	coalesceable: 18	coalesced: 11
165 moves: 4	coalesceable: 4	coalesced: 4
166 moves: 6	coalesceable: 6	coalesced: 6
167 moves: 4	coalesceable: 4	coalesced: 4
168 moves: 8	coalesceable: 8	coalesced: 7
169 moves: 8	coalesceable: 8	coalesced: 8
170 moves: 123	coalesceable: 71	coalesced: 57
171 moves: 6	coalesceable: 6	coalesced: 6
172 moves: 60	coalesceable: 28	coalesced: 26
173 moves: 8	coalesceable: 8	coalesced: 8
174 moves: 184	coalesceable: 97	coalesced: 90
175 moves: 6	coalesceable: 6	coalesced: 6
176 moves: 7	coalesceable: 7	coalesced: 4
177 moves: 6	coalesceable: 6	coalesced: 6
178 moves: 20	coalesceable: 13	coalesced: 9
179 moves: 6	coalesceable: 6	coalesced: 6
180 moves: 20	coalesceable: 13	coalesced: 9
181 moves: 6	coalesceable: 6	coalesced: 6
182 moves: 25	coalesceable: 15	coalesced: 12
183 moves: 6	coalesceable: 6	coalesced: 6
184 moves: 24	coalesceable: 17	coalesced: 13
185 moves: 6	coalesceable: 6	coalesced: 6
186 moves: 20	coalesceable: 15	coalesced: 12
187 moves: 6	coalesceable: 6	coalesced: 6
188 moves: 20	coalesceable: 15	coalesced: 12
189 moves: 6	coalesceable: 6	coalesced: 6
190 moves: 26	coalesceable: 21	coalesced: 18
191 moves: 4	coalesceable: 4	coalesced: 4
192 moves: 3	coalesceable: 3	coalesced: 3
193 moves: 4	coalesceable: 4	coalesced: 4
194 moves: 21	coalesceable: 14	coalesced: 12
195 moves: 4	coalesceable: 4	coalesced: 4
196 moves: 3	coalesceable: 3	coalesced: 3
197 moves: 6	coalesceable: 6	coalesced: 6
198 moves: 34	coalesceable: 22	coalesced: 15
199 moves: 6	coalesceable: 6	coalesced: 6
200 moves: 17	coalesceable: 15	coalesced: 15
201 moves: 8	coalesceable: 8	coalesced: 8
202 moves: 17	coalesceable: 15	coalesced: 15
203 moves: 12	coalesceable: 12	coalesced: 12
204 moves: 216	coalesceable: 133	coalesced: 84
205 moves: 8	coalesceable: 8	coalesced: 8
206 moves: 123	coalesceable: 71	coalesced: 57
207 moves: 4	coalesceable: 4	coalesced: 4
208 moves: 76	coalesceable: 55	coalesced: 52
209 moves: 6	coalesceable: 6	coalesced: 6
210 moves: 104	coalesceable: 73	coalesced: 63
211 moves: 8	coalesceable: 8	coalesced: 8
212 moves: 428	coalesceable: 228	coalesced: 178
213 moves: 4	coalesceable: 4	coalesced: 4
214 moves: 60	coalesceable: 38	coalesced: 35
215 moves: 4	coalesceable: 4	coalesced: 4
216 moves: 8	coalesceable: 6	coalesced: 6
217 moves: 8	coalesceable: 8	coalesced: 8
218 moves: 157	coalesceable: 104	coalesced: 87
219 moves: 6	coalesceable: 6	coalesced: 6
220 moves: 111	coalesceable: 77	coalesced: 69
221 moves: 4	coalesceable: 4	coalesced: 4
222 moves: 5	coalesceable: 5	coalesced: 5
223 moves: 8	coalesceable: 8	coalesced: 8
224 moves: 128	coalesceable: 77	coalesced: 70
225 moves: 8	coalesceable: 8	coalesced: 8
226 moves: 111	coalesceable: 66	coalesced: 51
227 moves: 6	coalesceable: 6	coalesced: 6
228 moves: 46	coalesceable: 34	coalesced: 31
229 moves: 6	coalesceable: 6	coalesced: 6
230 moves: 434	coalesceable: 270	coalesced: 198
231 moves: 4	coalesceable: 4	coalesced: 4
232 moves: 5	coalesceable: 5	coalesced: 5
233 moves: 4	coalesceable: 4	coalesced: 4
234 moves: 40	coalesceable: 26	coalesced: 25

Saved theorem _______ "temp_oracle_cv_eq"
Saved theorem _______ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 28.1s to build
cc cat.S /scratch/cakeml/regression2/cakeml-2544/basis/basis_ffi.o  -o cake_cat
/usr/bin/ld: warning: /tmp/ccut39lP.o: missing .note.GNU-stack section implies executable stack
/usr/bin/ld: NOTE: This behaviour is deprecated and will be removed in a future version of the linker
/usr/bin/ld: /scratch/cakeml/regression2/cakeml-2544/basis/basis_ffi.o: in function `ffidouble_pow':
basis_ffi.c:(.text+0x911): undefined reference to `pow'
/usr/bin/ld: /scratch/cakeml/regression2/cakeml-2544/basis/basis_ffi.o: in function `ffidouble_ln':
basis_ffi.c:(.text+0x959): undefined reference to `log'
/usr/bin/ld: /scratch/cakeml/regression2/cakeml-2544/basis/basis_ffi.o: in function `ffidouble_exp':
basis_ffi.c:(.text+0x9a1): undefined reference to `exp'
/usr/bin/ld: /scratch/cakeml/regression2/cakeml-2544/basis/basis_ffi.o: in function `ffidouble_floor':
basis_ffi.c:(.text+0x9e9): undefined reference to `floor'
collect2: error: ld returned 1 exit status