Job 2652

CakeML:91c65a0dce25352477c78c5b785808249f3e6c44
  fix top-level proofs [Oct 13 14:35:42]
#1068 (preserve)
Merging into:b9843ac59b40ad1a8adc0dfdfcd5e0656f44ab6e
  Merge pull request #1064 from CakeML/remove-define [Oct 10 11:32:18]
HOL:4d1b16443810923d9832780d757d1b868bc9eef4
  cv translator: allow known fun types in ctors [Oct 09 12:54:25]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Oct 13 19:31:23 Claimed job
Oct 13 19:31:25 Reusing HOL
Oct 13 19:32:09 Starting developers
Oct 13 19:32:15 Finished developers                                               6s 155MB
Oct 13 19:32:16 Starting developers/bin
Oct 13 19:32:22 Finished developers/bin                                           5s   1GB
Oct 13 19:32:22 Starting compiler/proofs
Oct 13 21:27:44 Finished compiler/proofs                                    1h55m22s  14GB
Oct 13 21:27:44 Starting compiler/bootstrap/translation
Oct 14 06:25:56 Finished compiler/bootstrap/translation                     8h58m11s  38GB
Oct 14 06:25:56 Starting semantics/ffi
Oct 14 06:26:02 Finished semantics/ffi                                            5s 410MB
Oct 14 06:26:02 Starting semantics
Oct 14 06:26:04 Finished semantics                                                1s  20MB
Oct 14 06:26:04 Starting semantics/proofs
Oct 14 06:26:30 Finished semantics/proofs                                        25s 413MB
Oct 14 06:26:30 Starting semantics/alt_semantics
Oct 14 06:26:53 Finished semantics/alt_semantics                                 22s 524MB
Oct 14 06:26:53 Starting semantics/alt_semantics/proofs
Oct 14 06:38:32 Finished semantics/alt_semantics/proofs                       11m38s   1GB
Oct 14 06:38:32 Starting basis/pure
Oct 14 06:38:33 Finished basis/pure                                               1s  19MB
Oct 14 06:38:34 Starting translator
Oct 14 06:40:15 Finished translator                                            1m41s   1GB
Oct 14 06:40:15 Starting compiler/parsing
Oct 14 06:40:17 Finished compiler/parsing                                         1s  18MB
Oct 14 06:40:17 Starting characteristic
Oct 14 06:40:19 Finished characteristic                                           1s  25MB
Oct 14 06:40:19 Starting translator/monadic
Oct 14 06:40:21 Finished translator/monadic                                       1s  22MB
Oct 14 06:40:21 Starting basis
Oct 14 06:42:54 Finished basis                                                 2m33s   2GB
Oct 14 06:42:54 Starting compiler/inference
Oct 14 06:42:56 Finished compiler/inference                                       1s  24MB
Oct 14 06:42:56 Starting compiler/backend/reg_alloc
Oct 14 06:42:58 Finished compiler/backend/reg_alloc                               1s  20MB
Oct 14 06:42:58 Starting compiler/backend/gc
Oct 14 06:43:00 Finished compiler/backend/gc                                      2s  24MB
Oct 14 06:43:01 Starting compiler/backend
Oct 14 06:43:06 Finished compiler/backend                                         5s 294MB
Oct 14 06:43:06 Starting compiler/encoders/asm
Oct 14 06:43:08 Finished compiler/encoders/asm                                    1s  23MB
Oct 14 06:43:08 Starting compiler/encoders/x64
Oct 14 06:43:10 Finished compiler/encoders/x64                                    1s  25MB
Oct 14 06:43:10 Starting compiler/encoders/arm7
Oct 14 06:43:12 Finished compiler/encoders/arm7                                   1s  23MB
Oct 14 06:43:12 Starting compiler/encoders/arm8
Oct 14 06:43:14 Finished compiler/encoders/arm8                                   1s  27MB
Oct 14 06:43:14 Starting compiler/encoders/arm8_asl
Oct 14 09:13:06 Finished compiler/encoders/arm8_asl                         2h29m51s  31GB
Oct 14 09:13:06 Starting compiler/encoders/mips
Oct 14 09:13:07 Finished compiler/encoders/mips                                   1s  22MB
Oct 14 09:13:08 Starting compiler/encoders/riscv
Oct 14 09:13:09 Finished compiler/encoders/riscv                                  1s  24MB
Oct 14 09:13:10 Starting compiler/encoders/ag32
Oct 14 09:13:11 Finished compiler/encoders/ag32                                   1s  26MB
Oct 14 09:13:12 Starting compiler/backend/x64
Oct 14 09:13:14 Finished compiler/backend/x64                                     2s  29MB
Oct 14 09:13:14 Starting compiler/backend/arm7
Oct 14 09:13:16 Finished compiler/backend/arm7                                    2s  33MB
Oct 14 09:13:16 Starting compiler/backend/arm8
Oct 14 09:13:19 Finished compiler/backend/arm8                                    2s  28MB
Oct 14 09:13:19 Starting compiler/backend/mips
Oct 14 09:13:21 Finished compiler/backend/mips                                    2s  25MB
Oct 14 09:13:21 Starting compiler/backend/riscv
Oct 14 09:13:23 Finished compiler/backend/riscv                                   2s  28MB
Oct 14 09:13:24 Starting compiler/backend/ag32
Oct 14 09:14:35 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 14 09:14:35 Starting compiler/parsing/proofs
Oct 14 09:14:36 Finished compiler/parsing/proofs                                  1s  22MB
Oct 14 09:14:37 Starting compiler/inference/proofs
Oct 14 09:14:38 Finished compiler/inference/proofs                                1s  20MB
Oct 14 09:14:39 Starting compiler/backend/semantics
Oct 14 09:18:09 Finished compiler/backend/semantics                            3m30s   1GB
Oct 14 09:18:09 Starting compiler/backend/reg_alloc/proofs
Oct 14 09:18:11 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Oct 14 09:18:11 Starting compiler/backend/proofs
Oct 14 09:19:04 Finished compiler/backend/proofs                                 52s   2GB
Oct 14 09:19:04 Starting compiler/backend/serialiser
Oct 14 09:19:06 Finished compiler/backend/serialiser                              2s  25MB
Oct 14 09:19:06 Starting compiler/encoders/x64/proofs
Oct 14 09:29:51 Finished compiler/encoders/x64/proofs                         10m44s   4GB
Oct 14 09:29:51 Starting compiler/encoders/arm7/proofs
Oct 14 09:43:40 Finished compiler/encoders/arm7/proofs                        13m48s   5GB
Oct 14 09:43:40 Starting compiler/encoders/arm8/proofs
Oct 14 09:51:13 Finished compiler/encoders/arm8/proofs                         7m32s   1GB
Oct 14 09:51:13 Starting compiler/encoders/arm8_asl/proofs
Oct 14 10:46:58 Finished compiler/encoders/arm8_asl/proofs                    55m44s   5GB
Oct 14 10:46:58 Starting compiler/encoders/mips/proofs
Oct 14 10:57:48 Finished compiler/encoders/mips/proofs                        10m50s   2GB
Oct 14 10:57:48 Starting compiler/encoders/riscv/proofs
Oct 14 11:06:57 Finished compiler/encoders/riscv/proofs                        9m09s   1GB
Oct 14 11:06:57 Starting compiler/encoders/ag32/proofs
Oct 14 11:10:16 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Oct 14 11:10:16 Starting compiler/backend/x64/proofs
Oct 14 11:10:48 Finished compiler/backend/x64/proofs                             32s   2GB
Oct 14 11:10:48 Starting compiler/backend/arm7/proofs
Oct 14 11:11:22 Finished compiler/backend/arm7/proofs                            33s   1GB
Oct 14 11:11:22 Starting compiler/backend/arm8/proofs
Oct 14 11:11:54 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 14 11:11:54 Starting compiler/backend/arm8_asl
Oct 14 11:12:19 Finished compiler/backend/arm8_asl                               24s   1GB
Oct 14 11:12:20 Starting compiler/backend/mips/proofs
Oct 14 11:12:54 Finished compiler/backend/mips/proofs                            34s   2GB
Oct 14 11:12:54 Starting compiler/backend/riscv/proofs
Oct 14 11:13:30 Finished compiler/backend/riscv/proofs                           36s   2GB
Oct 14 11:13:30 Starting compiler/backend/ag32/proofs
Oct 14 11:28:20 Finished compiler/backend/ag32/proofs                         14m49s   5GB
Oct 14 11:28:20 Starting compiler/backend/cv_compute
Oct 14 11:29:39 Finished compiler/backend/cv_compute                           1m18s   2GB
Oct 14 11:29:39 Starting cv_translator
Oct 14 11:50:59 Finished cv_translator                                        21m20s   5GB
Oct 14 11:50:59 Starting candle/set-theory
Oct 14 11:51:36 Finished candle/set-theory                                       36s   1GB
Oct 14 11:51:36 Starting candle/syntax-lib
Oct 14 11:51:38 Finished candle/syntax-lib                                        1s  23MB
Oct 14 11:51:38 Starting candle/standard/syntax
Oct 14 11:51:51 Finished candle/standard/syntax                                  13s 802MB
Oct 14 11:51:51 Starting candle/standard/semantics
Oct 14 11:54:05 Finished candle/standard/semantics                             2m13s   1GB
Oct 14 11:54:05 Starting candle/standard/monadic
Oct 14 11:54:07 Finished candle/standard/monadic                                  1s  21MB
Oct 14 11:54:07 Starting candle/standard/ml_kernel
Oct 14 11:56:01 Finished candle/standard/ml_kernel                             1m54s   3GB
Oct 14 11:56:01 Starting candle/overloading/syntax
Oct 14 11:59:32 Finished candle/overloading/syntax                             3m30s   1GB
Oct 14 11:59:32 Starting candle/overloading/semantics
Oct 14 12:12:07 Finished candle/overloading/semantics                         12m34s   3GB
Oct 14 12:12:07 Starting candle/overloading/monadic
Oct 14 12:14:38 Finished candle/overloading/monadic                            2m31s   1GB
Oct 14 12:14:38 Starting candle/overloading/ml_kernel
Oct 14 12:22:53 Finished candle/overloading/ml_kernel                          8m14s   4GB
Oct 14 12:22:53 Starting candle/overloading/ml_checker
Oct 14 12:25:41 Finished candle/overloading/ml_checker                         2m47s   2GB
Oct 14 12:25:41 Starting candle/prover
Oct 14 12:36:21 Finished candle/prover                                        10m39s   3GB
Oct 14 12:36:21 Starting pancake
Oct 14 12:36:47 Finished pancake                                                 25s 849MB
Oct 14 12:36:47 Starting pancake/ffi
Oct 14 12:36:47 Finished pancake/ffi                                              0s  13MB
Oct 14 12:36:47 Starting pancake/semantics
Oct 14 12:39:11 Finished pancake/semantics                                     2m23s   1GB
Oct 14 12:39:11 Starting pancake/parser
Oct 14 12:39:37 Finished pancake/parser                                          25s 433MB
Oct 14 12:39:37 Starting pancake/proofs
Oct 14 12:58:20 Finished pancake/proofs                                       18m42s   3GB
Oct 14 12:58:20 Starting compiler/dafny
Oct 14 13:00:52 Finished compiler/dafny                                        2m31s  10GB
Oct 14 13:00:52 Starting compiler/dafny/translation
Oct 14 13:30:56 Finished compiler/dafny/translation                           30m04s  16GB
Oct 14 13:30:56 Starting compiler/dafny/compilation
Oct 14 13:34:20 Finished compiler/dafny/compilation                            3m23s  10GB
Oct 14 13:34:20 Starting compiler/dafny/semantics
Oct 14 13:34:57 Finished compiler/dafny/semantics                                37s 824MB
Oct 14 13:34:57 Starting characteristic/examples
Oct 14 13:36:29 Finished characteristic/examples                               1m31s   2GB
Oct 14 13:36:29 Starting tutorial/solutions
Oct 14 13:39:20 Finished tutorial/solutions                                    2m51s   4GB
Oct 14 13:39:20 Starting translator/monadic/examples
Oct 14 13:42:58 Finished translator/monadic/examples                           3m37s   2GB
Oct 14 13:42:58 Starting examples
Oct 14 13:57:47 Finished examples                                             14m48s   2GB
Oct 14 13:57:47 Starting examples/compilation/x64
Oct 14 14:06:52 Finished examples/compilation/x64                              9m04s   6GB
Oct 14 14:06:52 Starting examples/compilation/x64/proofs
Oct 14 14:09:48 Finished examples/compilation/x64/proofs                       2m56s   4GB
Oct 14 14:09:48 Starting examples/compilation/ag32
Oct 14 14:12:04 Finished examples/compilation/ag32                             2m15s   3GB
Oct 14 14:12:04 Starting examples/compilation/ag32/proofs
Oct 14 14:13:19 Finished examples/compilation/ag32/proofs                      1m15s   5GB
Oct 14 14:13:19 Starting examples/compilation/to_word
Oct 14 14:16:48 Finished examples/compilation/to_word                          3m28s   5GB
Oct 14 14:16:48 Starting examples/lpr_checker
Oct 14 14:17:19 Finished examples/lpr_checker                                    30s 559MB
Oct 14 14:17:19 Starting examples/lpr_checker/array
Oct 14 14:45:29 Finished examples/lpr_checker/array                           28m09s   6GB
Oct 14 14:45:29 Starting examples/lpr_checker/array/compilation
Oct 14 14:48:17 Finished examples/lpr_checker/array/compilation                2m48s   7GB
Oct 14 14:48:17 Starting examples/lpr_checker/array/compilation/proofs
Oct 14 14:49:42 Finished examples/lpr_checker/array/compilation/proofs         1m24s   5GB
Oct 14 14:49:42 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 14 14:51:02 Finished examples/lpr_checker/array/compilation/proofsARM8     1m20s   5GB
Oct 14 14:51:02 Starting examples/xlrup_checker
Oct 14 14:51:39 Finished examples/xlrup_checker                                  37s 622MB
Oct 14 14:51:40 Starting examples/xlrup_checker/array
Oct 14 15:06:10 Finished examples/xlrup_checker/array                         14m30s   2GB
Oct 14 15:06:10 Starting examples/xlrup_checker/array/compilation
Oct 14 15:07:36 Finished examples/xlrup_checker/array/compilation              1m25s   4GB
Oct 14 15:07:36 Starting examples/xlrup_checker/array/compilation/proofs
Oct 14 15:08:41 Finished examples/xlrup_checker/array/compilation/proofs       1m05s   4GB
Oct 14 15:08:41 Starting examples/pseudo_bool
Oct 14 15:10:21 Finished examples/pseudo_bool                                  1m39s   1GB
Oct 14 15:10:21 Starting examples/pseudo_bool/cnf_encoding
Oct 14 15:10:51 Finished examples/pseudo_bool/cnf_encoding                       30s 952MB
Oct 14 15:10:51 Starting examples/pseudo_bool/graph_encoding
Oct 14 15:11:38 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Oct 14 15:11:38 Starting examples/pseudo_bool/array
Oct 14 16:23:26 Finished examples/pseudo_bool/array                         1h11m47s   8GB
Oct 14 16:23:26 Starting examples/pseudo_bool/array/compilation
Oct 14 16:39:25 Finished examples/pseudo_bool/array/compilation               15m59s  25GB
Oct 14 16:39:26 Starting examples/pseudo_bool/array/compilation/proofs
Oct 14 16:40:59 FAILED: examples/pseudo_bool/array/compilation/proofs
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/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/algebra/base[0m
Scanning [1m$(HOLDIR)/src/algebra/construction[0m
Scanning [1m$(HOLDIR)/src/algebra[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)/src/num/theories/cv_compute/automation[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$(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation[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)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/cv_compute[0m
Scanning [1m$(CAKEMLDIR)/cv_translator[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array/compilation[0m
Scanned 103 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                                                                                            (75s)     OK
Starting work on npbc_fullProofTheory
mccisProofTheory                                                                                           (81s)     OK
Starting work on subgraph_isoProofTheory
cliqueProofTheory                                                                                          (81s)     OK
Starting work on wcnfProofTheory
cnfProofTheory                                                                                             (81s)FAIL<1>
 <<HOL message: Created theory "cnfProof">>
 Saved theorem _______ "cake_pb_cnf_compiled_thm"
 Saved definition ____ "installed_x64_def"
 Saved definition ____ "cake_pb_cnf_code_def"
 Saved definition ____ "cake_pb_cnf_run_def"
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 103)
 error in quse /home/cug/hk324/cml-regression/cakeml-2652/examples/pseudo_bool/array/compilation/proofs/cnfProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 103)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-2652/examples/pseudo_bool/array/compilation/proofs/cnfProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 103)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 cake_pb_cnf_run cl fs mc ms 
 machine_sem mc (basis_ffi cl fs) ms 
 extend_with_resource_limit {Terminate Success (cake_pb_cnf_io_events cl fs)} 
 out err.
   extract_fs fs (cake_pb_cnf_io_events cl fs) =
   SOME (add_stdout (add_stderr fs err) out) 
   (out   
    inFS_fname fs (EL 1 cl) 
    (LENGTH cl = 2 
     (fml.
        parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml 
        out = concat (print_prob (mk_prob (fml_to_pbf fml)))) 
     LENGTH cl = 3 
     fml.
       parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml 
       (out = UNSAT_string  unsatisfiable (interp fml) 
        out = SAT_string  satisfiable (interp fml))))
 
 failed.
 Failed to prove theorem machine_code_sound.
 Uncaught exception at /home/cug/hk324/cml-regression/HOL-4d1b16443810923d9832780d757d1b868bc9eef4/src/prekernel/Feedback.sml:106: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 103)", origin_function = "THEN1", origin_structure = "Tactical"}
npbc_fullProofTheory                                                                                        (6s)MKILLED
subgraph_isoProofTheory                                                                                     (1s)MKILLED
wcnfProofTheory                                                                                             (0s)MKILLED