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 06:23:16 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
Options -s incr
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .12  28 .72
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .082 28 .93
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .082 28 .98
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .097 28 .70
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .12  28 .81
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .092 28 1.1 
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .11  28 .77
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .11  28 .77
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .083 28 .88
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .080 28 1.0 
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .072 26 .92
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .088 27 .89
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .072 26 .96
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .079 26 .90
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .073 26 1.0 
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .15  28 2.1 
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .36  28 2.9 
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .16  28 1.6 
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .15  28 1.9 
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .19  28 1.8 
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .23  28 2.0 
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .22  28 2.1 
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .17  28 1.8 
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900     390 10000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .14  28 1.4 
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .22  28 1.9 
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .32  28 2.6 
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .32  28 3.1 
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .18  28 1.7 
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .23  28 2.1 
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .32  28 2.4 
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .17  28 1.7 
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .24  28 1.6 
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .13  28 1.3 
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .12  28 1.5 
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .13  28 1.4 
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .13  28 1.1 
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .12  28 1.2 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .13  28 1.3 
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .16  28 1.8 
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     400 12000   
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .13  28 1.1 
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .13  28 1.6 
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .15  28 1.2 
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .12  28 1.3 
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .19  28 1.9 
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .26  28 2.2 
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .16  28 1.7 
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .13  28 1.6 
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .12  28 1.2 
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .17  28 2.5 
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .20  28 2.0 
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .19  28 2.0 
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .17  28 1.9 
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .29  28 2.2 
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .18  28 1.6 
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .17  28 1.5 
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .55  28 4.4 
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .25  28 2.3 
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .26  28 2.5 
termination-crafted/easy2_false-no-overflow.c timeout 900     890 11000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .087 26 .89
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1600 11000   
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout 900     1500 14000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1100 11000   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     130 10000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     190 12000   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .12  26 1.2 
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1300 9700   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown .056 15 .25
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     440 11000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     400 9700   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     760 11000   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     630 13000   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 750     15000 11000   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900     5900 11000   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     11000 9700   
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     150 12000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     6400 7300   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1000 11000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     12000 6500   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     12000 6200   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4900 6300   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4900 6800   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4800 5200   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     6100 6000   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 890     15000 7700   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 900     2100 11000   
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     170 11000   
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     380 12000   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     400 9700   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     220 12000   
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 timeout 900     410 14000   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     740 11000   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .069 26 .84
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 290     15000 4400   
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .61  26 8.6 
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     900 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .29  28 2.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .29  28 3.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .24  28 2.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .27  28 2.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .23  28 1.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .25  28 2.2 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .20  28 1.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900     890 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .27  28 2.4 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .13  28 1.4 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900     1100 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900     120 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .15  28 1.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .22  28 2.5 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .27  28 2.4 
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .28  28 2.2 
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .24  28 2.2 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .42  29 4.2 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .27  28 2.6 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .25  28 2.7 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .30  28 2.6 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .37  28 4.0 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .31  28 3.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .12  28 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .11  28 1.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .12  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .11  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .13  28 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .18  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .17  28 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .17  28 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .17  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .16  28 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .20  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .18  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .20  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .21  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .18  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .29  28 3.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .26  28 2.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .19  28 2.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .19  28 2.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .17  28 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .16  28 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .18  28 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .18  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .18  28 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .17  28 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .17  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .25  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .25  28 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .26  28 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .24  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .23  28 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .20  28 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .23  28 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .20  28 1.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .22  28 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .31  28 2.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .23  28 2.1 
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .28  28 2.2 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .28  28 2.7 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .28  28 2.3 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .24  28 2.0 
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .21  28 1.9 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .19  28 1.5 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .20  28 1.9 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .18  28 1.5 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .19  28 1.6 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .22  28 1.9 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .14  28 1.3 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .18  28 1.6 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .18  28 1.6 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .17  28 1.6 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .20  28 1.5 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .17  28 1.8 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .17  28 1.7 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .15  28 1.9 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .19  28 1.7 
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .19  28 1.5 
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .19  28 1.8 
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .19  28 1.9 
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .27  28 2.5 
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .28  28 2.6 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .24  28 2.5 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .29  28 2.4 
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .25  28 2.1 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .24  28 2.3 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .15  28 1.3 
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .34  29 2.8 
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .29  28 2.2 
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .13  28 1.3 
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .27  28 2.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     620 9300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 900     600 9700   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .62  26 7.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     900 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 900     310 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     870 9800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     130 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .18  26 1.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 900     240 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 900     190 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 900     250 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout 900     1100 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 900     280 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 900     120 12000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     310 13000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     110 12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     110 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 900     340 12000   
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 9900   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .63  26 7.4 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     900 13000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     130 10000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .16  26 2.2 
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 900     1200 12000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout 900     220 11000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 900     190 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 900     520 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 900     460 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 900     680 9900   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 900     140 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 900     180 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 900     160 12000   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .41  26 4.8 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     230 10000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 900     900 10000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     990 12000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 900     490 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 900     950 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 900     190 10000   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     800 9500   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 900     190 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 900     200 11000   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     250 14000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 590     15000 7100   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 510     15000 5600   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 900     180 13000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 900     560 13000   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .20  26 2.5 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 900     320 11000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 900     740 9600   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 900     350 12000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 900     470 10000   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 900     300 9900   
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 900     3600 12000   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 900     670 10000   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 900     420 12000   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout 900     400 9900   
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 5.7   32 72   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 900     5700 10000   
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 900     1400 9900   
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout 900     2900 9000   
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 900     1900 11000   
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 900     1800 8300   
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 900     12000 8100   
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout 900     1800 11000   
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .17  28 1.6 
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .18  28 1.8 
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 8.0   80 110   
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .20  28 2.0 
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .22  28 2.2 
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .19  28 1.9 
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .39  28 3.6 
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .30  28 2.8 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 16     51 180   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 460     15000 4900   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 900     1100 11000   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 900     8800 6500   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 900     900 10000   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 84     160 1000   
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900     2900 13000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 900     190 9600   
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout 900     890 8600   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .22  26 2.2 
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1.9   28 24   
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 900     1100 10000   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 900     1200 12000   
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     1200 12000   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .22  28 1.8 
recursive/Addition03_false-no-overflow.c false(no-overflow) .17  28 1.7 
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 440     15000 5400   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 450     15000 5100   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 460     15000 5000   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 450     15000 4700   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 810     15000 9200   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 840     15000 8100   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 830     15000 9000   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .081 26 .85
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 13000   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 900     8800 7500   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .15  26 1.4 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 7000   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 6700   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 7100   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 900     6400 7800   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 900     6300 7100   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 700     15000 6700   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 220     15000 2400   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     890 8600   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 900     1200 9200   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     13000 10000   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1.9   28 25   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1.9   27 24   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .16  28 .91
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .13  28 1.3 
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .15  28 1.1 
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) .18  28 1.9 
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 9500   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 9200   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 9500   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1200 9500   
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     460 11000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     460 11000   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     470 12000   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 9900   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 8700   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 10000   
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 10000   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 9300   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 9100   
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) .98  29 7.9 
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1.3   29 12   
bitvector/jain_1_false-no-overflow.i false(no-overflow) .080 28 1.0 
bitvector/jain_2_false-no-overflow.i false(no-overflow) .11  28 .88
bitvector/jain_4_false-no-overflow.i false(no-overflow) .088 28 .91
bitvector/jain_5_false-no-overflow.i timeout 900     12000 8900   
bitvector/jain_6_false-no-overflow.i false(no-overflow) .12  28 .81
bitvector/jain_7_false-no-overflow.i false(no-overflow) .091 28 1.1 
bitvector/modulus_false-no-overflow.i false(no-overflow) .16  28 2.0 
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .13  27 1.7 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .14  27 1.6 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .21  27 2.3 
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .56  29 7.4 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 9.9   43 110   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 9.9   43 120   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .12  26 .72
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .11  26 .96
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1200 11000   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 900     790 10000   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 900     730 9800   
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 900     11000 10000   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 900     730 8900   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1000 12000   
bitvector/modulus_true-unreach-call_true-no-overflow.i true 74     290 910   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .092 26 .98
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .11  26 1.0 
bitvector/parity_true-unreach-call_true-no-overflow.i true .82  26 9.4 
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900     1400 9700   
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900     1400 11000   
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 130000 500000 1500000
    correct results 197 92 5600 1000
        correct true 28 32 780 370
        correct false 169 60 4800 630
    correct-unconfimed results 7 160 590 2000
        correct-unconfirmed true 7 160 590 2000
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]