CakeML Regression Test

Job 3625

CakeML:8a2450ce5c0a2fe71604fdb5bd1470b3a3054661
  Simplify small arithmetic translation preconditions (#1485) [Oct 18 07:32:47]
#1551 (index-arith)
Merging into:8f955936e9473e3c85b80d6cb87e552ca73fa048
  Merge pull request #1544 from CakeML/pancake_int [Oct 17 06:28:28]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:fairybread

Oct 18 07:40:29 Claimed job
Oct 18 07:40:33 Reusing HOL
Oct 18 07:40:43 Starting developers
Oct 18 07:41:40 Finished developers                                              56s   1GB
Oct 18 07:41:41 Starting developers/bin
Oct 18 07:41:52 Finished developers/bin                                           9s   1GB
Oct 18 07:41:53 Starting misc
Oct 18 07:42:41 Finished misc                                                    47s   1GB
Oct 18 07:42:42 Starting compiler/proofs
Oct 18 09:12:00 Finished compiler/proofs                                    1h29m17s  12GB
Oct 18 09:12:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 18 15:24:10 Finished compiler/bootstrap/compilation/x64/64/proofs       6h12m07s  91GB
Oct 18 15:24:11 Starting semantics/ffi
Oct 18 15:24:35 Finished semantics/ffi                                           23s   1GB
Oct 18 15:24:36 Starting semantics
Oct 18 15:24:44 Finished semantics                                                6s   1GB
Oct 18 15:24:44 Starting semantics/proofs
Oct 18 15:25:15 Finished semantics/proofs                                        29s   1GB
Oct 18 15:25:16 Starting semantics/alt_semantics
Oct 18 15:25:41 Finished semantics/alt_semantics                                 23s   1GB
Oct 18 15:25:42 Starting semantics/alt_semantics/proofs
Oct 18 15:30:05 Finished semantics/alt_semantics/proofs                        4m22s   2GB
Oct 18 15:30:06 Starting basis/pure
Oct 18 15:30:14 Finished basis/pure                                               7s   1GB
Oct 18 15:30:15 Starting translator
Oct 18 15:31:40 Finished translator                                            1m23s   3GB
Oct 18 15:31:41 Starting compiler/parsing
Oct 18 15:32:37 Finished compiler/parsing                                        55s   1GB
Oct 18 15:32:38 Starting characteristic
Oct 18 15:32:46 Finished characteristic                                           6s   1GB
Oct 18 15:32:47 Starting translator/monadic
Oct 18 15:32:54 Finished translator/monadic                                       6s   1GB
Oct 18 15:32:55 Starting translator/monadic/monad_base
Oct 18 15:33:03 Finished translator/monadic/monad_base                            6s   1GB
Oct 18 15:33:04 Starting profiler
Oct 18 15:33:39 Finished profiler                                                34s   2GB
Oct 18 15:33:40 Starting basis
Oct 18 15:35:43 Finished basis                                                 2m01s   4GB
Oct 18 15:35:44 Starting compiler
Oct 18 15:35:51 Finished compiler                                                 6s   1GB
Oct 18 15:35:52 Starting compiler/inference
Oct 18 15:36:00 Finished compiler/inference                                       6s   1GB
Oct 18 15:36:01 Starting compiler/backend/reg_alloc
Oct 18 15:36:08 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 18 15:36:09 Starting compiler/backend/gc
Oct 18 15:36:17 Finished compiler/backend/gc                                      6s   1GB
Oct 18 15:36:18 Starting compiler/backend
Oct 18 15:36:29 Finished compiler/backend                                        10s   1GB
Oct 18 15:36:30 Starting compiler/backend/tests
Oct 18 15:37:03 Finished compiler/backend/tests                                  32s   1GB
Oct 18 15:37:04 Starting compiler/encoders/asm
Oct 18 15:37:11 Finished compiler/encoders/asm                                    6s   1GB
Oct 18 15:37:12 Starting compiler/encoders/x64
Oct 18 15:37:20 Finished compiler/encoders/x64                                    6s   1GB
Oct 18 15:37:21 Starting compiler/encoders/arm7
Oct 18 15:37:28 Finished compiler/encoders/arm7                                   6s   1GB
Oct 18 15:37:29 Starting compiler/encoders/arm8
Oct 18 15:37:36 Finished compiler/encoders/arm8                                   6s   1GB
Oct 18 15:37:37 Starting compiler/encoders/arm8_asl
Oct 18 15:37:59 Finished compiler/encoders/arm8_asl                              21s   1GB
Oct 18 15:38:00 Starting compiler/encoders/mips
Oct 18 15:38:08 Finished compiler/encoders/mips                                   6s   1GB
Oct 18 15:38:09 Starting compiler/encoders/riscv
Oct 18 15:38:16 Finished compiler/encoders/riscv                                  6s   1GB
Oct 18 15:38:17 Starting compiler/encoders/ag32
Oct 18 15:38:25 Finished compiler/encoders/ag32                                   6s   1GB
Oct 18 15:38:26 Starting compiler/encoders/tests
Oct 18 15:39:07 Finished compiler/encoders/tests                                 40s   2GB
Oct 18 15:39:08 Starting compiler/encoders/monadic_enc
Oct 18 15:39:36 Finished compiler/encoders/monadic_enc                           26s   1GB
Oct 18 15:39:37 Starting compiler/backend/x64
Oct 18 15:39:44 Finished compiler/backend/x64                                     6s   1GB
Oct 18 15:39:45 Starting compiler/backend/arm7
Oct 18 15:39:52 Finished compiler/backend/arm7                                    6s   1GB
Oct 18 15:39:53 Starting compiler/backend/arm8
Oct 18 15:40:01 Finished compiler/backend/arm8                                    6s   1GB
Oct 18 15:40:02 Starting compiler/backend/mips
Oct 18 15:40:09 Finished compiler/backend/mips                                    6s   1GB
Oct 18 15:40:10 Starting compiler/backend/riscv
Oct 18 15:40:17 Finished compiler/backend/riscv                                   6s   1GB
Oct 18 15:40:18 Starting compiler/backend/ag32
Oct 18 15:41:31 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 18 15:41:32 Starting compiler/backend/pattern_matching
Oct 18 15:41:53 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 18 15:41:54 Starting compiler/printing
Oct 18 15:42:56 Finished compiler/printing                                     1m01s   1GB
Oct 18 15:42:57 Starting compiler/parsing/proofs
Oct 18 15:43:05 Finished compiler/parsing/proofs                                  6s   1GB
Oct 18 15:43:06 Starting compiler/inference/proofs
Oct 18 15:43:13 Finished compiler/inference/proofs                                6s   1GB
Oct 18 15:43:14 Starting compiler/backend/semantics
Oct 18 15:45:55 Finished compiler/backend/semantics                            2m39s   1GB
Oct 18 15:45:56 Starting compiler/backend/reg_alloc/proofs
Oct 18 15:46:04 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 18 15:46:05 Starting compiler/backend/proofs
Oct 18 15:47:00 Finished compiler/backend/proofs                                 54s   3GB
Oct 18 15:47:01 Starting compiler/backend/serialiser
Oct 18 15:47:09 Finished compiler/backend/serialiser                              6s   1GB
Oct 18 15:47:10 Starting compiler/encoders/x64/proofs
Oct 18 15:47:17 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 18 15:47:18 Starting compiler/encoders/arm7/proofs
Oct 18 16:00:34 Finished compiler/encoders/arm7/proofs                        13m15s   9GB
Oct 18 16:00:35 Starting compiler/encoders/arm8/proofs
Oct 18 16:13:01 Finished compiler/encoders/arm8/proofs                        12m25s  14GB
Oct 18 16:13:02 Starting compiler/encoders/arm8_asl/proofs
Oct 18 16:41:48 Finished compiler/encoders/arm8_asl/proofs                    28m44s  34GB
Oct 18 16:41:49 Starting compiler/encoders/mips/proofs
Oct 18 16:53:41 Finished compiler/encoders/mips/proofs                        11m51s  10GB
Oct 18 16:53:42 Starting compiler/encoders/riscv/proofs
Oct 18 17:03:46 Finished compiler/encoders/riscv/proofs                       10m02s   4GB
Oct 18 17:03:47 Starting compiler/encoders/ag32/proofs
Oct 18 17:07:14 Finished compiler/encoders/ag32/proofs                         3m26s   1GB
Oct 18 17:07:15 Starting compiler/backend/x64/proofs
Oct 18 17:07:22 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 18 17:07:23 Starting compiler/backend/arm7/proofs
Oct 18 17:08:13 Finished compiler/backend/arm7/proofs                            49s   2GB
Oct 18 17:08:14 Starting compiler/backend/arm8/proofs
Oct 18 17:09:03 Finished compiler/backend/arm8/proofs                            47s   2GB
Oct 18 17:09:04 Starting compiler/backend/arm8_asl
Oct 18 17:09:53 Finished compiler/backend/arm8_asl                               47s   2GB
Oct 18 17:09:54 Starting compiler/backend/mips/proofs
Oct 18 17:10:46 Finished compiler/backend/mips/proofs                            51s   2GB
Oct 18 17:10:47 Starting compiler/backend/riscv/proofs
Oct 18 17:11:37 Finished compiler/backend/riscv/proofs                           48s   2GB
Oct 18 17:11:38 Starting compiler/backend/San
Oct 18 17:12:51 Finished compiler/backend/San                                  1m12s   3GB
Oct 18 17:12:52 Starting compiler/backend/ag32/proofs
Oct 18 17:22:41 Finished compiler/backend/ag32/proofs                          9m48s   4GB
Oct 18 17:22:42 Starting compiler/backend/cv_compute
Oct 18 17:23:19 Finished compiler/backend/cv_compute                             36s   1GB
Oct 18 17:23:20 Starting cv_translator
Oct 18 17:26:28 Finished cv_translator                                         3m07s   4GB
Oct 18 17:26:29 Starting candle
Oct 18 17:26:37 Finished candle                                                   6s   1GB
Oct 18 17:26:38 Starting candle/set-theory
Oct 18 17:27:00 Finished candle/set-theory                                       21s   1GB
Oct 18 17:27:01 Starting candle/syntax-lib
Oct 18 17:27:09 Finished candle/syntax-lib                                        6s   1GB
Oct 18 17:27:10 Starting candle/standard
Oct 18 17:27:17 Finished candle/standard                                          6s   1GB
Oct 18 17:27:18 Starting candle/standard/syntax
Oct 18 17:27:40 Finished candle/standard/syntax                                  20s   1GB
Oct 18 17:27:40 Starting candle/standard/syntax/little_theories
Oct 18 17:29:49 Finished candle/standard/syntax/little_theories                2m07s   1GB
Oct 18 17:29:50 Starting candle/standard/semantics
Oct 18 17:29:58 Finished candle/standard/semantics                                6s   1GB
Oct 18 17:29:59 Starting candle/standard/monadic
Oct 18 17:30:06 Finished candle/standard/monadic                                  6s   1GB
Oct 18 17:30:07 Starting candle/standard/ml_kernel
Oct 18 17:32:33 Finished candle/standard/ml_kernel                             2m24s   5GB
Oct 18 17:32:34 Starting candle/overloading
Oct 18 17:32:41 Finished candle/overloading                                       6s   1GB
Oct 18 17:32:42 Starting candle/overloading/syntax
Oct 18 17:36:13 Finished candle/overloading/syntax                             3m30s   2GB
Oct 18 17:36:14 Starting candle/overloading/semantics
Oct 18 17:44:58 Finished candle/overloading/semantics                          8m42s   3GB
Oct 18 17:44:58 Starting candle/overloading/monadic
Oct 18 17:47:14 Finished candle/overloading/monadic                            2m14s   1GB
Oct 18 17:47:15 Starting candle/overloading/ml_kernel
Oct 18 17:55:07 Finished candle/overloading/ml_kernel                          7m50s   6GB
Oct 18 17:55:08 Starting candle/overloading/ml_checker
Oct 18 17:57:27 Finished candle/overloading/ml_checker                         2m17s   7GB
Oct 18 17:57:27 Starting candle/prover
Oct 18 17:57:35 Finished candle/prover                                            6s   1GB
Oct 18 17:57:36 Starting candle/prover/compute
Oct 18 17:57:44 Finished candle/prover/compute                                    6s   1GB
Oct 18 17:57:45 Starting candle/parser
Oct 18 17:57:52 Finished candle/parser                                            6s   1GB
Oct 18 17:57:53 Starting pancake
Oct 18 17:58:01 Finished pancake                                                  6s   1GB
Oct 18 17:58:01 Starting pancake/semantics
Oct 18 18:01:31 Finished pancake/semantics                                     3m28s   2GB
Oct 18 18:01:32 Starting pancake/parser
Oct 18 18:02:21 Finished pancake/parser                                          48s   1GB
Oct 18 18:02:22 Starting pancake/static_checker
Oct 18 18:05:07 Finished pancake/static_checker                                2m44s   1GB
Oct 18 18:05:08 Starting pancake/proofs
Oct 18 18:22:51 Finished pancake/proofs                                       17m42s   6GB
Oct 18 18:22:52 Starting pancake/decompiler
Oct 18 18:23:49 Finished pancake/decompiler                                      56s   2GB
Oct 18 18:23:50 Starting pancake/decompiler/examples
Oct 18 18:24:43 Finished pancake/decompiler/examples                             52s   2GB
Oct 18 18:24:44 Starting compiler/dafny
Oct 18 18:25:15 Finished compiler/dafny                                          30s   1GB
Oct 18 18:25:16 Starting compiler/dafny/translation
Oct 18 18:37:55 Finished compiler/dafny/translation                           12m37s   7GB
Oct 18 18:37:56 Starting compiler/dafny/compilation
Oct 18 18:40:27 Finished compiler/dafny/compilation                            2m30s   7GB
Oct 18 18:40:28 Starting compiler/dafny/semantics
Oct 18 18:41:13 Finished compiler/dafny/semantics                                44s   1GB
Oct 18 18:41:14 Starting compiler/dafny/proofs
Oct 18 18:41:30 FAILED: compiler/dafny/proofs
  HOLORIG=/scratch/regbox/regression2/cakeml-3625/compiler/dafny/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
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)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/parser
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/tests
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64/64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/32
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
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)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
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/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/decompiler
Scanning $(CAKEMLDIR)/pancake/decompiler/examples
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 312 directories
Building 7 theory files
Starting work on README.md
Starting work on dafny_freshenProofTheory
Starting work on dafny_remove_assertProofTheory
Starting work on dafny_wp_calcTheory
README.md                            compiler/dafny/proofs  (0s)             OK
dafny_remove_assertProofTheory       compiler/dafny/proofs  (3s)   [1/7]     OK
dafny_freshenProofTheory             compiler/dafny/proofs  (7s)        FAIL<1>
dafny_wp_calcTheory                     compiler/dafny/vcg  (7s)         killed
*** Holmake aborted - 1 target failed:
*** dafny_freshenProofTheory in $(CAKEMLDIR)/compiler/dafny/proofs (status 1)
 Proved triviality ___ "locals_rel_push"
 Proved triviality ___ "locals_rel_from_map"
 Proved triviality ___ "locals_rel_read_local"
 Proved triviality ___ "opt_mmap_read_local"
 Proved triviality ___ "add_fresh_map_inv"
 Proved triviality ___ "map_add_fresh_map_inv"
 Proved triviality ___ "map_add_fresh_mono"
 Proved triviality ___ "map_add_fresh_distinct"
 Proved triviality ___ "map_add_fresh_len"
 Proved triviality ___ "map_add_fresh_exists"
 Proved triviality ___ "map_add_fresh_imp"
 Proved triviality ___ "map_add_fresh_all_distinct"
 Proved triviality ___ "map_add_fresh_ins_locals_rel"
 Proved triviality ___ "map_add_fresh_ins_outs_locals_rel"
 Proved triviality ___ "map_add_fresh_drop"
 Proved triviality ___ "freshen_exp_mono"
 Proved triviality ___ "freshen_lhs_exp_mono"
 Proved triviality ___ "freshen_lhs_exps_mono"
 Proved triviality ___ "freshen_rhs_exp_mono"
 Proved triviality ___ "freshen_rhs_exps_mono"
 Proved triviality ___ "freshen_stmt_mono"
 Proved triviality ___ "state_rel_mono"
 Proved triviality ___ "state_rel_dec_clock"
 Proved triviality ___ "state_rel_same_map_imp"
 Proved triviality ___ "state_rel_push_locals"
 Proved triviality ___ "state_rel_drop"
 Proved triviality ___ "get_member_aux_some"
 Proved triviality ___ "get_member_some"
 Proved triviality ___ "freshen_exps_len_eq"
 Proved triviality ___ "freshen_rhs_exp_len_eq"
 Proved triviality ___ "freshen_lhs_exp_len_eq"
 Proved triviality ___ "distinct_ins_lookup"
 Proof of 
 
 (s env e s' res t m m_old m_prev cnt cnt' e' env'.
    evaluate_exp s env e = (s',res)  state_rel s t m m_old m_prev cnt 
    freshen_exp m m_old m_prev cnt e = (cnt',e')  env_rel env env' 
    res  Rerr Rfail 
    t'.
      evaluate_exp t env' e' = (t',res)  state_rel s' t' m m_old m_prev cnt') 
 s env es s' res t m m_old m_prev cnt cnt' es' env'.
   evaluate_exps s env es = (s',res)  state_rel s t m m_old m_prev cnt 
   freshen_exps m m_old m_prev cnt es = (cnt',es')  env_rel env env' 
   res  Rerr Rfail 
   t'.
     evaluate_exps t env' es' = (t',res)  state_rel s' t' m m_old m_prev cnt'
 
 failed.
 Tactic failure proving "correct_freshen_exp"; heap saved to dafny_freshenProof.correct_freshen_exp.dumpedheap.
 Resume with: bin/hol --holstate=dafny_freshenProof.correct_freshen_exp.dumpedheap
 Full log: /scratch/regbox/regression2/cakeml-3625/compiler/dafny/proofs/.hol/logs/dafny_freshenProofTheory