Tool CPAchecker 1.6.1-svn 26773
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 10:49:29 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 3.4 300 29
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 3.5 280 32
signedintegeroverflow-regression/Division_false-no-overflow.c.i 3.6 280 32
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 3.4 280 27
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 3.4 280 34
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 3.5 280 31
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 3.4 280 29
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 3.7 280 32
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 3.4 270 31
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 3.5 280 31
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i 3.0 270 24
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i 3.1 270 30
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i 3.1 280 28
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i 3.0 280 24
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i 2.9 270 29
termination-crafted/2Nested_false-no-overflow.c 2.6 270 26
termination-crafted/4NestedWith3Variables_false-no-overflow.c 2.6 270 24
termination-crafted/Ackermann_false-no-overflow.c 900   3800 11000
termination-crafted/Bangalore_false-no-overflow.c 2.6 270 26
termination-crafted/Bangalore_v3_false-no-overflow.c 2.6 270 24
termination-crafted/Benghazi_nondet_false-no-overflow.c 2.7 280 27
termination-crafted/Binary_Search_false-no-overflow.c 2.9 290 25
termination-crafted/Cairo_nondet_false-no-overflow.c 2.7 270 22
termination-crafted/Cairo_step2_false-no-overflow.c 900   2600 13000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 2.8 280 28
termination-crafted/Copenhagen_disj_false-no-overflow.c 2.7 270 24
termination-crafted/Gothenburg_false-no-overflow.c 2.7 270 24
termination-crafted/Gothenburg_v2_false-no-overflow.c 2.7 270 22
termination-crafted/Hanoi_2vars_false-no-overflow.c 2.6 270 24
termination-crafted/Hanoi_3vars_false-no-overflow.c 2.7 270 22
termination-crafted/Hanoi_plus_false-no-overflow.c 2.7 270 25
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 2.5 270 24
termination-crafted/Mysore_false-no-overflow.c 2.7 270 23
termination-crafted/NestedRecursion_1a_false-no-overflow.c 2.7 270 26
termination-crafted/NestedRecursion_2a_false-no-overflow.c 2.7 270 26
termination-crafted/NonTermination1_false-no-overflow.c 2.7 280 24
termination-crafted/NonTermination2_false-no-overflow.c 3.0 280 27
termination-crafted/NonTermination4_false-no-overflow.c 190   1300 1500
termination-crafted/NonTerminationSimple2_false-no-overflow.c 2.8 270 23
termination-crafted/NonTerminationSimple3_false-no-overflow.c 2.7 270 21
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   2200 12000
termination-crafted/NonTerminationSimple5_false-no-overflow.c 2.7 270 23
termination-crafted/NonTerminationSimple6_false-no-overflow.c 2.6 270 23
termination-crafted/NonTerminationSimple8_false-no-overflow.c 2.7 280 26
termination-crafted/NonTerminationSimple9_false-no-overflow.c 2.7 280 26
termination-crafted/Pure2Phase_false-no-overflow.c 2.6 270 23
termination-crafted/Pure3Phase_false-no-overflow.c 2.7 270 25
termination-crafted/RecursiveMultiplication_false-no-overflow.c 3.5 300 30
termination-crafted/RecursiveNonterminating_false-no-overflow.c 2.6 270 21
termination-crafted/Rotation180_false-no-overflow.c 2.6 260 23
termination-crafted/Singapore_false-no-overflow.c 2.6 270 22
termination-crafted/Singapore_plus_false-no-overflow.c 2.8 270 23
termination-crafted/Singapore_v1_false-no-overflow.c 2.5 260 23
termination-crafted/Singapore_v2_false-no-overflow.c 2.6 270 26
termination-crafted/Stockholm_false-no-overflow.c 2.7 270 22
termination-crafted/Thun_false-no-overflow.c 2.7 270 23
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 2.7 270 22
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 3.1 280 28
termination-crafted/aaron2_false-no-overflow.c 2.7 280 28
termination-crafted/aaron3_false-no-overflow.c 2.7 270 23
termination-crafted/easy2_false-no-overflow.c 900   13000 10000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 2.6 270 24
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 2.9 270 25
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 2.7 270 24
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 900   6200 11000
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 25
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 2.7 270 28
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 2.6 270 25
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900   4900 11000
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 2.6 270 21
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 900   2600 10000
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 2.8 270 23
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 22
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 2.9 290 23
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 25
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900   6300 9900
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 2.5 270 24
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900   600 12000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 2.9 280 27
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 2.9 270 25
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 3.9 290 33
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 4.0 290 40
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900   1200 13000
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 3.3 280 30
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 900   1400 9800
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 900   5100 9900
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 900   4300 11000
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 2.6 270 22
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 2.7 270 26
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 23
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 2.6 270 24
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 26
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 2.6 270 26
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 260 23
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 2.6 270 23
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 290 25
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 2.6 270 24
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 2.7 270 22
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 900   13000 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 2.8 270 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 2.7 280 26
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 2.6 270 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 2.8 270 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 2.6 270 21
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 2.8 270 26
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 2.8 270 26
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 900   13000 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 2.6 270 23
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 2.6 270 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 900   6200 10000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 910   620 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 2.9 280 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 2.7 280 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 2.7 270 23
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 2.8 270 23
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 2.7 270 25
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 2.7 270 23
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 2.8 270 22
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 2.7 270 23
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 2.6 270 23
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 2.7 270 25
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 2.6 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 2.7 270 24
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 2.7 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 2.6 280 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 2.7 290 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 2.8 280 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 2.6 270 24
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 2.6 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 2.6 280 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 2.6 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 2.6 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 2.6 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 2.8 290 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 2.7 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 2.6 260 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 2.7 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 2.7 280 21
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 2.6 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 2.6 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 2.6 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 2.8 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 2.6 260 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 2.6 260 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 2.8 270 24
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 2.6 260 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 2.8 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 2.6 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 2.7 270 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 2.6 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 2.7 270 24
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 2.6 270 22
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 2.7 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 2.7 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 2.7 260 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 3.2 310 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 2.7 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 2.7 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 2.8 270 22
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 2.7 260 25
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 2.8 270 21
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 2.8 270 26
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 2.6 270 23
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 2.7 280 24
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 3.2 290 26
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 2.7 270 26
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 2.8 270 24
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 2.7 280 26
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 2.8 280 24
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 3.0 280 26
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 3.2 280 27
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 900   2500 8200
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 3.1 310 28
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 2.5 260 23
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 2.6 270 26
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 2.8 270 26
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 2.6 270 22
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 2.9 290 24
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 2.6 270 26
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 2.7 270 26
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 2.7 270 27
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 2.9 270 25
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 2.9 270 25
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 2.8 270 24
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 2.7 270 25
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 2.7 270 23
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 2.7 270 23
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 2.7 280 24
termination-crafted-lit/cstrncmp_false-no-overflow.c 3.7 330 34
termination-crafted-lit/gcd1_false-no-overflow.c 2.6 270 20
termination-crafted-lit/joey_false-no-overflow.c 2.7 270 22
termination-crafted-lit/min_rf_false-no-overflow.c 2.8 270 26
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 850   15000 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 2.7 270 23
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2.7 260 23
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900   13000 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 100   1100 860
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900   6200 10000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900   540 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 59   480 780
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 2.8 270 24
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 2.8 270 23
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 2.9 280 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 3.9 280 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 2.8 260 25
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 2.8 270 25
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900   6900 11000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 2.8 270 25
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 2.8 270 24
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 900   8000 11000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 890   15000 11000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 900   4000 9100
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2.8 270 24
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900   13000 11000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 910   610 11000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 59   460 710
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 2.7 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 2.9 300 23
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 3.0 290 26
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 2.6 270 25
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 2.7 270 24
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 2.7 270 27
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 2.8 290 27
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 2.7 270 25
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 2.6 280 23
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 900   7100 10000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   560 11000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 2.6 270 23
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900   4000 9700
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 2.6 270 22
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 2.8 270 23
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 2.6 270 25
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900   6800 13000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 2.5 270 20
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 2.7 270 24
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   510 13000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 3.0 270 24
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 900   5300 10000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 2.6 270 26
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 2.7 270 24
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2.6 260 23
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 110   1000 790
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 2.5 270 21
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 2.6 270 25
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 2.7 270 23
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 2.6 260 23
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 900   4900 12000
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 4.1 290 39
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 2.8 270 26
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 2.6 270 24
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 900   8100 11000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 3.4 310 31
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 3.4 310 29
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 2.8 280 25
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 3.3 310 32
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 3.3 310 31
termination-crafted-lit/genady_true-termination_true-no-overflow.c 900   4500 11000
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 2.8 290 23
termination-numeric/Addition01_false-no-overflow.c 3.1 310 28
termination-numeric/Avg_true_false-no-overflow.c 2.6 270 24
termination-numeric/Binomial_true-termination_false-no-overflow.c 900   2000 8300
termination-numeric/Et1_true_false-no-overflow.c 2.6 270 21
termination-numeric/Et2_true_false-no-overflow.c 2.7 260 27
termination-numeric/Et3_true_false-no-overflow.c 2.6 270 21
termination-numeric/Et4_true_false-no-overflow.c 2.7 270 23
termination-numeric/MultCommutative_false-no-overflow.c 900   1600 11000
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 900   1600 7500
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 900   6500 10000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900   4300 11000
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 5.3 310 57
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 3.0 280 24
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900   1900 9300
termination-numeric/Parts_true-termination_true-no-overflow.c 900   2900 10000
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900   740 11000
termination-numeric/gcd01_true-termination_true-no-overflow.c 3.5 310 33
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 15   460 160
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 900   4400 9800
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900   4500 12000
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900   5700 11000
termination-numeric/twisted_true-termination_true-no-overflow.c 900   7800 11000
recursive/Addition02WithOverflowBug_false-no-overflow.c 2.8 280 25
recursive/Addition03_false-no-overflow.c 3.1 300 29
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 2.6 270 22
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 900   3600 12000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 900   4300 9600
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 900   4500 12000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 900   5700 10000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 900   5700 10000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900   5700 9100
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 2.8 270 24
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2.8 270 26
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 900   4100 10000
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 900   4400 9800
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 4.4 290 39
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 670   810 6100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 5.9 310 63
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 4.2 300 40
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 4.2 290 42
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 3.4 280 26
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 3.3 280 29
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 900   1500 10000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 900   1500 12000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 3.4 310 29
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 3.5 290 33
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 900   6800 9900
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 900   5000 12000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 900   4400 9800
recursive-simple/id_b3_o2_false-no-overflow.c 2.8 270 24
recursive-simple/id_b3_o5_false-no-overflow.c 2.8 280 23
recursive-simple/id_b5_o10_false-no-overflow.c 3.0 300 25
recursive-simple/sum_non_eq_false-no-overflow.c 2.9 270 20
recursive-simple/sum_non_false-no-overflow.c 2.7 270 26
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 3.0 270 28
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 3.0 290 30
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2.9 270 27
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2.8 270 23
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2.8 270 27
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 3.7 290 32
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 3.7 290 31
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 4.5 300 40
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 2.8 260 24
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 2.9 290 25
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 2.7 260 25
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 3.0 300 25
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 3.0 290 24
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 2.8 270 25
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 2.8 270 27
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2.8 270 23
bitvector/byte_add_1_false-no-overflow.i 5.9 320 55
bitvector/byte_add_2_false-no-overflow.i 6.4 330 55
bitvector/byte_add_false-no-overflow.i 6.8 350 57
bitvector/jain_1_false-no-overflow.i 2.8 280 29
bitvector/jain_2_false-no-overflow.i 2.9 290 24
bitvector/jain_4_false-no-overflow.i 2.9 280 29
bitvector/jain_5_false-no-overflow.i 900   3900 8100
bitvector/jain_6_false-no-overflow.i 2.9 290 26
bitvector/jain_7_false-no-overflow.i 2.8 280 24
bitvector/modulus_false-no-overflow.i 2.6 270 21
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 3.8 310 36
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 3.4 280 31
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 3.5 280 32
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2.8 280 25
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2.8 270 24
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2.7 270 25
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2.7 270 24
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2.5 270 23
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2.6 280 23
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2.6 270 26
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2.6 270 24
bitvector/jain_5_true-unreach-call_true-no-overflow.i 2.5 270 23
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2.6 270 26
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2.7 270 24
bitvector/modulus_true-unreach-call_true-no-overflow.i 2.7 270 25
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2.8 270 25
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 3.0 270 24
bitvector/parity_true-unreach-call_true-no-overflow.i 2.8 260 24
bitvector/sum02_false-unreach-call_true-no-overflow.i 2.8 270 24
bitvector/sum02_true-unreach-call_true-no-overflow.i 2.7 270 24
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 59000 400000 700000
    correct results 285 2000 82000 18000
        correct true 121 1300 36000 12000
        correct false 164 660 46000 5600
    correct-unconfimed results 10 38 2900 360
        correct-unconfirmed true 10 38 2900 360
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]