[Hol-builds] SUCCESS: --expk:af8861b49:poly560:-F-t2

[<Mic...@da...>]

Running in /home/michaeln/regressionHOLs/expk on machine telemachus
Uname info (srm): Linux 3.13.0-143-generic x86_64
Cpu: Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz  x 8
Memory: 16005 MB
ML Implementation: poly560
Started: Tue, 24 Apr 2018 07:00:12 +1000
Extra commandline arguments: -F -t2
Revision: af8861b49 Merge branch 'master' into remove-term-eqtype
>From github.com:mn200/HOL
   6ad012b9a..126335620  mjcg       -> origin/mjcg
Already up-to-date.
-- Configuration Description Ends --

Building directory tools/Holmake/tests/holdep                  [24 Apr, 07:01:10]
Building directory tools/Holmake/tests/depchainloop            [24 Apr, 07:01:10]
Building directory tools/Holmake/tests/recursiveclean          [24 Apr, 07:01:10]
Building directory tools/set_mtime                             [24 Apr, 07:01:10]
Building directory tools/mlyacc/mlyacclib                      [24 Apr, 07:01:10]
Building directory src/portableML/poly                         [24 Apr, 07:01:10]
Building directory src/portableML                              [24 Apr, 07:01:10]
Building directory src/portableML/monads                       [24 Apr, 07:01:11]
Building directory src/portableML/testsrc                      [24 Apr, 07:01:11]
Building directory src/prekernel                               [24 Apr, 07:01:16]
Building directory src/experimental-kernel                     [24 Apr, 07:01:16]
Building directory src/thm                                     [24 Apr, 07:01:16]
Building directory src/postkernel                              [24 Apr, 07:01:16]
Building directory src/parse                                   [24 Apr, 07:01:16]
Building directory src/opentheory                              [24 Apr, 07:01:21]
Building directory src/bool                                    [24 Apr, 07:01:21]
Building directory src/1                                       [24 Apr, 07:01:28]
Building directory src/proofman                                [24 Apr, 07:01:40]
Building directory src/tactictoe/src                           [24 Apr, 07:01:45]
Building directory src/holyhammer/hh/hh1                       [24 Apr, 07:01:45]
Building directory src/holyhammer/hh                           [24 Apr, 07:01:45]
Building directory src/holyhammer                              [24 Apr, 07:01:45]
Building directory tools/Holmake/tests/depchain1/dir3          [24 Apr, 07:01:45]
Building directory tools/Holmake/tests/depchain2/dir1          [24 Apr, 07:01:46]
Building directory tools/Holmake/tests/altquote1               [24 Apr, 07:01:46]
Building directory tools/Holmake/tests/brokenstrings           [24 Apr, 07:01:46]
Building directory tools/Holmake/tests/holdep                  [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/nullary_tgt             [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/phony_tgt               [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/quote-filter            [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/cheatspotting           [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/depchain_heap/          [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/depchain_heap/dir2      [24 Apr, 07:01:47]
Building directory tools/Holmake/tests/coproduct               [24 Apr, 07:01:48]
Building directory tools/Holmake/tests/noprereqs/dir1          [24 Apr, 07:01:51]
Building directory tools/Holmake/tests/noprereqs/dir2          [24 Apr, 07:01:51]
Building directory tools/Holmake/tests/noprereqs/dir3          [24 Apr, 07:01:51]
Building directory tools/Holmake/tests/noprereqs/dir4          [24 Apr, 07:01:51]
Building directory tools/Holmake/tests/indepchildren           [24 Apr, 07:01:52]
Building directory src/1/theory_tests                          [24 Apr, 07:01:52]
Building directory src/compute/src                             [24 Apr, 07:01:54]
Building directory src/HolSat/sat_solvers/minisat              [24 Apr, 07:01:54]
Building directory src/HolSat/sat_solvers/zc2hs                [24 Apr, 07:01:58]
Building directory src/HolSat                                  [24 Apr, 07:01:59]
Building directory src/taut                                    [24 Apr, 07:01:59]
Building directory src/marker                                  [24 Apr, 07:01:59]
Building directory src/q                                       [24 Apr, 07:02:00]
Building directory src/combin                                  [24 Apr, 07:02:00]
Building directory src/lite                                    [24 Apr, 07:02:01]
Building directory src/refute                                  [24 Apr, 07:02:01]
Building directory src/simp/src                                [24 Apr, 07:02:04]
Building directory src/metis                                   [24 Apr, 07:02:07]
Building directory src/meson/src                               [24 Apr, 07:02:07]
Building directory src/IndDef                                  [24 Apr, 07:02:07]
Building directory src/basicProof                              [24 Apr, 07:02:09]
Building directory src/relation                                [24 Apr, 07:02:09]
Building directory src/coretypes                               [24 Apr, 07:02:16]
Building directory src/tfl/src                                 [24 Apr, 07:02:35]
Building directory src/num/theories                            [24 Apr, 07:02:41]
Building directory src/num/reduce/src                          [24 Apr, 07:03:11]
Building directory src/num/arith/src                           [24 Apr, 07:03:11]
Building directory src/num                                     [24 Apr, 07:03:20]
Building directory src/num/termination                         [24 Apr, 07:03:20]
Building directory src/num/extra_theories                      [24 Apr, 07:03:28]
Building directory src/pred_set/src                            [24 Apr, 07:03:36]
Building directory src/datatype/equiv                          [24 Apr, 07:04:14]
Building directory src/datatype/record                         [24 Apr, 07:04:14]
Building directory src/datatype                                [24 Apr, 07:04:14]
Building directory src/datatype/theory_tests                   [24 Apr, 07:04:19]
Building directory src/list/src                                [24 Apr, 07:04:26]
Building directory src/monad                                   [24 Apr, 07:04:49]
Building directory src/quantHeuristics                         [24 Apr, 07:04:54]
Building directory src/unwind                                  [24 Apr, 07:05:04]
Building directory src/pattern_matches                         [24 Apr, 07:05:04]
Building directory src/HolSat/vector_def_CNF                   [24 Apr, 07:05:34]
Building directory src/boss/ml_evaluation                      [24 Apr, 07:05:35]
Building directory src/boss                                    [24 Apr, 07:05:35]
Building directory tools/Holmake/tests/Iflag                   [24 Apr, 07:05:55]
Building directory tools/Holmake/tests/holpathdb/proj2         [24 Apr, 07:05:56]
Building directory src/boss/theory_tests                       [24 Apr, 07:05:58]
Building directory src/tfl/src/test                            [24 Apr, 07:06:00]
Building directory src/TeX                                     [24 Apr, 07:06:03]
Building directory src/TeX/theory_tests                        [24 Apr, 07:06:04]
Building directory src/TeX/theory_tests/proj1paper             [24 Apr, 07:06:09]
Building directory examples/RSA                                [24 Apr, 07:06:11]
Building directory examples/zipper                             [24 Apr, 07:06:14]
Building directory src/string                                  [24 Apr, 07:06:16]
Building directory src/sort                                    [24 Apr, 07:06:23]
Building directory src/string/theorytesting                    [24 Apr, 07:06:30]
Building directory src/tfl/examples                            [24 Apr, 07:06:31]
Building directory examples/STE                                [24 Apr, 07:06:44]
Building directory src/res_quan/src                            [24 Apr, 07:06:48]
Building directory src/quotient/src                            [24 Apr, 07:06:49]
Building directory src/hol88                                   [24 Apr, 07:06:55]
Building directory src/quotient/examples                       [24 Apr, 07:06:56]
Building directory src/finite_map                              [24 Apr, 07:07:00]
Building directory examples/ind_def                            [24 Apr, 07:07:09]
Building directory examples/decidable_separationLogic/src/     [24 Apr, 07:07:11]
Building directory src/bag                                     [24 Apr, 07:07:57]
Building directory examples/unification/triangular/first-order [24 Apr, 07:08:09]
Building directory src/n-bit                                   [24 Apr, 07:08:35]
Building directory examples/ARM/arm6-verification              [24 Apr, 07:09:28]
Building directory examples/ARM/arm6-verification/correctness  [24 Apr, 07:10:13]
Building directory src/ring/src                                [24 Apr, 07:12:48]
Building directory src/integer                                 [24 Apr, 07:12:55]
Building directory src/enumfset                                [24 Apr, 07:13:25]
Building directory examples/rings                              [24 Apr, 07:13:43]
Building directory src/coalgebras                              [24 Apr, 07:13:47]
Building directory src/integer/testing                         [24 Apr, 07:13:59]
Building directory src/patricia                                [24 Apr, 07:14:05]
Building directory src/transfer                                [24 Apr, 07:14:26]
Building directory src/update                                  [24 Apr, 07:14:28]
Building directory src/emit                                    [24 Apr, 07:14:29]
Building directory examples/ARM/v4                             [24 Apr, 07:14:37]
Building directory examples/ARM/v7                             [24 Apr, 07:16:16]
Building directory src/emit/ML                                 [24 Apr, 07:20:41]
Building directory src/emit/theory_tests                       [24 Apr, 07:20:42]
Building directory src/emit/theory_tests1                      [24 Apr, 07:20:46]
Building directory examples/dev                                [24 Apr, 07:20:49]
Building directory examples/imperative                         [24 Apr, 07:21:41]
Building directory src/quotient/examples/lambda                [24 Apr, 07:21:45]
Building directory src/quotient/examples/sigma                 [24 Apr, 07:22:07]
Building directory src/rational                                [24 Apr, 07:22:30]
Building directory src/datatype/inftree                        [24 Apr, 07:23:00]
Building directory examples/hfs                                [24 Apr, 07:23:01]
Building directory src/search                                  [24 Apr, 07:23:02]
Building directory examples/CCS                                [24 Apr, 07:23:05]
Building directory src/real                                    [24 Apr, 07:23:42]
Building directory src/HolQbf                                  [24 Apr, 07:24:30]
Building directory src/HolSmt                                  [24 Apr, 07:24:30]
Building directory examples/separationLogic/src/               [24 Apr, 07:25:03]
Building directory examples/separationLogic/src/holfoot        [24 Apr, 07:26:28]
Building directory examples/separationLogic/src/holfoot/poly   [24 Apr, 07:27:27]
Building directory examples/misc                               [24 Apr, 07:27:57]
Building directory examples/lambda/basics                      [24 Apr, 07:28:01]
Building directory examples/logic                              [24 Apr, 07:28:26]
Building directory examples/unification/triangular/nominal     [24 Apr, 07:28:30]
Building directory examples/lambda/barendregt                  [24 Apr, 07:29:43]
Building directory examples/computability                      [24 Apr, 07:30:32]
Building directory examples/lambda/other-models                [24 Apr, 07:30:37]
Building directory examples/lambda/typing                      [24 Apr, 07:30:50]
Building directory examples/computability/lambda               [24 Apr, 07:30:58]
Building directory examples/computability/register             [24 Apr, 07:32:00]
Building directory examples/computability/turing               [24 Apr, 07:32:05]
Building directory examples/balanced_bst                       [24 Apr, 07:32:28]
Building directory examples/formal-languages/regular           [24 Apr, 07:36:41]
Building directory src/Boolify/src                             [24 Apr, 07:38:47]
Building directory src/float                                   [24 Apr, 07:38:55]
Building directory src/floating-point                          [24 Apr, 07:39:12]
Building directory examples/l3-machine-code/common             [24 Apr, 07:39:56]
Building directory examples/l3-machine-code/decompilers        [24 Apr, 07:40:24]
Building directory src/floating-point/native                   [24 Apr, 07:56:34]
Building directory src/probability                             [24 Apr, 07:58:40]
Building directory src/temporal/src                            [24 Apr, 08:00:00]
Building directory examples/parity                             [24 Apr, 08:00:14]
Building directory examples/formal-languages                   [24 Apr, 08:00:15]
Building directory examples/formal-languages/context-free      [24 Apr, 08:00:15]
Building directory examples/MLsyntax                           [24 Apr, 08:01:46]
Building directory examples/set-theory/zfset                   [24 Apr, 08:01:47]
Building directory examples/set-theory/vbg                     [24 Apr, 08:02:01]
Building directory examples/set-theory/hol_sets                [24 Apr, 08:02:09]
Building directory examples/category                           [24 Apr, 08:02:55]
Building directory examples/miller/ho_prover                   [24 Apr, 08:03:43]
Building directory examples/miller/miller                      [24 Apr, 08:03:43]
Building directory examples/fun-op-sem/lprefix_lub             [24 Apr, 08:08:06]
Building directory examples/fun-op-sem/for                     [24 Apr, 08:08:10]
Building directory examples/logic/ltl                          [24 Apr, 08:09:18]
Building directory examples/Crypto/AES                         [24 Apr, 08:19:01]
Building directory examples/Crypto/IDEA                        [24 Apr, 08:20:45]
Building directory examples/Crypto/MARS                        [24 Apr, 08:21:09]
Building directory examples/Crypto/RC6                         [24 Apr, 08:24:33]
Building directory examples/Crypto/Serpent/Reference           [24 Apr, 08:24:40]
Building directory examples/Crypto/Serpent/Bitslice            [24 Apr, 08:26:46]
Building directory examples/Crypto/SHA-1                       [24 Apr, 08:28:50]
Building directory examples/Crypto/TEA                         [24 Apr, 08:28:58]
Building directory examples/Crypto/TWOFISH                     [24 Apr, 08:29:11]