Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux
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-02 18:23:42 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
Options -s kinduction
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .11  28 .83
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .092 28 .97
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .079 28 1.1 
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .11  28 .82
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .081 28 1.0 
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .083 28 .90
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .11  28 .76
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .10  28 .97
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .12  28 .58
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .082 28 .83
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .081 26 .77
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .089 27 .77
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .080 27 .76
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .088 26 .72
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .075 26 .84
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .21  28 1.6 
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .41  28 4.0 
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .20  28 1.7 
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .19  28 2.4 
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .17  28 2.2 
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .24  28 3.2 
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .35  28 3.3 
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .18  28 1.5 
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900     390 11000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .24  28 2.3 
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .24  28 1.9 
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .42  28 3.4 
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .37  28 4.0 
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .20  28 1.8 
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .41  28 3.9 
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .24  28 3.3 
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .15  28 1.9 
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .23  28 2.4 
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .18  28 1.9 
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .14  28 1.2 
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .15  28 1.1 
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .26  28 1.7 
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .12  28 1.2 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .16  28 1.2 
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .22  28 2.1 
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     390 12000   
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .12  28 1.5 
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .20  28 1.6 
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .16  28 1.7 
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .13  28 1.3 
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .27  28 2.1 
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .27  28 2.8 
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .19  28 1.9 
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .11  28 1.5 
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .21  28 2.2 
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .21  28 1.9 
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .29  28 2.9 
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .20  28 1.9 
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .21  28 1.9 
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .32  28 2.5 
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .27  28 2.4 
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .28  28 1.8 
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .57  28 5.7 
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .34  28 3.3 
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .33  28 2.9 
termination-crafted/easy2_false-no-overflow.c timeout 900     880 11000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .074 26 .79
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true .12  26 .57
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true .072 26 .78
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true .089 26 .78
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true .10  26 .85
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true .089 26 1.1 
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .096 26 .95
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1300 11000   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown .033 15 .31
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     450 12000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     400 11000   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true .075 26 .77
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true .082 26 .86
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c true .11  26 .96
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900     5900 11000   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true .082 26 .66
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     150 11000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     9000 9500   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1000 10000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 720     15000 7600   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 670     15000 7800   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4800 12000   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 770     15000 6700   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 680     15000 6600   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     12000 7200   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     12000 10000   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true .079 26 .74
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true .072 26 .89
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true .10  26 .62
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true .076 26 .86
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true .12  26 1.1 
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 900     720 11000   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true .12  26 .86
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true .11  26 .72
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .093 26 .73
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .10  26 .68
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .11  26 .66
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     890 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .41  29 4.6 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .56  30 6.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .26  28 3.2 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .35  28 2.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .38  28 3.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .38  28 2.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .36  28 3.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900     890 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .36  28 3.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .14  28 1.1 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900     1000 9700   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900     120 9600   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .13  28 1.5 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .26  28 2.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .35  28 3.7 
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .45  28 3.7 
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .26  28 2.5 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .69  32 6.7 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .31  28 2.9 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .29  28 3.4 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .33  28 2.9 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .47  29 4.2 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .42  28 4.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .14  28 1.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .13  28 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .12  28 1.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .16  28 1.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .14  28 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .19  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .29  28 3.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .30  28 2.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .21  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .22  28 2.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .24  28 2.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .27  28 2.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .21  28 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .24  28 3.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .25  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .37  29 4.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .31  28 2.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .25  28 2.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .25  28 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .17  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .23  28 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .16  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .27  28 2.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .22  28 3.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .22  28 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .20  28 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .34  28 3.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .37  28 4.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .35  28 3.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .27  28 2.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .22  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .23  28 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .29  28 2.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .25  28 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .26  28 2.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .32  28 3.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .23  28 2.5 
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .41  28 3.3 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .30  28 3.1 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .49  28 4.5 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .22  28 2.6 
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .25  28 2.2 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .16  28 1.7 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .25  28 2.5 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .18  28 1.8 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .18  28 2.1 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .25  28 2.3 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .12  28 1.7 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .19  28 2.2 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .20  28 1.5 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .21  28 1.8 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .19  28 2.4 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .20  28 1.9 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .23  28 3.1 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .26  28 2.9 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .21  28 1.8 
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .22  28 1.7 
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .21  28 1.7 
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .25  28 2.2 
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .43  28 3.6 
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .24  28 2.5 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .30  28 2.9 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .34  28 3.0 
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .34  28 2.9 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .32  29 3.0 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .15  28 1.4 
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .37  29 4.5 
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .26  28 3.7 
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .14  28 1.3 
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .29  28 3.5 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     590 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true .12  26 .65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .074 26 .91
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     900 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 900     310 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true .23  27 2.6 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     130 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .25  26 3.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true .077 26 .86
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true .12  26 1.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true .14  26 1.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true .12  26 .78
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true .091 26 .71
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 900     120 13000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     310 11000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     99 10000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     99 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true .16  26 1.5 
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     350 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900     670 11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .11  26 .68
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     900 11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     120 11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .28  26 3.6 
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .077 26 .80
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true .11  26 .75
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true .11  26 1.1 
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true .11  26 .74
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true .098 26 .90
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true .092 26 .96
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true .18  26 1.7 
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true .11  26 .95
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true .11  26 1.1 
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .46  26 6.3 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     240 11000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true .079 26 .74
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     990 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true .087 26 .93
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 900     940 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true .078 26 .88
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     760 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true .10  26 1.1 
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true .11  26 1.3 
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     230 12000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 690     15000 7100   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 890     15000 7600   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true .29  26 3.3 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true .12  26 .70
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .11  26 .59
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 900     310 13000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true .075 26 .86
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true .12  26 1.2 
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true .083 26 .95
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .096 26 .98
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true .085 26 .75
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true .11  26 .65
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true .14  26 1.0 
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true .10  26 1.0 
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 6.1   33 77   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true .19  27 1.7 
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true .14  27 1.9 
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true .15  27 1.3 
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true .16  27 1.5 
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true .16  27 1.7 
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 900     11000 10000   
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true .12  27 1.4 
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .20  28 1.5 
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .17  28 1.8 
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 5.5   64 71   
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .24  28 2.0 
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .27  28 2.7 
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .22  28 2.1 
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .44  28 3.5 
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .43  29 4.7 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 23     57 310   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 620     15000 6600   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 900     1100 12000   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 900     11000 11000   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 900     900 9800   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 110     170 1200   
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900     3700 13000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 900     190 10000   
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout 900     1600 8300   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .22  26 2.8 
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2.0   27 27   
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 900     1100 9900   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 900     1100 9700   
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     1000 9000   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .16  28 3.3 
recursive/Addition03_false-no-overflow.c false(no-overflow) .18  28 1.8 
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .12  28 1.4 
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 620     15000 7700   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 630     15000 7700   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 640     15000 7100   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 610     15000 8800   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 580     15000 5800   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 580     15000 7200   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 570     15000 6000   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .073 26 .77
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     1100 10000   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 900     1100 10000   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 900     4400 8600   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .16  26 1.4 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 900     11000 11000   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 900     11000 9300   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 900     11000 8600   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 900     9100 10000   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 900     9000 8700   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 380     15000 3900   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 450     15000 6100   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     1600 9200   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 900     2300 8300   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     5300 6400   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2.0   27 29   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2.0   28 27   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .13  28 1.6 
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .17  28 1.2 
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .13  28 1.4 
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .21  28 1.7 
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .22  28 1.8 
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 11000   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 12000   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 10000   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 10000   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 9900   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 900     470 11000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     470 11000   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     470 11000   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 11000   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 9600   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 11000   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 12000   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 11000   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 9700   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 10000   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 12000   
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1.1   29 11   
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1.1   29 9.6 
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1.4   29 9.9 
bitvector/jain_1_false-no-overflow.i false(no-overflow) .10  28 .83
bitvector/jain_2_false-no-overflow.i false(no-overflow) .13  28 .87
bitvector/jain_4_false-no-overflow.i false(no-overflow) .11  28 1.2 
bitvector/jain_5_false-no-overflow.i timeout 900     12000 9600   
bitvector/jain_6_false-no-overflow.i false(no-overflow) .14  28 1.2 
bitvector/jain_7_false-no-overflow.i false(no-overflow) .13  28 1.1 
bitvector/modulus_false-no-overflow.i false(no-overflow) .18  28 1.6 
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .098 27 1.0 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .12  27 1.0 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .10  27 1.1 
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .35  27 4.7 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .29  26 3.0 
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .26  27 3.2 
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .15  26 1.7 
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .078 26 .74
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true .079 26 .77
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true .12  26 .76
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true .094 26 .96
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .089 26 .74
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true .11  26 .88
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true .080 26 .80
bitvector/modulus_true-unreach-call_true-no-overflow.i true .14  26 1.2 
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .11  26 .90
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .087 26 .75
bitvector/parity_true-unreach-call_true-no-overflow.i true .10  26 .84
bitvector/sum02_false-unreach-call_true-no-overflow.i true .093 26 .77
bitvector/sum02_true-unreach-call_true-no-overflow.i true .074 26 .89
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 77000 440000 890000
    correct results 259 89 7200 990
        correct true 90 17 2400 180
        correct false 169 72 4800 800
    correct-unconfimed results 8 110 350 1300
        correct-unconfirmed true 8 110 350 1300
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]