Job 2335

CakeML:d369d3393eb79b13e58bd7cc2ae4797ab80a003e
  simplify shmem_extra in installed lemmas [Mar 12 12:14:58]
#977 (share_mem_new2)
Merging into:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:3a51c81db857b7722efa0871ac507883adf6d440
  Remove compilerTheory (put its content at end of codegenTheory) [Mar 11 19:26:17]
Machine:pavlova

Mar 13 03:17:00 Claimed job
Mar 13 03:17:03 Reusing HOL
Mar 13 03:17:13 Starting developers
Mar 13 03:17:17 Finished developers                                               2s 206MB
Mar 13 03:17:18 Starting developers/bin
Mar 13 03:18:19 Finished developers/bin                                          59s   1GB
Mar 13 03:18:20 Starting compiler/proofs
Mar 13 05:06:15 Finished compiler/proofs                                    1h47m54s  36GB
Mar 13 05:06:16 Starting compiler/bootstrap/translation
Mar 13 13:07:42 Finished compiler/bootstrap/translation                     8h01m24s  88GB
Mar 13 13:07:43 Starting semantics/ffi
Mar 13 13:07:51 Finished semantics/ffi                                            7s 674MB
Mar 13 13:07:52 Starting semantics
Mar 13 13:07:53 Finished semantics                                                0s  66MB
Mar 13 13:07:54 Starting semantics/proofs
Mar 13 13:08:29 Finished semantics/proofs                                        33s   1GB
Mar 13 13:08:30 Starting semantics/alt_semantics
Mar 13 13:09:08 Finished semantics/alt_semantics                                 37s   1GB
Mar 13 13:09:09 Starting semantics/alt_semantics/proofs
Mar 13 13:20:00 Finished semantics/alt_semantics/proofs                       10m49s   4GB
Mar 13 13:20:00 Starting basis/pure
Mar 13 13:20:02 Finished basis/pure                                               0s  69MB
Mar 13 13:20:03 Starting translator
Mar 13 13:21:43 Finished translator                                            1m39s   2GB
Mar 13 13:21:44 Starting compiler/parsing
Mar 13 13:21:46 Finished compiler/parsing                                         0s  67MB
Mar 13 13:21:46 Starting characteristic
Mar 13 13:21:48 Finished characteristic                                           0s  88MB
Mar 13 13:21:49 Starting translator/monadic
Mar 13 13:21:50 Finished translator/monadic                                       0s  91MB
Mar 13 13:21:51 Starting basis
Mar 13 13:25:26 Finished basis                                                 3m33s   5GB
Mar 13 13:25:26 Starting compiler/inference
Mar 13 13:25:28 Finished compiler/inference                                       0s  80MB
Mar 13 13:25:29 Starting compiler/backend/reg_alloc
Mar 13 13:25:30 Finished compiler/backend/reg_alloc                               0s  67MB
Mar 13 13:25:31 Starting compiler/backend/gc
Mar 13 13:25:33 Finished compiler/backend/gc                                      0s 134MB
Mar 13 13:25:34 Starting compiler/backend
Mar 13 13:25:52 Finished compiler/backend                                        16s   1GB
Mar 13 13:25:52 Starting compiler/encoders/asm
Mar 13 13:25:54 Finished compiler/encoders/asm                                    0s  92MB
Mar 13 13:25:55 Starting compiler/encoders/x64
Mar 13 13:25:56 Finished compiler/encoders/x64                                    0s  94MB
Mar 13 13:25:57 Starting compiler/encoders/arm7
Mar 13 13:25:59 Finished compiler/encoders/arm7                                   0s  93MB
Mar 13 13:26:00 Starting compiler/encoders/arm8
Mar 13 13:26:01 Finished compiler/encoders/arm8                                   0s  94MB
Mar 13 13:26:02 Starting compiler/encoders/arm8_asl
Mar 13 13:28:19 Finished compiler/encoders/arm8_asl                            2m16s   1GB
Mar 13 13:28:20 Starting compiler/encoders/mips
Mar 13 13:28:22 Finished compiler/encoders/mips                                   0s  93MB
Mar 13 13:28:22 Starting compiler/encoders/riscv
Mar 13 13:28:24 Finished compiler/encoders/riscv                                  0s  94MB
Mar 13 13:28:25 Starting compiler/encoders/ag32
Mar 13 13:28:26 Finished compiler/encoders/ag32                                   0s  92MB
Mar 13 13:28:27 Starting compiler/backend/x64
Mar 13 13:28:29 Finished compiler/backend/x64                                     0s 130MB
Mar 13 13:28:30 Starting compiler/backend/arm7
Mar 13 13:28:32 Finished compiler/backend/arm7                                    0s 126MB
Mar 13 13:28:33 Starting compiler/backend/arm8
Mar 13 13:28:34 Finished compiler/backend/arm8                                    0s 125MB
Mar 13 13:28:35 Starting compiler/backend/mips
Mar 13 13:28:37 Finished compiler/backend/mips                                    0s 125MB
Mar 13 13:28:38 Starting compiler/backend/riscv
Mar 13 13:28:40 Finished compiler/backend/riscv                                   0s 126MB
Mar 13 13:28:41 Starting compiler/backend/ag32
Mar 13 13:30:00 Finished compiler/backend/ag32                                 1m18s   2GB
Mar 13 13:30:00 Starting compiler/parsing/proofs
Mar 13 13:30:02 Finished compiler/parsing/proofs                                  0s  78MB
Mar 13 13:30:03 Starting compiler/inference/proofs
Mar 13 13:30:04 Finished compiler/inference/proofs                                0s  90MB
Mar 13 13:30:05 Starting compiler/backend/semantics
Mar 13 13:33:45 Finished compiler/backend/semantics                            3m38s   2GB
Mar 13 13:33:46 Starting compiler/backend/reg_alloc/proofs
Mar 13 13:33:47 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Mar 13 13:33:48 Starting compiler/backend/proofs
Mar 13 13:34:53 Finished compiler/backend/proofs                               1m03s   3GB
Mar 13 13:34:54 Starting compiler/backend/serialiser
Mar 13 13:34:56 Finished compiler/backend/serialiser                              1s 193MB
Mar 13 13:34:57 Starting compiler/encoders/x64/proofs
Mar 13 13:44:25 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Mar 13 13:44:26 Starting compiler/encoders/arm7/proofs
Mar 13 13:57:10 Finished compiler/encoders/arm7/proofs                        12m42s  10GB
Mar 13 13:57:11 Starting compiler/encoders/arm8/proofs
Mar 13 14:03:30 Finished compiler/encoders/arm8/proofs                         6m18s   5GB
Mar 13 14:03:31 Starting compiler/encoders/arm8_asl/proofs
Mar 13 14:17:17 Finished compiler/encoders/arm8_asl/proofs                    13m44s   5GB
Mar 13 14:17:18 Starting compiler/encoders/mips/proofs
Mar 13 14:27:23 Finished compiler/encoders/mips/proofs                        10m04s  11GB
Mar 13 14:27:23 Starting compiler/encoders/riscv/proofs
Mar 13 14:35:39 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Mar 13 14:35:40 Starting compiler/encoders/ag32/proofs
Mar 13 14:38:01 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 13 14:38:02 Starting compiler/backend/x64/proofs
Mar 13 14:38:43 Finished compiler/backend/x64/proofs                             40s   3GB
Mar 13 14:38:44 Starting compiler/backend/arm7/proofs
Mar 13 14:39:28 Finished compiler/backend/arm7/proofs                            42s   2GB
Mar 13 14:39:29 Starting compiler/backend/arm8/proofs
Mar 13 14:40:08 Finished compiler/backend/arm8/proofs                            38s   2GB
Mar 13 14:40:09 Starting compiler/backend/arm8_asl
Mar 13 14:40:39 Finished compiler/backend/arm8_asl                               29s   2GB
Mar 13 14:40:40 Starting compiler/backend/mips/proofs
Mar 13 14:41:25 Finished compiler/backend/mips/proofs                            43s   3GB
Mar 13 14:41:26 Starting compiler/backend/riscv/proofs
Mar 13 14:42:15 Finished compiler/backend/riscv/proofs                           48s   4GB
Mar 13 14:42:16 Starting compiler/backend/ag32/proofs
Mar 13 14:56:03 Finished compiler/backend/ag32/proofs                         13m45s   6GB
Mar 13 14:56:04 Starting candle/set-theory
Mar 13 14:56:48 Finished candle/set-theory                                       43s   1GB
Mar 13 14:56:49 Starting candle/syntax-lib
Mar 13 14:56:50 Finished candle/syntax-lib                                        0s  73MB
Mar 13 14:56:51 Starting candle/standard/syntax
Mar 13 14:57:08 Finished candle/standard/syntax                                  15s   1GB
Mar 13 14:57:09 Starting candle/standard/semantics
Mar 13 14:59:35 Finished candle/standard/semantics                             2m25s   3GB
Mar 13 14:59:36 Starting candle/standard/monadic
Mar 13 14:59:37 Finished candle/standard/monadic                                  0s  96MB
Mar 13 14:59:38 Starting candle/standard/ml_kernel
Mar 13 15:01:27 Finished candle/standard/ml_kernel                             1m48s   6GB
Mar 13 15:01:28 Starting candle/overloading/syntax
Mar 13 15:04:51 Finished candle/overloading/syntax                             3m21s   3GB
Mar 13 15:04:52 Starting candle/overloading/semantics
Mar 13 15:16:10 Finished candle/overloading/semantics                         11m17s   7GB
Mar 13 15:16:11 Starting candle/overloading/monadic
Mar 13 15:18:44 Finished candle/overloading/monadic                            2m31s   3GB
Mar 13 15:18:45 Starting candle/overloading/ml_kernel
Mar 13 15:26:15 Finished candle/overloading/ml_kernel                          7m29s   6GB
Mar 13 15:26:16 Starting candle/overloading/ml_checker
Mar 13 15:28:48 Finished candle/overloading/ml_checker                         2m31s   6GB
Mar 13 15:28:49 Starting candle/prover
Mar 13 15:38:38 Finished candle/prover                                         9m48s   5GB
Mar 13 15:38:39 Starting pancake
Mar 13 15:39:40 Finished pancake                                               1m00s   1GB
Mar 13 15:39:41 Starting pancake/ffi
Mar 13 15:39:42 Finished pancake/ffi                                              0s  20MB
Mar 13 15:39:43 Starting pancake/semantics
Mar 13 15:42:20 Finished pancake/semantics                                     2m36s   2GB
Mar 13 15:42:21 Starting pancake/parser
Mar 13 15:42:48 Finished pancake/parser                                          25s   2GB
Mar 13 15:42:49 Starting pancake/proofs
Mar 13 16:13:44 Finished pancake/proofs                                       30m54s   8GB
Mar 13 16:13:45 Starting characteristic/examples
Mar 13 16:15:21 Finished characteristic/examples                               1m34s   6GB
Mar 13 16:15:22 Starting tutorial/solutions
Mar 13 16:31:08 Finished tutorial/solutions                                   15m45s  10GB
Mar 13 16:31:09 Starting translator/monadic/examples
Mar 13 16:34:56 Finished translator/monadic/examples                           3m46s   5GB
Mar 13 16:34:57 Starting examples
Mar 13 16:49:09 Finished examples                                             14m10s   7GB
Mar 13 16:49:10 Starting examples/compilation/x64
Mar 13 18:48:13 Finished examples/compilation/x64                           1h59m02s  36GB
Mar 13 18:48:14 Starting examples/compilation/x64/proofs
Mar 13 18:52:11 Finished examples/compilation/x64/proofs                       3m55s   6GB
Mar 13 18:52:12 Starting examples/compilation/ag32
Mar 13 19:21:41 Finished examples/compilation/ag32                            29m27s  10GB
Mar 13 19:21:42 Starting examples/compilation/ag32/proofs
Mar 13 19:23:08 Finished examples/compilation/ag32/proofs                      1m26s   7GB
Mar 13 19:23:09 Starting examples/compilation/to_word
Mar 13 19:27:06 Finished examples/compilation/to_word                          3m56s  13GB
Mar 13 19:27:07 Starting examples/lpr_checker
Mar 13 19:28:24 Finished examples/lpr_checker                                  1m15s   2GB
Mar 13 19:28:25 Starting examples/lpr_checker/array
Mar 13 19:58:41 Finished examples/lpr_checker/array                           30m15s   8GB
Mar 13 19:58:42 Starting examples/lpr_checker/array/compilation
Mar 13 20:39:58 Finished examples/lpr_checker/array/compilation               41m15s  93GB
Mar 13 20:39:59 Starting examples/lpr_checker/array/compilation/proofs
Mar 13 20:41:38 Finished examples/lpr_checker/array/compilation/proofs         1m38s   8GB
Mar 13 20:41:39 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 13 20:53:24 Finished examples/lpr_checker/array/compilation/proofsARM8    11m44s  47GB
Mar 13 20:53:25 Starting examples/xlrup_checker
Mar 13 20:54:35 Finished examples/xlrup_checker                                1m09s   1GB
Mar 13 20:54:36 Starting examples/xlrup_checker/array
Mar 13 21:10:48 Finished examples/xlrup_checker/array                         16m10s   6GB
Mar 13 21:10:48 Starting examples/xlrup_checker/array/compilation
Mar 13 21:32:51 Finished examples/xlrup_checker/array/compilation             22m01s  42GB
Mar 13 21:32:52 Starting examples/xlrup_checker/array/compilation/proofs
Mar 13 21:34:17 Finished examples/xlrup_checker/array/compilation/proofs       1m24s   7GB
Mar 13 21:34:18 Starting examples/pseudo_bool
Mar 13 21:36:18 Finished examples/pseudo_bool                                  1m59s   1GB
Mar 13 21:36:19 Starting examples/pseudo_bool/cnf_encoding
Mar 13 21:36:56 Finished examples/pseudo_bool/cnf_encoding                       36s   1GB
Mar 13 21:36:57 Starting examples/pseudo_bool/graph_encoding
Mar 13 21:37:45 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Mar 13 21:37:46 Starting examples/pseudo_bool/array
Mar 13 22:42:15 Finished examples/pseudo_bool/array                         1h04m28s  25GB
Mar 13 22:42:16 Starting examples/pseudo_bool/array/compilation
Mar 14 06:14:36 Finished examples/pseudo_bool/array/compilation             7h32m18s 145GB
Mar 14 06:14:37 Starting examples/pseudo_bool/array/compilation/proofs
Mar 14 06:17:47 FAILED: examples/pseudo_bool/array/compilation/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[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/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(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)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[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/rational[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/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/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/cnf_encoding[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/graph_encoding[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array/compilation[0m
Scanned 94 directories
Starting work on README.md
Starting work on cliqueProofTheory
Starting work on cnfProofTheory
Starting work on mccisProofTheory
README.md                                                           (0s)     OK
Starting work on mcisProofTheory
mcisProofTheory                                                    (82s)     OK
Starting work on npbc_fullProofTheory
cnfProofTheory                                                     (83s)     OK
Starting work on subgraph_isoProofTheory
cliqueProofTheory                                                  (84s)     OK
Starting work on wcnfProofTheory
mccisProofTheory                                                   (86s)     OK
npbc_fullProofTheory                                               (84s)     OK
wcnfProofTheory                                                    (82s)FAIL<1>
 <<HOL message: Created theory "wcnfProof">>
 Saved theorem _______ "cake_pb_wcnf_compiled_thm"
 error in quse /scratch/cakeml/regression/cakeml-2335/examples/pseudo_bool/array/compilation/proofs/wcnfProofScript.sml : HOL_ERR {message = "between line 46, character 6 and line 50, character 64:\n\nType inference failure: unable to infer a type for the application of\n\n$/\\\n  (is_x64_machine_config\n     (mc :(64, x64_state,\n           word64 #\n           (Zreg -> word64) #\n           (word3 -> word128) #\n           (word64 # word8 -> bool) #\n           (Zeflags -> bool option) # MXCSR # x64$exception) machine_config))\n\nbetween line 45, character 6 and line 50, character 64\n\nwhich has type\n\n:bool -> bool\n\nto\n\ninstalled (code :word8 list) (cbspace :num) (data :word64 list)\n  (data_sp :num) (cfg :64 config).lab_conf.ffi_names\n  (heap_regs x64_backend_config.stack_conf.reg_names)\n  (mc :(64, x64_state,\n        word64 #\n        (Zreg -> word64) #\n        (word3 -> word128) #\n        (word64 # word8 -> bool) #\n        (Zeflags -> bool option) # MXCSR # x64$exception) machine_config)\n  (ms :64 shmem_rec list)\n\nbetween line 46, character 6 and line 50, character 64\n\nwhich has type\n\n:x64_state -> bool\n\nunification failure message: Attempt to unify different type operators: min$bool and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /scratch/cakeml/regression/cakeml-2335/examples/pseudo_bool/array/compilation/proofs/wcnfProofScript : HOL_ERR {message = "between line 46, character 6 and line 50, character 64:\n\nType inference failure: unable to infer a type for the application of\n\n$/\\\n  (is_x64_machine_config\n     (mc :(64, x64_state,\n           word64 #\n           (Zreg -> word64) #\n           (word3 -> word128) #\n           (word64 # word8 -> bool) #\n           (Zeflags -> bool option) # MXCSR # x64$exception) machine_config))\n\nbetween line 45, character 6 and line 50, character 64\n\nwhich has type\n\n:bool -> bool\n\nto\n\ninstalled (code :word8 list) (cbspace :num) (data :word64 list)\n  (data_sp :num) (cfg :64 config).lab_conf.ffi_names\n  (heap_regs x64_backend_config.stack_conf.reg_names)\n  (mc :(64, x64_state,\n        word64 #\n        (Zreg -> word64) #\n        (word3 -> word128) #\n        (word64 # word8 -> bool) #\n        (Zeflags -> bool option) # MXCSR # x64$exception) machine_config)\n  (ms :64 shmem_rec list)\n\nbetween line 46, character 6 and line 50, character 64\n\nwhich has type\n\n:x64_state -> bool\n\nunification failure message: Attempt to unify different type operators: min$bool and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "between line 46, character 6 and line 50, character 64:\n\nType inference failure: unable to infer a type for the application of\n\n$/\\\n  (is_x64_machine_config\n     (mc :(64, x64_state,\n           word64 #\n           (Zreg -> word64) #\n           (word3 -> word128) #\n           (word64 # word8 -> bool) #\n           (Zeflags -> bool option) # MXCSR # x64$exception) machine_config))\n\nbetween line 45, character 6 and line 50, character 64\n\nwhich has type\n\n:bool -> bool\n\nto\n\ninstalled (code :word8 list) (cbspace :num) (data :word64 list)\n  (data_sp :num) (cfg :64 config).lab_conf.ffi_names\n  (heap_regs x64_backend_config.stack_conf.reg_names)\n  (mc :(64, x64_state,\n        word64 #\n        (Zreg -> word64) #\n        (word3 -> word128) #\n        (word64 # word8 -> bool) #\n        (Zeflags -> bool option) # MXCSR # x64$exception) machine_config)\n  (ms :64 shmem_rec list)\n\nbetween line 46, character 6 and line 50, character 64\n\nwhich has type\n\n:x64_state -> bool\n\nunification failure message: Attempt to unify different type operators: min$bool and min$fun\n", origin_function = "type-analysis", origin_structure = "Preterm"}
subgraph_isoProofTheory                                            (84s)MKILLED