Job 3454

CakeML:fc2757ca9983a47fd47dcbe5ef265be828801ca8
  Restrict backward reification to a single literal, and extend the par [Aug 14 09:59:03]
#1457 (pb-parse)
Merging into:65b66a712338f80db2b1e3e31f0c337d81ad32b5
  Simplify the bvi_inline proofs [Aug 14 12:44:07]
HOL:fac52534ceb43806d35b11f91dafd558266bcbb6
  Remove yet one more same_const instance in Compute.sml [Aug 02 03:13:23]
Machine:timtam

Aug 15 05:32:20 Claimed job
Aug 15 05:32:24 Reusing HOL
Aug 15 05:32:32 Starting developers
Aug 15 05:32:38 Finished developers                                               4s 241MB
Aug 15 05:32:39 Starting developers/bin
Aug 15 05:32:43 Finished developers/bin                                           2s  92MB
Aug 15 05:32:43 Starting misc
Aug 15 05:33:30 Finished misc                                                    45s   1GB
Aug 15 05:33:30 Starting compiler/proofs
Aug 15 06:45:59 Finished compiler/proofs                                    1h12m27s  15GB
Aug 15 06:46:00 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 15 13:05:07 Finished compiler/bootstrap/compilation/x64/64/proofs       6h19m05s  74GB
Aug 15 13:05:08 Starting semantics/ffi
Aug 15 13:05:20 Finished semantics/ffi                                           11s 538MB
Aug 15 13:05:21 Starting semantics
Aug 15 13:05:22 Finished semantics                                                0s  90MB
Aug 15 13:05:23 Starting semantics/proofs
Aug 15 13:05:48 Finished semantics/proofs                                        24s 691MB
Aug 15 13:05:49 Starting semantics/alt_semantics
Aug 15 13:06:07 Finished semantics/alt_semantics                                 16s 500MB
Aug 15 13:06:08 Starting semantics/alt_semantics/proofs
Aug 15 13:10:00 Finished semantics/alt_semantics/proofs                        3m50s   1GB
Aug 15 13:10:00 Starting basis/pure
Aug 15 13:10:02 Finished basis/pure                                               0s  86MB
Aug 15 13:10:03 Starting translator
Aug 15 13:11:17 Finished translator                                            1m13s   3GB
Aug 15 13:11:18 Starting compiler/parsing
Aug 15 13:12:04 Finished compiler/parsing                                        45s   2GB
Aug 15 13:12:05 Starting characteristic
Aug 15 13:12:07 Finished characteristic                                           1s 118MB
Aug 15 13:12:08 Starting translator/monadic
Aug 15 13:12:10 Finished translator/monadic                                       0s 114MB
Aug 15 13:12:11 Starting translator/monadic/monad_base
Aug 15 13:12:12 Finished translator/monadic/monad_base                            0s  89MB
Aug 15 13:12:13 Starting profiler
Aug 15 13:12:45 Finished profiler                                                31s   1GB
Aug 15 13:12:46 Starting basis
Aug 15 13:14:39 Finished basis                                                 1m52s   4GB
Aug 15 13:14:40 Starting compiler
Aug 15 13:14:42 Finished compiler                                                 1s 227MB
Aug 15 13:14:43 Starting compiler/inference
Aug 15 13:14:45 Finished compiler/inference                                       0s 115MB
Aug 15 13:14:46 Starting compiler/backend/reg_alloc
Aug 15 13:14:48 Finished compiler/backend/reg_alloc                               0s  93MB
Aug 15 13:14:48 Starting compiler/backend/gc
Aug 15 13:14:50 Finished compiler/backend/gc                                      1s 132MB
Aug 15 13:14:51 Starting compiler/backend
Aug 15 13:14:53 Finished compiler/backend                                         1s 136MB
Aug 15 13:14:54 Starting compiler/encoders/asm
Aug 15 13:14:56 Finished compiler/encoders/asm                                    0s  99MB
Aug 15 13:14:57 Starting compiler/encoders/x64
Aug 15 13:14:58 Finished compiler/encoders/x64                                    0s 106MB
Aug 15 13:14:59 Starting compiler/encoders/arm7
Aug 15 13:15:01 Finished compiler/encoders/arm7                                   0s 103MB
Aug 15 13:15:02 Starting compiler/encoders/arm8
Aug 15 13:15:03 Finished compiler/encoders/arm8                                   0s 103MB
Aug 15 13:15:04 Starting compiler/encoders/arm8_asl
Aug 15 13:15:27 Finished compiler/encoders/arm8_asl                              21s   1GB
Aug 15 13:15:28 Starting compiler/encoders/mips
Aug 15 13:15:29 Finished compiler/encoders/mips                                   0s 104MB
Aug 15 13:15:30 Starting compiler/encoders/riscv
Aug 15 13:15:32 Finished compiler/encoders/riscv                                  0s 108MB
Aug 15 13:15:33 Starting compiler/encoders/ag32
Aug 15 13:15:34 Finished compiler/encoders/ag32                                   0s 100MB
Aug 15 13:15:35 Starting compiler/encoders/tests
Aug 15 13:15:37 Finished compiler/encoders/tests                                  1s 126MB
Aug 15 13:15:38 Starting compiler/encoders/monadic_enc
Aug 15 13:16:01 Finished compiler/encoders/monadic_enc                           22s   1GB
Aug 15 13:16:02 Starting compiler/backend/x64
Aug 15 13:16:04 Finished compiler/backend/x64                                     1s 138MB
Aug 15 13:16:04 Starting compiler/backend/arm7
Aug 15 13:16:06 Finished compiler/backend/arm7                                    1s 145MB
Aug 15 13:16:07 Starting compiler/backend/arm8
Aug 15 13:16:09 Finished compiler/backend/arm8                                    1s 139MB
Aug 15 13:16:10 Starting compiler/backend/mips
Aug 15 13:16:12 Finished compiler/backend/mips                                    1s 139MB
Aug 15 13:16:13 Starting compiler/backend/riscv
Aug 15 13:16:15 Finished compiler/backend/riscv                                   1s 148MB
Aug 15 13:16:16 Starting compiler/backend/ag32
Aug 15 13:17:20 Finished compiler/backend/ag32                                 1m03s   2GB
Aug 15 13:17:21 Starting compiler/backend/pattern_matching
Aug 15 13:17:38 Finished compiler/backend/pattern_matching                       16s 882MB
Aug 15 13:17:39 Starting compiler/parsing/ocaml
Aug 15 13:19:48 Finished compiler/parsing/ocaml                                2m07s   1GB
Aug 15 13:19:48 Starting compiler/printing
Aug 15 13:20:43 Finished compiler/printing                                       54s   1GB
Aug 15 13:20:44 Starting compiler/parsing/proofs
Aug 15 13:20:46 Finished compiler/parsing/proofs                                  0s  98MB
Aug 15 13:20:47 Starting compiler/inference/proofs
Aug 15 13:20:49 Finished compiler/inference/proofs                                0s 116MB
Aug 15 13:20:49 Starting compiler/backend/semantics
Aug 15 13:23:56 Finished compiler/backend/semantics                            3m05s   3GB
Aug 15 13:23:56 Starting compiler/backend/reg_alloc/proofs
Aug 15 13:23:58 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Aug 15 13:23:59 Starting compiler/backend/proofs
Aug 15 13:24:45 Finished compiler/backend/proofs                                 45s   1GB
Aug 15 13:24:46 Starting compiler/backend/serialiser
Aug 15 13:24:48 Finished compiler/backend/serialiser                              1s 155MB
Aug 15 13:24:49 Starting compiler/encoders/x64/proofs
Aug 15 13:24:50 Finished compiler/encoders/x64/proofs                             0s 110MB
Aug 15 13:24:51 Starting compiler/encoders/arm7/proofs
Aug 15 13:37:19 Finished compiler/encoders/arm7/proofs                        12m26s   4GB
Aug 15 13:37:20 Starting compiler/encoders/arm8/proofs
Aug 15 13:45:16 Finished compiler/encoders/arm8/proofs                         7m55s   3GB
Aug 15 13:45:17 Starting compiler/encoders/arm8_asl/proofs
Aug 15 14:02:55 Finished compiler/encoders/arm8_asl/proofs                    17m36s   3GB
Aug 15 14:02:55 Starting compiler/encoders/mips/proofs
Aug 15 14:13:54 Finished compiler/encoders/mips/proofs                        10m57s   5GB
Aug 15 14:13:55 Starting compiler/encoders/riscv/proofs
Aug 15 14:23:26 Finished compiler/encoders/riscv/proofs                        9m30s   3GB
Aug 15 14:23:27 Starting compiler/encoders/ag32/proofs
Aug 15 14:26:32 Finished compiler/encoders/ag32/proofs                         3m04s   1GB
Aug 15 14:26:33 Starting compiler/backend/x64/proofs
Aug 15 14:26:35 Finished compiler/backend/x64/proofs                              1s 220MB
Aug 15 14:26:36 Starting compiler/backend/arm7/proofs
Aug 15 14:27:17 Finished compiler/backend/arm7/proofs                            39s   2GB
Aug 15 14:27:18 Starting compiler/backend/arm8/proofs
Aug 15 14:27:56 Finished compiler/backend/arm8/proofs                            37s   2GB
Aug 15 14:27:57 Starting compiler/backend/arm8_asl
Aug 15 14:28:33 Finished compiler/backend/arm8_asl                               35s   2GB
Aug 15 14:28:34 Starting compiler/backend/mips/proofs
Aug 15 14:29:14 Finished compiler/backend/mips/proofs                            39s   2GB
Aug 15 14:29:15 Starting compiler/backend/riscv/proofs
Aug 15 14:29:59 Finished compiler/backend/riscv/proofs                           43s   2GB
Aug 15 14:30:00 Starting compiler/backend/ag32/proofs
Aug 15 14:39:43 Finished compiler/backend/ag32/proofs                          9m42s   5GB
Aug 15 14:39:44 Starting compiler/backend/cv_compute
Aug 15 14:40:16 Finished compiler/backend/cv_compute                             31s   1GB
Aug 15 14:40:17 Starting cv_translator
Aug 15 14:45:39 Finished cv_translator                                         5m21s   4GB
Aug 15 14:45:40 Starting candle
Aug 15 14:45:41 Finished candle                                                   0s   7MB
Aug 15 14:45:42 Starting candle/set-theory
Aug 15 14:45:59 Finished candle/set-theory                                       16s 901MB
Aug 15 14:46:00 Starting candle/syntax-lib
Aug 15 14:46:01 Finished candle/syntax-lib                                        0s  79MB
Aug 15 14:46:02 Starting candle/standard
Aug 15 14:46:03 Finished candle/standard                                          0s   7MB
Aug 15 14:46:04 Starting candle/standard/syntax
Aug 15 14:46:20 Finished candle/standard/syntax                                  14s 806MB
Aug 15 14:46:20 Starting candle/standard/syntax/little_theories
Aug 15 14:47:33 Finished candle/standard/syntax/little_theories                1m11s 861MB
Aug 15 14:47:34 Starting candle/standard/semantics
Aug 15 14:47:36 Finished candle/standard/semantics                                0s  96MB
Aug 15 14:47:36 Starting candle/standard/monadic
Aug 15 14:47:38 Finished candle/standard/monadic                                  0s 121MB
Aug 15 14:47:39 Starting candle/standard/ml_kernel
Aug 15 14:49:52 Finished candle/standard/ml_kernel                             2m12s   4GB
Aug 15 14:49:53 Starting candle/overloading
Aug 15 14:49:54 Finished candle/overloading                                       0s   7MB
Aug 15 14:49:55 Starting candle/overloading/syntax
Aug 15 14:53:09 Finished candle/overloading/syntax                             3m13s   2GB
Aug 15 14:53:10 Starting candle/overloading/semantics
Aug 15 15:02:57 Finished candle/overloading/semantics                          9m46s   7GB
Aug 15 15:02:58 Starting candle/overloading/monadic
Aug 15 15:05:00 Finished candle/overloading/monadic                            2m01s   2GB
Aug 15 15:05:01 Starting candle/overloading/ml_kernel
Aug 15 15:12:14 Finished candle/overloading/ml_kernel                          7m11s   6GB
Aug 15 15:12:15 Starting candle/overloading/ml_checker
Aug 15 15:15:02 Finished candle/overloading/ml_checker                         2m46s   6GB
Aug 15 15:15:03 Starting candle/prover
Aug 15 15:15:06 Finished candle/prover                                            1s 179MB
Aug 15 15:15:06 Starting candle/prover/compute
Aug 15 15:15:08 Finished candle/prover/compute                                    1s 165MB
Aug 15 15:15:09 Starting pancake
Aug 15 15:15:11 Finished pancake                                                  1s 144MB
Aug 15 15:15:12 Starting pancake/semantics
Aug 15 15:18:08 Finished pancake/semantics                                     2m54s   1GB
Aug 15 15:18:09 Starting pancake/parser
Aug 15 15:18:49 Finished pancake/parser                                          39s 500MB
Aug 15 15:18:50 Starting pancake/static_checker
Aug 15 15:21:24 Finished pancake/static_checker                                2m33s   1GB
Aug 15 15:21:25 Starting pancake/proofs
Aug 15 15:38:44 Finished pancake/proofs                                       17m17s   5GB
Aug 15 15:38:45 Starting compiler/dafny
Aug 15 15:39:10 Finished compiler/dafny                                          24s 657MB
Aug 15 15:39:11 Starting compiler/dafny/translation
Aug 15 15:49:57 Finished compiler/dafny/translation                           10m45s   6GB
Aug 15 15:49:58 Starting compiler/dafny/compilation
Aug 15 15:52:09 Finished compiler/dafny/compilation                            2m10s   6GB
Aug 15 15:52:10 Starting compiler/dafny/semantics
Aug 15 15:52:50 Finished compiler/dafny/semantics                                38s 504MB
Aug 15 15:52:50 Starting compiler/dafny/proofs
Aug 15 15:54:29 Finished compiler/dafny/proofs                                 1m37s   1GB
Aug 15 15:54:30 Starting compiler/dafny/vcg
Aug 15 15:54:32 Finished compiler/dafny/vcg                                       0s 104MB
Aug 15 15:54:32 Starting compiler/dafny/vcg/examples
Aug 15 15:55:01 Finished compiler/dafny/vcg/examples                             27s   1GB
Aug 15 15:55:02 Starting compiler/scheme
Aug 15 15:55:29 Finished compiler/scheme                                         26s   1GB
Aug 15 15:55:30 Starting compiler/scheme/translation
Aug 15 16:02:11 Finished compiler/scheme/translation                           6m39s   7GB
Aug 15 16:02:12 Starting compiler/scheme/compilation
Aug 15 16:03:46 Finished compiler/scheme/compilation                           1m33s   3GB
Aug 15 16:03:47 Starting compiler/scheme/proofs
Aug 15 16:10:30 Finished compiler/scheme/proofs                                6m42s   2GB
Aug 15 16:10:31 Starting characteristic/examples
Aug 15 16:12:05 Finished characteristic/examples                               1m33s   5GB
Aug 15 16:12:06 Starting tutorial/solutions
Aug 15 16:14:59 Finished tutorial/solutions                                    2m51s   5GB
Aug 15 16:15:00 Starting translator/monadic/examples
Aug 15 16:18:09 Finished translator/monadic/examples                           3m08s   3GB
Aug 15 16:18:10 Starting examples
Aug 15 16:22:22 Finished examples                                              4m11s   3GB
Aug 15 16:22:23 Starting examples/compilation
Aug 15 16:22:24 Finished examples/compilation                                     0s   7MB
Aug 15 16:22:25 Starting examples/compilation/x64
Aug 15 16:31:30 Finished examples/compilation/x64                              9m04s   4GB
Aug 15 16:31:31 Starting examples/compilation/x64/proofs
Aug 15 16:35:18 Finished examples/compilation/x64/proofs                       3m46s   4GB
Aug 15 16:35:19 Starting examples/compilation/ag32
Aug 15 16:38:05 Finished examples/compilation/ag32                             2m44s   3GB
Aug 15 16:38:06 Starting examples/compilation/ag32/proofs
Aug 15 16:39:29 Finished examples/compilation/ag32/proofs                      1m22s   4GB
Aug 15 16:39:30 Starting examples/lpr_checker
Aug 15 16:40:08 Finished examples/lpr_checker                                    36s   1GB
Aug 15 16:40:08 Starting examples/lpr_checker/array
Aug 15 16:52:58 Finished examples/lpr_checker/array                           12m48s   6GB
Aug 15 16:52:59 Starting examples/lpr_checker/array/compilation
Aug 15 16:56:46 Finished examples/lpr_checker/array/compilation                3m46s   6GB
Aug 15 16:56:47 Starting examples/lpr_checker/array/compilation/proofs
Aug 15 16:58:29 Finished examples/lpr_checker/array/compilation/proofs         1m40s   6GB
Aug 15 16:58:29 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 15 17:00:15 Finished examples/lpr_checker/array/compilation/proofsARM8     1m44s   6GB
Aug 15 17:00:15 Starting .
Aug 15 17:00:19 Finished .                                                        2s 358MB
Aug 15 17:00:20 Starting examples/xlrup_checker
Aug 15 17:01:13 Finished examples/xlrup_checker                                  52s   1GB
Aug 15 17:01:14 Starting examples/xlrup_checker/array
Aug 15 17:10:38 Finished examples/xlrup_checker/array                          9m23s   5GB
Aug 15 17:10:39 Starting examples/xlrup_checker/array/compilation
Aug 15 17:12:18 Finished examples/xlrup_checker/array/compilation              1m38s   5GB
Aug 15 17:12:19 Starting examples/xlrup_checker/array/compilation/proofs
Aug 15 17:13:51 Finished examples/xlrup_checker/array/compilation/proofs       1m30s   5GB
Aug 15 17:13:52 Starting examples/cnf
Aug 15 17:14:15 Finished examples/cnf                                            22s 419MB
Aug 15 17:14:16 Starting examples/cnf/array
Aug 15 17:16:34 Finished examples/cnf/array                                    2m16s   2GB
Aug 15 17:16:34 Starting examples/cnf/dist
Aug 15 17:16:41 Finished examples/cnf/dist                                        5s 265MB
Aug 15 17:16:41 Starting examples/cnf/dist/array
Aug 15 17:23:30 Finished examples/cnf/dist/array                               6m47s   7GB
Aug 15 17:23:31 Starting examples/cnf/dist/array/compilation
Aug 15 17:24:34 Finished examples/cnf/dist/array/compilation                   1m02s   3GB
Aug 15 17:24:35 Starting examples/cnf/dist/array/compilation/proofs
Aug 15 17:25:55 Finished examples/cnf/dist/array/compilation/proofs            1m18s   4GB
Aug 15 17:25:55 Starting examples/scpog_checker
Aug 15 17:26:44 Finished examples/scpog_checker                                  47s   1GB
Aug 15 17:26:45 Starting examples/scpog_checker/array
Aug 15 17:32:35 Finished examples/scpog_checker/array                          5m48s   2GB
Aug 15 17:32:35 Starting examples/scpog_checker/array/compilation
Aug 15 17:35:10 Finished examples/scpog_checker/array/compilation              2m33s   8GB
Aug 15 17:35:11 Starting examples/scpog_checker/array/compilation/proofs
Aug 15 17:36:54 Finished examples/scpog_checker/array/compilation/proofs       1m42s   6GB
Aug 15 17:36:55 Starting examples/pseudo_bool
Aug 15 17:39:14 Finished examples/pseudo_bool                                  2m18s   2GB
Aug 15 17:39:15 Starting examples/pseudo_bool/cnf_encoding
Aug 15 17:39:50 Finished examples/pseudo_bool/cnf_encoding                       33s 968MB
Aug 15 17:39:50 Starting examples/pseudo_bool/graph_encoding
Aug 15 17:40:41 Finished examples/pseudo_bool/graph_encoding                     49s   1GB
Aug 15 17:40:42 Starting examples/pseudo_bool/array
Aug 15 18:23:55 Finished examples/pseudo_bool/array                           43m12s  20GB
Aug 15 18:23:56 Starting examples/pseudo_bool/array/compilation
Aug 15 18:47:27 Finished examples/pseudo_bool/array/compilation               23m29s  22GB
Aug 15 18:47:28 Starting examples/pseudo_bool/array/compilation/proofs
Aug 15 18:55:18 Finished examples/pseudo_bool/array/compilation/proofs         7m49s   9GB
Aug 15 18:55:18 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 15 18:57:59 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m40s   8GB
Aug 15 18:58:00 Starting examples/pseudo_bool/cp_encoding
Aug 15 19:01:11 Finished examples/pseudo_bool/cp_encoding                      3m10s   1GB
Aug 15 19:01:12 Starting examples/pseudo_bool/cp_encoding/array
Aug 15 19:05:48 FAILED: examples/pseudo_bool/cp_encoding/array
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/algorithms
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
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)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/pseudo_bool
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(CAKEMLDIR)/examples/pseudo_bool/cnf_encoding
Scanning $(CAKEMLDIR)/examples/pseudo_bool/graph_encoding
Scanning $(CAKEMLDIR)/examples/pseudo_bool/array
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/examples/pseudo_bool/cp_encoding
Scanned 75 directories
Building 1 theory file
Starting work on README.md
Starting work on cpProgTheory
README.md                                                   (0s)             OK
cpProgTheory                                              (266s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** cpProgTheory (status 1)
 Saved theorem _______ "encode_nivar_v_thm"
 Translating proj_ivar
 Adding nsLookup representation thms for [cpProg_env_474]
 Saved theorem _______ "nsLookup_cpProg_env_475_pfun_eqs"
 Saved theorem _______ "proj_ivar_v_thm"
 Translating encode_prob_type
 Adding nsLookup representation thms for [cpProg_env_475]
 Saved theorem _______ "nsLookup_cpProg_env_476_pfun_eqs"
 Saved theorem _______ "encode_prob_type_v_thm"
 Translating format_string
 Adding nsLookup representation thms for [cpProg_env_476]
 Saved theorem _______ "nsLookup_cpProg_env_477_pfun_eqs"
 Saved theorem _______ "format_string_v_thm"
 <<HOL warning: ThmSetData.revise_data: 
   Theorems in set "compute":
     ADD<cpProg$generated_definition_def>
   invalidated by DelConstant(cpProg$generated_definition)>>
 Translating full_encode
 Adding nsLookup representation thms for [cpProg_env_477]
 Saved theorem _______ "nsLookup_cpProg_env_478_pfun_eqs"
 Saved theorem _______ "full_encode_v_thm"
 Translating conv_concl
 Adding nsLookup representation thms for [cpProg_env_478]
 Saved theorem _______ "nsLookup_cpProg_env_479_pfun_eqs"
 Saved theorem _______ "conv_concl_v_thm"
 Saved definition ____ "get_cp_inst_def"
 Saved theorem _______ "nsLookup_cpProg_env_480_pfun_eqs"
 Adding nsLookup representation thms for [cpProg_env_480, cpProg_env_479]
 Post condition: POSTv v. &(v = Conv (SOME (TypeStamp Some 2)) [fv]) * STDIO fs
 Using translator specification notfound_string_v_thm from theory npbc_parseProg
 Post condition: POSTv sv. STDIO fs * &vomap_TYPE (notfound_string f) sv
 Using translator specification parse_cp_inst_v_thm from theory cpProg
 Saved theorem _______ "parse_cp_file_spec"
 Saved theorem _______ "nsLookup_cpProg_env_481_pfun_eqs"
 Adding nsLookup representation thms for [cpProg_env_481]
 
 Exception raised at Q.store_thm_at:
 at Preterm.type-analysis:
   between line 1016, character 8 and line 1022, character 32:
   
 Type error in case expression.
   case res :(mlstring prob_type #
  mlstring list option #
  (mlstring lin_term # int) option # (mlstring list # mlstring pbc) list)
 result
   of INL err => get_cp_inst fs f = NONE | INR (cpobj,prob) => inst.
   get_cp_inst fs f = SOME inst  SND (SND inst) = cpobj 
   full_encode inst = prob
   Reason: Attempt to unify different type operators: list$list and option$option
 
 Full log: /scratch/cakeml/regression2/cakeml-3454/examples/pseudo_bool/cp_encoding/array/.hol/logs/cpProgTheory