Started by an SCM change [EnvInject] - Loading node environment variables. Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow [isabelle-nightly-slow] $ hg showconfig paths.default [isabelle-nightly-slow] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ searching for changes no changes found [isabelle-nightly-slow] $ hg update --clean --rev default 2 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all [isabelle-nightly-slow] $ hg log --rev . --template {node} [isabelle-nightly-slow] $ hg log --rev . --template {rev} [isabelle-nightly-slow] $ hg log --rev 6be69d6881cd829a29f9c68a89acc9342970e61d --template exists\n exists [isabelle-nightly-slow] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(6be69d6881cd829a29f9c68a89acc9342970e61d)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://bitbucket.org/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 6 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev df890a63c1faa44510471cf646c051209c831456 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(df890a63c1faa44510471cf646c051209c831456)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-nightly-slow] $ /bin/sh -xe /tmp/hudson6333705301140598468.sh + Admin/jenkins/run_build slow + set -e + PROFILE=slow + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building graph browser ... warning: [options] bootstrap class path not set in conjunction with -source 1.4 warning: [options] source value 1.4 is obsolete and will be removed in a future release warning: [options] target value 1.4 is obsolete and will be removed in a future release warning: [options] To suppress warnings about obsolete options, use -Xlint:-options. Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API. Note: Recompile with -Xlint:deprecation for details. 4 warnings ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ci_build_slow === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7-20170217/x86_64-linux" ML_SYSTEM="polyml-5.7" ML_OPTIONS="-H 4000 --maxheap 10G" === BUILD === Build started at Mon, 20 Feb 2017 01:35:01 +0100 Isabelle id b46fe5138cb0 Build for AFP id 901f6bfc8084 === LOG === Session Pure/Pure Session HOL/HOL (main) Session AFP/AWN (AFP) Session AFP/AODV (AFP slow) Session HOL/HOL-Analysis (main timing) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/HOL-ODE (AFP) Session AFP/HOL-ODE-Refinement (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-Examples (AFP slow) Session HOL/HOL-Library (main timing) Session AFP/ConcurrentIMP (AFP) Session AFP/ConcurrentGC (AFP slow) Session AFP/Flyspeck-Tame (AFP slow very_slow) Session HOL/HOL-Word (main timing) Session AFP/JinjaThreads (AFP slow) Session AFP/Word_Lib (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP slow very_slow) Building Pure ... Pure: theory Pure Pure: theory ML_Bootstrap Warning: missing document directory Timing Pure (1 threads, 0.817s elapsed time, 0.816s cpu time, 0.000s GC time, factor 1.00) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure Finished Pure (0:00:20 elapsed time, 0:00:20 cpu time, factor 0.99) Building HOL ... HOL: theory Code_Generator HOL: theory HOL HOL: theory Argo HOL: theory Ctr_Sugar HOL: theory Orderings HOL: theory SAT HOL: theory Groups HOL: theory Lattices HOL: theory Set HOL: theory Fun HOL: theory Typedef HOL: theory Rings HOL: theory Complete_Lattices HOL: theory Inductive HOL: theory Sum_Type HOL: theory Product_Type HOL: theory Complete_Partial_Order HOL: theory Nat HOL: theory Fields HOL: theory Meson HOL: theory ATP HOL: theory Metis HOL: theory Finite_Set HOL: theory Relation HOL: theory Transitive_Closure HOL: theory Wellfounded HOL: theory Fun_Def_Base HOL: theory Hilbert_Choice HOL: theory Wfrec HOL: theory Order_Relation HOL: theory BNF_Wellorder_Relation HOL: theory Zorn HOL: theory BNF_Wellorder_Embedding HOL: theory BNF_Wellorder_Constructions HOL: theory BNF_Cardinal_Order_Relation HOL: theory BNF_Cardinal_Arithmetic HOL: theory BNF_Def HOL: theory BNF_Composition HOL: theory Basic_BNFs HOL: theory BNF_Fixpoint_Base HOL: theory BNF_Least_Fixpoint HOL: theory Basic_BNF_LFPs HOL: theory Transfer HOL: theory Num HOL: theory Power HOL: theory Groups_Big HOL: theory Equiv_Relations HOL: theory Lifting HOL: theory Lifting_Set HOL: theory Quotient HOL: theory Option HOL: theory Extraction HOL: theory Lattices_Big HOL: theory Partial_Function HOL: theory Fun_Def HOL: theory Int HOL: theory Nat_Transfer HOL: theory Euclidean_Division HOL: theory Parity HOL: theory Divides HOL: theory Code_Numeral HOL: theory Numeral_Simprocs HOL: theory SMT HOL: theory Set_Interval HOL: theory Semiring_Normalization HOL: theory Conditionally_Complete_Lattices HOL: theory Filter HOL: theory Groebner_Basis HOL: theory Presburger HOL: theory Sledgehammer HOL: theory List HOL: theory Groups_List HOL: theory Map HOL: theory Enum HOL: theory Random HOL: theory String HOL: theory BNF_Greatest_Fixpoint HOL: theory Predicate HOL: theory Typerep HOL: theory Lazy_Sequence HOL: theory Limited_Sequence HOL: theory Code_Evaluation HOL: theory Quickcheck_Random HOL: theory Quickcheck_Exhaustive HOL: theory Random_Pred HOL: theory Quickcheck_Narrowing HOL: theory Random_Sequence HOL: theory Record HOL: theory Predicate_Compile HOL: theory Nitpick HOL: theory Main HOL: theory Archimedean_Field HOL: theory Binomial HOL: theory GCD HOL: theory Topological_Spaces HOL: theory Rat HOL: theory Real HOL: theory Real_Vector_Spaces HOL: theory Inequalities HOL: theory Limits HOL: theory Deriv HOL: theory Series HOL: theory NthRoot HOL: theory Transcendental HOL: theory Complex HOL: theory MacLaurin HOL: theory Complex_Main Timing HOL (8 threads, 247.945s elapsed time, 807.480s cpu time, 82.484s GC time, factor 3.26) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL/outline.pdf Finished HOL (0:05:34 elapsed time, 0:16:15 cpu time, factor 2.92) Building HOL-Library ... HOL-Library: theory Adhoc_Overloading HOL-Library: theory Lattice_Syntax HOL-Library: theory AList HOL-Library: theory BNF_Corec HOL-Library: theory Bits HOL-Library: theory Bit HOL-Library: theory Stirling HOL-Library: theory BNF_Axiomatization HOL-Library: theory Boolean_Algebra HOL-Library: theory Cancellation HOL-Library: theory Cardinal_Notations HOL-Library: theory Char_ord HOL-Library: theory Code_Abstract_Nat HOL-Library: theory Code_Binary_Nat HOL-Library: theory Code_Target_Nat HOL-Library: theory Code_Char HOL-Library: theory Code_Prolog HOL-Library: theory Code_Test HOL-Library: theory Combine_PER HOL-Library: theory Complete_Partial_Order2 HOL-Library: theory Multiset HOL-Library: theory Bits_Bit HOL-Library: theory Debug HOL-Library: theory Disjoint_Sets HOL-Library: theory Dlist HOL-Library: theory FSet HOL-Library: theory Fraction_Field HOL-Library: theory Fun_Lexorder HOL-Library: theory FuncSet HOL-Library: theory DAList HOL-Library: theory Function_Algebras HOL-Library: theory Function_Division HOL-Library: theory Code_Target_Int HOL-Library: theory Groups_Big_Fun HOL-Library: theory Code_Target_Numeral HOL-Library: theory IArray HOL-Library: theory Infinite_Set HOL-Library: theory LaTeXsugar HOL-Library: theory Lattice_Constructions HOL-Library: theory ListVector HOL-Library: theory Omega_Words_Fun HOL-Library: theory List_lexord HOL-Library: theory Mapping HOL-Library: theory Misc_Numeric HOL-Library: theory Misc_Typedef HOL-Library: theory Bit_Representation HOL-Library: theory Monad_Syntax HOL-Library: theory More_List HOL-Library: theory Nat_Bijection HOL-Library: theory Old_Datatype HOL-Library: theory Bits_Int HOL-Library: theory Finite_Map HOL-Library: theory AList_Mapping HOL-Library: theory Stream HOL-Library: theory Old_Recdef HOL-Library: theory Countable HOL-Library: theory Bool_List_Representation HOL-Library: theory Option_ord HOL-Library: theory Parallel HOL-Library: theory DAList_Multiset HOL-Library: theory Multiset_Order HOL-Library: theory Permutation HOL-Library: theory Permutations HOL-Library: theory Factorial_Ring HOL-Library: theory Perm HOL-Library: theory Phantom_Type HOL-Library: theory Predicate_Compile_Alternative_Defs HOL-Library: theory Product_Lexorder HOL-Library: theory Product_Plus HOL-Library: theory Quotient_Syntax HOL-Library: theory Quotient_Option HOL-Library: theory Product_Order HOL-Library: theory Quotient_Product HOL-Library: theory Countable_Set HOL-Library: theory Predicate_Compile_Quickcheck HOL-Library: theory Quotient_Set HOL-Library: theory Quotient_List HOL-Library: theory Finite_Lattice HOL-Library: theory Cardinality HOL-Library: theory Quotient_Sum HOL-Library: theory Quotient_Type HOL-Library: theory RBT_Impl HOL-Library: theory Countable_Complete_Lattices HOL-Library: theory Countable_Set_Type HOL-Library: theory Ramsey HOL-Library: theory Reflection HOL-Library: theory Refute HOL-Library: theory Rewrite HOL-Library: theory Set_Algebras HOL-Library: theory FinFun HOL-Library: theory Numeral_Type HOL-Library: theory Simps_Case_Conv HOL-Library: theory Extended HOL-Library: theory Type_Length HOL-Library: theory Saturated HOL-Library: theory State_Monad HOL-Library: theory Sublist HOL-Library: theory Polynomial HOL-Library: theory BigO HOL-Library: theory Code_Real_Approx_By_Float HOL-Library: theory Diagonal_Subsequence HOL-Library: theory Discrete HOL-Library: theory Indicator_Function HOL-Library: theory Prefix_Order HOL-Library: theory Sublist_Order HOL-Library: theory Lattice_Algebras HOL-Library: theory Liminf_Limsup HOL-Library: theory Log_Nat HOL-Library: theory Lub_Glb HOL-Library: theory Multiset_Permutations HOL-Library: theory Nonpos_Ints HOL-Library: theory OptionalSugar HOL-Library: theory Order_Continuity HOL-Library: theory Periodic_Fun HOL-Library: theory Quadratic_Discriminant HOL-Library: theory Sum_of_Squares HOL-Library: theory Transitive_Closure_Table HOL-Library: theory Tree HOL-Library: theory Extended_Nat HOL-Library: theory While_Combinator HOL-Library: theory Bourbaki_Witt_Fixpoint HOL-Library: theory Extended_Real HOL-Library: theory Linear_Temporal_Logic_on_Streams HOL-Library: theory Word_Miscellaneous HOL-Library: theory Euclidean_Algorithm HOL-Library: theory Word HOL-Library: theory Preorder HOL-Library: theory Function_Growth HOL-Library: theory Tree_Multiset HOL-Library: theory Float HOL-Library: theory Fundamental_Theorem_Algebra HOL-Library: theory Extended_Nonnegative_Real HOL-Library: theory Old_SMT HOL-Library: theory Normalized_Fraction HOL-Library: theory Formal_Power_Series HOL-Library: theory Field_as_Ring HOL-Library: theory Polynomial_Factorial HOL-Library: theory Polynomial_FPS HOL-Library: theory Library HOL-Library: theory RBT HOL-Library: theory RBT_Mapping HOL-Library: theory RBT_Set Timing HOL-Library (8 threads, 163.222s elapsed time, 917.944s cpu time, 75.672s GC time, factor 5.62) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library/outline.pdf Finished HOL-Library (0:04:12 elapsed time, 0:18:18 cpu time, factor 4.36) Building HOL-Word ... HOL-Word: theory Bits HOL-Word: theory Bit HOL-Word: theory Boolean_Algebra HOL-Word: theory Misc_Numeric HOL-Word: theory Phantom_Type HOL-Word: theory Misc_Typedef HOL-Word: theory Bit_Representation HOL-Word: theory Bits_Bit HOL-Word: theory Word_Miscellaneous HOL-Word: theory Bits_Int HOL-Word: theory Cardinality HOL-Word: theory Numeral_Type HOL-Word: theory Bool_List_Representation HOL-Word: theory Type_Length HOL-Word: theory Word Timing HOL-Word (8 threads, 13.818s elapsed time, 62.860s cpu time, 2.084s GC time, factor 4.55) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Word/outline.pdf Finished HOL-Word (0:00:34 elapsed time, 0:01:40 cpu time, factor 2.94) Building AWN ... AWN: theory Lib AWN: theory TransitionSystems AWN: theory AWN AWN: theory Invariants AWN: theory OInvariants AWN: theory AWN_Cterms AWN: theory AWN_SOS AWN: theory OAWN_SOS AWN: theory AWN_Labels AWN: theory Inv_Cterms AWN: theory Pnet AWN: theory AWN_Invariants AWN: theory AWN_SOS_Labels AWN: theory Closed AWN: theory Qmsg AWN: theory OAWN_Invariants AWN: theory OAWN_SOS_Labels AWN: theory ONode_Lifting AWN: theory OPnet AWN: theory OPnet_Lifting AWN: theory OClosed_Lifting AWN: theory OClosed_Transfer AWN: theory OAWN_Convert AWN: theory Qmsg_Lifting AWN: theory AWN_Main AWN: theory Toy Timing AWN (8 threads, 53.605s elapsed time, 270.156s cpu time, 9.920s GC time, factor 5.04) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN/outline.pdf Finished AWN (0:01:57 elapsed time, 0:06:07 cpu time, factor 3.13) Building ConcurrentIMP ... ConcurrentIMP: theory CIMP_pred ConcurrentIMP: theory CIMP_lang ConcurrentIMP: theory CIMP_vcg ConcurrentIMP: theory CIMP ConcurrentIMP: theory CIMP_one_place_buffer_ex ConcurrentIMP: theory CIMP_unbounded_buffer_ex Timing ConcurrentIMP (8 threads, 22.506s elapsed time, 54.424s cpu time, 2.692s GC time, factor 2.42) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP/outline.pdf Finished ConcurrentIMP (0:00:58 elapsed time, 0:02:00 cpu time, factor 2.05) Building Word_Lib ... Word_Lib: theory Sublist Word_Lib: theory WordBitwise Word_Lib: theory Prefix_Order Word_Lib: theory HOL_Lemmas Word_Lib: theory More_Divides Word_Lib: theory Hex_Words Word_Lib: theory Signed_Words Word_Lib: theory Enumeration Word_Lib: theory Norm_Words Word_Lib: theory WordBitwise_Signed Word_Lib: theory Word_Syntax Word_Lib: theory Word_Lib Word_Lib: theory Aligned Word_Lib: theory Word_Enum Word_Lib: theory Word_Setup_32 Word_Lib: theory Word_Setup_64 Word_Lib: theory Word_Lemmas Word_Lib: theory Word_Lemmas_32 Word_Lib: theory Word_Lemmas_64 Timing Word_Lib (8 threads, 77.659s elapsed time, 192.848s cpu time, 4.708s GC time, factor 2.48) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib/outline.pdf Finished Word_Lib (0:01:36 elapsed time, 0:03:45 cpu time, factor 2.34) Building IP_Addresses ... IP_Addresses: theory Cancellation IP_Addresses: theory NumberWang_IPv4 IP_Addresses: theory NumberWang_IPv6 IP_Addresses: theory Option_ord IP_Addresses: theory Char_ord IP_Addresses: theory Infinite_Set IP_Addresses: theory Code_Abstract_Nat IP_Addresses: theory Code_Target_Int IP_Addresses: theory Word_More IP_Addresses: theory Code_Target_Nat IP_Addresses: theory Code_Char IP_Addresses: theory Multiset IP_Addresses: theory Quicksort IP_Addresses: theory List_More IP_Addresses: theory Misc IP_Addresses: theory Hs_Compat IP_Addresses: theory Product_Lexorder IP_Addresses: theory Lib_Numbers_toString IP_Addresses: theory Word_Next IP_Addresses: theory WordInterval IP_Addresses: theory Lib_List_toString IP_Addresses: theory Lib_Word_toString IP_Addresses: theory IP_Address IP_Addresses: theory WordInterval_Sorted IP_Addresses: theory IPv4 IP_Addresses: theory IPv6 IP_Addresses: theory Prefix_Match IP_Addresses: theory CIDR_Split IP_Addresses: theory IP_Address_Parser IP_Addresses: theory IP_Address_toString Timing IP_Addresses (8 threads, 333.388s elapsed time, 1028.280s cpu time, 61.668s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses/outline.pdf Finished IP_Addresses (0:06:18 elapsed time, 0:18:53 cpu time, factor 2.99) Building Simple_Firewall ... Simple_Firewall: theory Firewall_Common_Decision_State Simple_Firewall: theory Iface Simple_Firewall: theory Lib_Enum_toString Simple_Firewall: theory GroupF Simple_Firewall: theory Option_Helpers Simple_Firewall: theory IP_Partition_Preliminaries Simple_Firewall: theory List_Product_More Simple_Firewall: theory IP_Addr_WordInterval_toString Simple_Firewall: theory L4_Protocol Simple_Firewall: theory Simple_Packet Simple_Firewall: theory Primitives_toString Simple_Firewall: theory SimpleFw_Syntax Simple_Firewall: theory SimpleFw_Semantics Simple_Firewall: theory Shadowed Simple_Firewall: theory Generic_SimpleFw Simple_Firewall: theory Service_Matrix Timing Simple_Firewall (8 threads, 27.162s elapsed time, 106.832s cpu time, 4.376s GC time, factor 3.93) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall/outline.pdf Finished Simple_Firewall (0:01:00 elapsed time, 0:02:53 cpu time, factor 2.90) Building Routing ... Routing: theory Adhoc_Overloading Routing: theory Monad_Syntax Routing: theory Linorder_Helper Routing: theory Prefix_Match_toString Routing: theory Routing_Table Routing: theory IpRoute_Parser Routing: theory Linux_Router Timing Routing (8 threads, 13.317s elapsed time, 49.164s cpu time, 1.052s GC time, factor 3.69) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing/outline.pdf Finished Routing (0:00:40 elapsed time, 0:01:35 cpu time, factor 2.35) Building Iptables_Semantics ... Iptables_Semantics: theory LaTeXsugar Iptables_Semantics: theory List_Misc Iptables_Semantics: theory More_Bits_Int Iptables_Semantics: theory Negation_Type Iptables_Semantics: theory WordInterval_Lists Iptables_Semantics: theory Bits_Integer Iptables_Semantics: theory Code_Target_Bits_Int Iptables_Semantics: theory Conntrack_State Iptables_Semantics: theory Negation_Type_DNF Iptables_Semantics: theory Remdups_Rev Iptables_Semantics: theory L4_Protocol_Flags Iptables_Semantics: theory SimpleFw_toString Iptables_Semantics: theory Ternary Iptables_Semantics: theory Repeat_Stabilize Iptables_Semantics: theory Datatype_Selectors Iptables_Semantics: theory IpAddresses Iptables_Semantics: theory Firewall_Common Iptables_Semantics: theory Word_Upto Iptables_Semantics: theory Ports Iptables_Semantics: theory Tagged_Packet Iptables_Semantics: theory Common_Primitive_Syntax Iptables_Semantics: theory Semantics Iptables_Semantics: theory Semantics_Goto Iptables_Semantics: theory Matching_Ternary Iptables_Semantics: theory Matching Iptables_Semantics: theory Semantics_Stateful Iptables_Semantics: theory Ruleset_Update Iptables_Semantics: theory Call_Return_Unfolding Iptables_Semantics: theory Semantics_Ternary Iptables_Semantics: theory Unknown_Match_Tacs Iptables_Semantics: theory Matching_Embeddings Iptables_Semantics: theory Fixed_Action Iptables_Semantics: theory Optimizing Iptables_Semantics: theory Normalized_Matches Iptables_Semantics: theory Common_Primitive_Matcher_Generic Iptables_Semantics: theory Negation_Type_Matching Iptables_Semantics: theory Primitive_Normalization Iptables_Semantics: theory Common_Primitive_Matcher Iptables_Semantics: theory MatchExpr_Fold Iptables_Semantics: theory Ipassmt Iptables_Semantics: theory Routing_IpAssmt Iptables_Semantics: theory Common_Primitive_toString Iptables_Semantics: theory Common_Primitive_Lemmas Iptables_Semantics: theory Conntrack_State_Transform Iptables_Semantics: theory Example_Semantics Iptables_Semantics: theory Interfaces_Normalize Iptables_Semantics: theory No_Spoof Iptables_Semantics: theory IpAddresses_Normalize Iptables_Semantics: theory Ports_Normalize Iptables_Semantics: theory Protocols_Normalize Iptables_Semantics: theory Output_Interface_Replace Iptables_Semantics: theory Interface_Replace Iptables_Semantics: theory Transform Iptables_Semantics: theory Primitive_Abstract Iptables_Semantics: theory SimpleFw_Compliance Iptables_Semantics: theory Code_Interface Iptables_Semantics: theory Semantics_Embeddings Iptables_Semantics: theory Iptables_Semantics Iptables_Semantics: theory No_Spoof_Embeddings Iptables_Semantics: theory Parser Iptables_Semantics: theory Documentation Iptables_Semantics: theory Code_haskell Timing Iptables_Semantics (8 threads, 196.601s elapsed time, 821.944s cpu time, 62.444s GC time, factor 4.18) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline.pdf Finished Iptables_Semantics (0:04:28 elapsed time, 0:16:53 cpu time, factor 3.77) Building HOL-Analysis ... HOL-Analysis: theory Old_Datatype HOL-Analysis: theory FuncSet HOL-Analysis: theory Cancellation HOL-Analysis: theory Product_Plus HOL-Analysis: theory Infinite_Set HOL-Analysis: theory Nat_Bijection HOL-Analysis: theory Phantom_Type HOL-Analysis: theory Disjoint_Sets HOL-Analysis: theory Product_Order HOL-Analysis: theory Set_Algebras HOL-Analysis: theory L2_Norm HOL-Analysis: theory Discrete HOL-Analysis: theory Indicator_Function HOL-Analysis: theory Inner_Product HOL-Analysis: theory Multiset HOL-Analysis: theory Liminf_Limsup HOL-Analysis: theory Nonpos_Ints HOL-Analysis: theory Operator_Norm HOL-Analysis: theory Cardinality HOL-Analysis: theory Periodic_Fun HOL-Analysis: theory Poly_Roots HOL-Analysis: theory Sum_of_Squares HOL-Analysis: theory Countable HOL-Analysis: theory Product_Vector HOL-Analysis: theory Numeral_Type HOL-Analysis: theory Euclidean_Space HOL-Analysis: theory Countable_Set HOL-Analysis: theory Countable_Complete_Lattices HOL-Analysis: theory Continuum_Not_Denumerable HOL-Analysis: theory Norm_Arith HOL-Analysis: theory Finite_Cartesian_Product HOL-Analysis: theory Linear_Algebra HOL-Analysis: theory Permutations HOL-Analysis: theory Factorial_Ring HOL-Analysis: theory Order_Continuity HOL-Analysis: theory Extended_Nat HOL-Analysis: theory Topology_Euclidean_Space HOL-Analysis: theory Extended_Real HOL-Analysis: theory Extended_Nonnegative_Real HOL-Analysis: theory Summation_Tests HOL-Analysis: theory Euclidean_Algorithm HOL-Analysis: theory Sigma_Algebra HOL-Analysis: theory Bounded_Linear_Function HOL-Analysis: theory Convex_Euclidean_Space HOL-Analysis: theory Extended_Real_Limits HOL-Analysis: theory Tagged_Division HOL-Analysis: theory Uniform_Limit HOL-Analysis: theory Measurable HOL-Analysis: theory Measure_Space HOL-Analysis: theory Caratheodory HOL-Analysis: theory Primes HOL-Analysis: theory Continuous_Extension HOL-Analysis: theory Path_Connected HOL-Analysis: theory Homeomorphism HOL-Analysis: theory Brouwer_Fixpoint HOL-Analysis: theory Derivative HOL-Analysis: theory Cartesian_Euclidean_Space HOL-Analysis: theory Weierstrass_Theorems HOL-Analysis: theory Determinants HOL-Analysis: theory Fashoda_Theorem HOL-Analysis: theory Ordered_Euclidean_Space HOL-Analysis: theory Polytope HOL-Analysis: theory Arcwise_Connected HOL-Analysis: theory Borel_Space HOL-Analysis: theory Nonnegative_Lebesgue_Integration HOL-Analysis: theory Regularity HOL-Analysis: theory Binary_Product_Measure HOL-Analysis: theory Embed_Measure HOL-Analysis: theory Finite_Product_Measure HOL-Analysis: theory Bochner_Integration HOL-Analysis: theory Function_Topology HOL-Analysis: theory Complete_Measure HOL-Analysis: theory Radon_Nikodym HOL-Analysis: theory Lebesgue_Measure HOL-Analysis: theory Set_Integral HOL-Analysis: theory Henstock_Kurzweil_Integration HOL-Analysis: theory Bounded_Continuous_Function HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory Integral_Test HOL-Analysis: theory Complex_Analysis_Basics HOL-Analysis: theory Interval_Integral HOL-Analysis: theory Lebesgue_Integral_Substitution HOL-Analysis: theory Complex_Transcendental HOL-Analysis: theory Generalised_Binomial_Theorem HOL-Analysis: theory Harmonic_Numbers HOL-Analysis: theory Cauchy_Integral_Theorem HOL-Analysis: theory Further_Topology HOL-Analysis: theory Jordan_Curve HOL-Analysis: theory Conformal_Mappings HOL-Analysis: theory Gamma_Function HOL-Analysis: theory Analysis Timing HOL-Analysis (8 threads, 481.536s elapsed time, 2266.668s cpu time, 185.416s GC time, factor 4.71) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis/outline.pdf Finished HOL-Analysis (0:10:10 elapsed time, 0:41:31 cpu time, factor 4.08) Building Ordinary_Differential_Equations ... Ordinary_Differential_Equations: theory Code_Target_Int Ordinary_Differential_Equations: theory Dense_Linear_Order Ordinary_Differential_Equations: theory Code_Abstract_Nat Ordinary_Differential_Equations: theory Lattice_Algebras Ordinary_Differential_Equations: theory Diagonal_Subsequence Ordinary_Differential_Equations: theory Log_Nat Ordinary_Differential_Equations: theory Code_Target_Nat Ordinary_Differential_Equations: theory Code_Target_Numeral Ordinary_Differential_Equations: theory Float Ordinary_Differential_Equations: theory Approximation Ordinary_Differential_Equations: theory ODE_Auxiliarities Ordinary_Differential_Equations: theory Bounded_Linear_Operator Ordinary_Differential_Equations: theory Initial_Value_Problem Ordinary_Differential_Equations: theory MVT_Ex Ordinary_Differential_Equations: theory Multivariate_Taylor Ordinary_Differential_Equations: theory Picard_Lindeloef_Qualitative Ordinary_Differential_Equations: theory Flow Ordinary_Differential_Equations: theory Reachability_Analysis Ordinary_Differential_Equations: theory Upper_Lower_Solution Ordinary_Differential_Equations: theory Linear_ODE Ordinary_Differential_Equations: theory ODE_Analysis Timing Ordinary_Differential_Equations (8 threads, 171.157s elapsed time, 520.512s cpu time, 14.308s GC time, factor 3.04) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf Finished Ordinary_Differential_Equations (0:03:37 elapsed time, 0:10:03 cpu time, factor 2.77) Building HOL-ODE ... Timing HOL-ODE (8 threads, 0.173s elapsed time, 0.180s cpu time, 0.000s GC time, factor 1.04) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE Finished HOL-ODE (0:00:32 elapsed time, 0:00:48 cpu time, factor 1.50) Building HOL-ODE-Refinement ... HOL-ODE-Refinement: theory Adhoc_Overloading HOL-ODE-Refinement: theory AList HOL-ODE-Refinement: theory Bits HOL-ODE-Refinement: theory Omega_Words_Fun HOL-ODE-Refinement: theory Quicksort HOL-ODE-Refinement: theory Foldi HOL-ODE-Refinement: theory Boolean_Algebra HOL-ODE-Refinement: theory Bit HOL-ODE-Refinement: theory List_More HOL-ODE-Refinement: theory Misc_Numeric HOL-ODE-Refinement: theory Misc_Typedef HOL-ODE-Refinement: theory Bit_Representation HOL-ODE-Refinement: theory Monad_Syntax HOL-ODE-Refinement: theory Option_ord HOL-ODE-Refinement: theory Type_Length HOL-ODE-Refinement: theory Prio_List HOL-ODE-Refinement: theory RBT_Impl HOL-ODE-Refinement: theory Refine_Chapter HOL-ODE-Refinement: theory Refine_Util HOL-ODE-Refinement: theory While_Combinator HOL-ODE-Refinement: theory Bits_Bit HOL-ODE-Refinement: theory Word_Miscellaneous HOL-ODE-Refinement: theory Misc HOL-ODE-Refinement: theory Anti_Unification HOL-ODE-Refinement: theory Attr_Comb HOL-ODE-Refinement: theory Bits_Int HOL-ODE-Refinement: theory Autoref_Data HOL-ODE-Refinement: theory Named_Sorted_Thms HOL-ODE-Refinement: theory Mk_Term_Antiquot HOL-ODE-Refinement: theory Mpat_Antiquot HOL-ODE-Refinement: theory Tagged_Solver HOL-ODE-Refinement: theory Select_Solve HOL-ODE-Refinement: theory Indep_Vars HOL-ODE-Refinement: theory Mk_Record_Simp HOL-ODE-Refinement: theory Bool_List_Representation HOL-ODE-Refinement: theory More_Bits_Int HOL-ODE-Refinement: theory Word HOL-ODE-Refinement: theory Bits_Integer HOL-ODE-Refinement: theory SetIterator HOL-ODE-Refinement: theory Digraph_Basic HOL-ODE-Refinement: theory Refine_Lib HOL-ODE-Refinement: theory Autoref_Phases HOL-ODE-Refinement: theory Autoref_Tagging HOL-ODE-Refinement: theory Refine_Mono_Prover HOL-ODE-Refinement: theory Relators HOL-ODE-Refinement: theory SetIteratorOperations HOL-ODE-Refinement: theory Word_Misc HOL-ODE-Refinement: theory Param_Tool HOL-ODE-Refinement: theory Param_HOL HOL-ODE-Refinement: theory Parametricity HOL-ODE-Refinement: theory Autoref_Id_Ops HOL-ODE-Refinement: theory Assoc_List HOL-ODE-Refinement: theory Proper_Iterator HOL-ODE-Refinement: theory SetIteratorGA HOL-ODE-Refinement: theory Autoref_Fix_Rel HOL-ODE-Refinement: theory Diff_Array HOL-ODE-Refinement: theory It_to_It HOL-ODE-Refinement: theory Autoref_Translate HOL-ODE-Refinement: theory Autoref_Relator_Interface HOL-ODE-Refinement: theory Autoref_Gen_Algo HOL-ODE-Refinement: theory Autoref_Tool HOL-ODE-Refinement: theory Autoref_Bindings_HOL HOL-ODE-Refinement: theory Code_Target_Bits_Int HOL-ODE-Refinement: theory Uint HOL-ODE-Refinement: theory Uint32 HOL-ODE-Refinement: theory Code_Target_ICF HOL-ODE-Refinement: theory Automatic_Refinement HOL-ODE-Refinement: theory Idx_Iterator HOL-ODE-Refinement: theory Intf_Comp HOL-ODE-Refinement: theory Refine_Misc HOL-ODE-Refinement: theory Impl_Array_Stack HOL-ODE-Refinement: theory RefineG_Domain HOL-ODE-Refinement: theory RefineG_Transfer HOL-ODE-Refinement: theory RefineG_Assert HOL-ODE-Refinement: theory RefineG_Recursion HOL-ODE-Refinement: theory HashCode HOL-ODE-Refinement: theory Refine_Basic HOL-ODE-Refinement: theory RefineG_While HOL-ODE-Refinement: theory Intf_Hash HOL-ODE-Refinement: theory Refine_Det HOL-ODE-Refinement: theory Gen_Hash HOL-ODE-Refinement: theory Refine_Heuristics HOL-ODE-Refinement: theory Refine_Leof HOL-ODE-Refinement: theory Refine_Pfun HOL-ODE-Refinement: theory Refine_While HOL-ODE-Refinement: theory Refine_Transfer HOL-ODE-Refinement: theory Autoref_Monadic HOL-ODE-Refinement: theory Refine_Automation HOL-ODE-Refinement: theory Refine_Foreach HOL-ODE-Refinement: theory Refine_Monadic HOL-ODE-Refinement: theory Gen_Iterator HOL-ODE-Refinement: theory Intf_Map HOL-ODE-Refinement: theory Intf_Set HOL-ODE-Refinement: theory Impl_Cfun_Set HOL-ODE-Refinement: theory Iterator HOL-ODE-Refinement: theory Array_Iterator HOL-ODE-Refinement: theory Gen_Map HOL-ODE-Refinement: theory Gen_Map2Set HOL-ODE-Refinement: theory Gen_Set HOL-ODE-Refinement: theory Impl_Bit_Set HOL-ODE-Refinement: theory Impl_List_Set HOL-ODE-Refinement: theory Impl_Uv_Set HOL-ODE-Refinement: theory Impl_Array_Map HOL-ODE-Refinement: theory Impl_List_Map HOL-ODE-Refinement: theory Impl_Array_Hash_Map HOL-ODE-Refinement: theory RBT_add HOL-ODE-Refinement: theory Impl_RBT_Map HOL-ODE-Refinement: theory GenCF_No_Comp HOL-ODE-Refinement: theory Refine_Dflt_No_Comp Timing HOL-ODE-Refinement (8 threads, 128.105s elapsed time, 645.868s cpu time, 32.872s GC time, factor 5.04) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Refinement Finished HOL-ODE-Refinement (0:03:10 elapsed time, 0:14:04 cpu time, factor 4.43) Building HOL-ODE-Numerics ... HOL-ODE-Numerics: theory Permutation HOL-ODE-Numerics: theory Float_Real HOL-ODE-Numerics: theory Counterclockwise HOL-ODE-Numerics: theory Quotient_Syntax HOL-ODE-Numerics: theory Euclidean_Space_Explicit HOL-ODE-Numerics: theory Quotient_Set HOL-ODE-Numerics: theory Executable_Euclidean_Space HOL-ODE-Numerics: theory Affine_Form HOL-ODE-Numerics: theory Counterclockwise_Vector HOL-ODE-Numerics: theory Counterclockwise_2D_Strict HOL-ODE-Numerics: theory Counterclockwise_2D_Arbitrary HOL-ODE-Numerics: theory Polygon HOL-ODE-Numerics: theory Affine_Approximation HOL-ODE-Numerics: theory Affine_Code HOL-ODE-Numerics: theory Straight_Line_Program HOL-ODE-Numerics: theory Ex_Affine_Approximation HOL-ODE-Numerics: theory Ex_Ineqs HOL-ODE-Numerics: theory Intersection HOL-ODE-Numerics: theory Ex_Inter HOL-ODE-Numerics: theory Affine_Arithmetic HOL-ODE-Numerics: theory Char_ord HOL-ODE-Numerics: theory ICF_Tools HOL-ODE-Numerics: theory Generator_Aux HOL-ODE-Numerics: theory Optimize_Integer HOL-ODE-Numerics: theory Derive_Manager HOL-ODE-Numerics: theory One_Step_Method HOL-ODE-Numerics: theory Autoref_Misc HOL-ODE-Numerics: theory Ord_Code_Preproc HOL-ODE-Numerics: theory Code_Char HOL-ODE-Numerics: theory Show HOL-ODE-Numerics: theory Locale_Code HOL-ODE-Numerics: theory Optimize_Float HOL-ODE-Numerics: theory Runge_Kutta HOL-ODE-Numerics: theory Show_Instances HOL-ODE-Numerics: theory Print HOL-ODE-Numerics: theory Refine_Folds HOL-ODE-Numerics: theory Refine_String HOL-ODE-Numerics: theory Weak_Set HOL-ODE-Numerics: theory Plot HOL-ODE-Numerics: theory Refine_Rigorous_Numerics HOL-ODE-Numerics: theory Refine_Reachability_Analysis HOL-ODE-Numerics: theory Refine_Rigorous_Numerics_Aform HOL-ODE-Numerics: theory ODE_Numerics Timing HOL-ODE-Numerics (8 threads, 801.088s elapsed time, 1981.316s cpu time, 110.880s GC time, factor 2.47) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics Finished HOL-ODE-Numerics (0:14:43 elapsed time, 0:35:36 cpu time, factor 2.42) Running Flyspeck-Tame ... Flyspeck-Tame: theory Trie Flyspeck-Tame: theory Tries Flyspeck-Tame: theory Arch Flyspeck-Tame: theory Quasi_Order Flyspeck-Tame: theory ListAux Flyspeck-Tame: theory IArray_Syntax Flyspeck-Tame: theory RTranCl Flyspeck-Tame: theory PlaneGraphIso Flyspeck-Tame: theory Worklist Flyspeck-Tame: theory Maps Flyspeck-Tame: theory ListSum Flyspeck-Tame: theory Rotation Flyspeck-Tame: theory Graph Flyspeck-Tame: theory Enumerator Flyspeck-Tame: theory FaceDivision Flyspeck-Tame: theory GraphProps Flyspeck-Tame: theory Tame Flyspeck-Tame: theory Plane Flyspeck-Tame: theory EnumeratorProps Flyspeck-Tame: theory TameProps Flyspeck-Tame: theory Plane1 Flyspeck-Tame: theory Generator Flyspeck-Tame: theory FaceDivisionProps Flyspeck-Tame: theory TameEnum Flyspeck-Tame: theory Invariants Flyspeck-Tame: theory ArchCompAux Flyspeck-Tame: theory PlaneProps Flyspeck-Tame: theory Plane1Props Flyspeck-Tame: theory ScoreProps Flyspeck-Tame: theory LowerBound Flyspeck-Tame: theory GeneratorProps Flyspeck-Tame: theory TameEnumProps Flyspeck-Tame: theory ArchCompProps Flyspeck-Tame: theory ArchComp Flyspeck-Tame: theory Completeness Timing Flyspeck-Tame (8 threads, 36236.825s elapsed time, 54160.820s cpu time, 899.476s GC time, factor 1.49) Browser info at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/document.pdf Document at /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame/outline.pdf Finished Flyspeck-Tame (10:04:18 elapsed time, 15:03:05 cpu time, factor 1.49) Running Iptables_Semantics_Examples ... Iptables_Semantics_Examples: theory Analyze_Ringofsaturn_com Iptables_Semantics_Examples: theory Analyze_medium_sized_company Iptables_Semantics_Examples: theory Analyze_SQRL_Shorewall Iptables_Semantics_Examples: theory Analyze_topos_generated Iptables_Semantics_Examples: theory Analyze_TUM_Net_Firewall Iptables_Semantics_Examples: theory Contrived_Example Iptables_Semantics_Examples: theory IP_Address_Space_Examples_All_Small Iptables_Semantics_Examples: theory Parser_Test Iptables_Semantics_Examples: theory SNS_IAS_Eduroam_Spoofing Iptables_Semantics_Examples: theory SQRL_2015_nospoof Iptables_Semantics_Examples: theory TUM_Spoofing_new3 Iptables_Semantics_Examples: theory Parser6 Iptables_Semantics_Examples: theory Parser6_Test Iptables_Semantics_Examples: theory Ports_Fail Iptables_Semantics_Examples: theory Small_Examples Iptables_Semantics_Examples: theory iptables_Ln_tuned_parsed Iptables_Semantics_Examples: theory Analyze_Synology_Diskstation Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Run out of store - interrupting threads Failed to recover - exiting Iptables_Semantics_Examples FAILED (see also /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.7_x86_64-linux/log/Iptables_Semantics_Examples) Rule (MatchAnd (Match (Extra ''-d ::ffff:127.0.0.1/128'')) (MatchAnd (Match (IIface (Iface ''eth0''))) (Match (OIface (Iface ''foobar''))))) (Call ''gh32_-2qns''), Rule (MatchAnd (Match (Src (IpAddrNetmask 1 128))) (MatchAnd (Match (IIface (Iface ''lo''))) (Match (OIface (Iface ''lo''))))) action.Accept, Rule (Match (Extra [CHR ''-'', CHR ''-'', CHR ''l'', CHR ''o'', CHR ''g'', CHR ''-'', CHR ''p'', CHR ''r'', CHR ''e'', CHR ''f'', CHR ''i'', CHR ''x'', CHR '' '', CHR 0x22, CHR ''~'', CHR ''%'', CHR ''&'', CHR ''/'', CHR ''('', CHR '')'', CHR ''='', CHR ''?'', CHR 0x22, CHR '' '', CHR ''-'', CHR ''-'', CHR ''l'', CHR ''o'', CHR ''g'', CHR ''-'', CHR ''l'', CHR ''e'', CHR ''v'', CHR ''e'', CHR ''l'', CHR '' '', CHR ''6''])) Log, Rule (Match (Src (IpAddrNetmask 0 128))) action.Drop]), (''INPUT'', []), (''OUTPUT'', []), (''gh32_-2qns'', [Rule (Match (Src (IpAddrNetmask 0x20010DB885A308D313198A2E03707344 128))) Reject, Rule MatchAny Empty, Rule MatchAny action.Accept])]" :: "(char list \ 128 common_primitive rule list) list" Simplified term (23462.961 seconds) checked sanity with sanity_wf_ruleset (46.781 seconds) Defining constant `fw11_def' Defining constant `fw11_INPUT_default_policy_def' Defining constant `fw11_FORWARD_default_policy_def' Defining constant `fw11_OUTPUT_default_policy_def' loading file /media/data/jenkins/workspace/isabelle-nightly-slow/afp/thys/Iptables_Semantics/Examples/IPPartEval/medium-sized-company/iptables-save Loaded 602 lines of the filter table Parsed 7 chain declarations Parsed 595 rules unfolding (this may take a while) ... Running AODV ... AODV: theory Aodv_Basic AODV: theory A_Norreqid AODV: theory Aodv_Data AODV: theory B_Fwdrreps AODV: theory C_Gtobcast AODV: theory D_Fwdrreqs AODV: theory E_All_ABCD AODV: theory Aodv_Message AODV: theory A_Aodv_Data AODV: theory A_Aodv_Message AODV: theory D_Aodv_Data AODV: theory D_Aodv_Message AODV: theory B_Aodv_Data AODV: theory B_Aodv_Message AODV: theory Fresher AODV: theory C_Aodv_Data AODV: theory A_Fresher AODV: theory C_Aodv_Message AODV: theory B_Fresher AODV: theory E_Aodv_Data AODV: theory D_Fresher AODV: theory E_Aodv_Message AODV: theory A_Aodv AODV: theory Aodv AODV: theory B_Aodv AODV: theory D_Aodv AODV: theory C_Fresher AODV: theory E_Fresher AODV: theory C_Aodv AODV: theory E_Aodv AODV: theory Aodv_Predicates AODV: theory Loop_Freedom AODV: theory Quality_Increases AODV: theory Seq_Invariants AODV: theory OAodv AODV: theory Global_Invariants AODV: theory Aodv_Loop_Freedom AODV: theory A_Aodv_Predicates AODV: theory A_OAodv AODV: theory A_Loop_Freedom AODV: theory A_Quality_Increases AODV: theory A_Seq_Invariants AODV: theory A_Global_Invariants AODV: theory A_Aodv_Loop_Freedom AODV: theory B_Aodv_Predicates AODV: theory B_OAodv AODV: theory B_Loop_Freedom AODV: theory B_Quality_Increases AODV: theory B_Seq_Invariants AODV: theory B_Global_Invariants AODV: theory B_Aodv_Loop_Freedom AODV: theory C_Aodv_Predicates AODV: theory C_Loop_Freedom AODV: theory C_Quality_Increases AODV: theory C_Seq_Invariants AODV: theory E_Aodv_Predicates AODV: theory C_OAodv AODV: theory E_Loop_Freedom AODV: theory E_Quality_Increases AODV: theory E_Seq_Invariants AODV: theory C_Global_Invariants AODV: theory E_OAodv AODV: theory E_Global_Invariants AODV: theory C_Aodv_Loop_Freedom AODV: theory E_Aodv_Loop_Freedom AODV: theory D_Aodv_Predicates AODV: theory D_OAodv AODV: theory D_Loop_Freedom AODV: theory D_Quality_Increases AODV: theory D_Seq_Invariants AODV: theory D_Global_Invariants AODV: theory D_Aodv_Loop_Freedom AODV: theory All Build timed out (after 1,200 minutes). Marking the build as aborted. Build was aborted Archiving artifacts Terminated Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds No emails were triggered. Finished: ABORTED