Tool ESBMC version 6.0.0 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:03:31 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.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) .078 26 1.1 
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .090 26 .99
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .083 26 1.0 
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .077 26 .92
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .095 26 .72
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .084 26 .89
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .080 26 .89
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .077 26 .87
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .090 26 1.4 
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .10  26 .82
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .085 26 .87
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .084 26 .95
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .081 26 .84
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .082 26 1.2 
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .084 26 .83
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .083 26 1.2 
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .14  26 1.6 
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .080 26 1.1 
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .10  26 .76
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .078 26 .92
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .085 26 .80
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .11  26 1.3 
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .090 26 .97
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900     480 12000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .11  26 1.1 
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .081 26 .80
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .13  26 1.3 
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .13  26 2.2 
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .086 26 .74
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .092 26 1.0 
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .11  26 1.2 
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .087 26 1.0 
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .10  26 1.1 
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .080 26 .86
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .090 26 .81
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .10  26 .74
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .084 26 .73
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .11  26 1.3 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .084 26 .75
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .077 26 .95
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900     480 11000   
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .081 26 .92
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .082 26 .95
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .099 26 .83
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .083 26 .85
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .10  26 .79
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .10  26 1.3 
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .11  26 .74
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .089 26 .79
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .078 26 .89
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .10  26 1.1 
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .092 26 1.1 
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .10  26 1.3 
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .10  26 1.3 
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .13  26 1.0 
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .098 26 .84
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .083 26 .88
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .11  26 1.0 
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .14  26 1.3 
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .12  26 .96
termination-crafted/easy2_false-no-overflow.c timeout 900     1100 11000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .088 26 1.0 
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1800 13000   
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c timeout 900     1600 11000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1200 11000   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     140 11000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     220 11000   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .12  26 1.3 
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1500 10000   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     890 13000   
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     560 10000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     480 11000   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     930 11000   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     780 11000   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     15000 11000   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900     5900 13000   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     15000 13000   
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     160 11000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     6400 6900   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1200 13000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     12000 7700   
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 5200   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4800 4700   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     4800 8100   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     6000 6000   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     15000 8700   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 900     2200 13000   
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900     190 10000   
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     470 11000   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     500 11000   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     240 12000   
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 900     870 11000   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     490 14000   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     890 11000   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .082 26 .87
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 280     15000 4100   
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .60  26 9.3 
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900     1100 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .14  26 1.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .14  26 1.6 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .11  26 1.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .11  26 1.2 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .10  26 1.1 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .088 26 .95
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .086 26 .85
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900     1100 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .11  26 .80
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .10  26 .65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900     1100 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900     130 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .088 26 .91
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .11  26 1.5 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .11  26 .87
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .083 26 .96
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .12  26 .97
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .25  27 2.9 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .11  26 1.1 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .11  26 1.2 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .10  26 1.1 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .11  26 1.0 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .11  26 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .080 26 .93
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .085 26 .96
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .11  26 .83
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .079 26 .83
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .080 26 .85
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .082 26 .94
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .078 26 .94
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .089 26 .87
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .099 26 1.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .095 26 .94
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .12  26 1.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .085 26 .97
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .10  26 .86
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .095 26 1.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .084 26 .83
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .16  26 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .10  26 1.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .11  26 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .11  26 1.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .11  26 .83
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .081 26 .80
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .083 26 .88
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .092 26 .91
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .12  26 .98
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .11  26 .96
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .084 26 .94
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .10  26 .80
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .11  26 .92
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .10  26 1.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .087 26 .89
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .081 26 .87
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .086 26 .94
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .098 26 .87
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .11  26 .78
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .11  26 .89
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .11  26 .87
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .16  26 2.6 
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .085 26 .89
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .090 26 .99
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .086 26 .98
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .10  26 .94
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .084 26 .83
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .082 26 1.0 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .10  26 1.4 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .091 26 .78
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .083 26 1.0 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .11  26 .75
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .097 26 .83
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .083 26 .89
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .10  26 .82
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .10  26 .72
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .089 26 .99
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .080 26 .86
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .10  26 .84
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .082 26 .89
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .11  26 .92
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .12  26 .77
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .10  26 .84
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .12  26 1.3 
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .084 26 .95
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .10  26 1.6 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .10  26 .84
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .083 26 .85
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .10  26 .70
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .13  26 1.8 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .085 26 .82
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .11  26 1.2 
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .11  26 1.1 
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .077 26 .91
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .10  26 1.4 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     650 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 900     730 9800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .63  26 6.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900     1100 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 900     340 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900     870 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900     130 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .16  26 1.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 900     270 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 900     220 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 900     310 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout 900     1300 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 900     320 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 900     130 13000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900     380 11000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900     100 12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900     110 12000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 900     380 14000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900     370 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900     840 10000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .60  26 8.1 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900     1100 13000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900     130 14000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .17  26 2.0 
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 900     1400 12000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout 900     280 11000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 900     220 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 900     610 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 900     540 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 900     770 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 900     140 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 900     200 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 900     180 11000   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .39  26 4.8 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900     270 11000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 900     1100 10000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900     1200 10000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 900     600 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 900     1200 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 900     200 13000   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900     880 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 900     210 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 900     230 11000   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900     260 14000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 620     15000 6300   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 530     15000 5000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 900     180 11000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 900     660 11000   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .21  26 2.5 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 900     330 12000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 900     890 10000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 900     390 13000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 900     550 12000   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 900     350 10000   
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 900     3500 11000   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 900     810 13000   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 900     480 12000   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout 900     450 13000   
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 5.3   33 61   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 900     5600 10000   
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 900     1800 11000   
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout 900     2600 11000   
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 900     2100 9500   
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 900     2000 8900   
termination-crafted-lit/genady_true-termination_true-no-overflow.c out of memory 860     15000 8300   
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout 900     1800 12000   
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .080 26 .92
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .11  26 1.3 
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 7.6   77 93   
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .13  26 1.2 
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .12  26 1.3 
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .10  26 1.3 
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .14  26 1.6 
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .21  26 2.0 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 14     50 180   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 460     15000 5800   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 900     1100 9200   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 900     8800 7900   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 900     960 10000   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 81     160 1100   
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900     2800 11000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 900     200 11000   
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout 900     890 7800   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .19  26 2.7 
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1.8   27 27   
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 900     1200 12000   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 900     1200 9700   
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900     1200 11000   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .12  26 1.1 
recursive/Addition03_false-no-overflow.c false(no-overflow) .091 26 .85
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .088 26 .91
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 460     15000 4800   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 480     15000 5800   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 470     15000 5300   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 470     15000 5300   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 840     15000 7900   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 840     15000 8200   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 840     15000 9300   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .086 26 1.1 
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     1100 12000   
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 10000   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .13  26 1.4 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 6700   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 6200   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 900     8800 6700   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 900     6400 8000   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 900     6400 7400   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 760     15000 7400   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 230     15000 2600   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     890 8100   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 900     1200 7400   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 900     13000 9100   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1.8   27 28   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1.8   27 24   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .093 26 .93
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .11  26 .83
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .11  26 .77
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .092 26 1.4 
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .085 26 1.2 
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 11000   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 11000   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 9400   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 8900   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 900     1100 10000   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 900     520 12000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 900     520 13000   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 900     530 13000   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 9600   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 11000   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 11000   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 11000   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c timeout 900     1000 9200   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 900     990 11000   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 900     980 9600   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 900     980 11000   
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .11  27 1.2 
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .12  27 1.0 
bitvector/byte_add_false-no-overflow.i false(no-overflow) .14  27 2.2 
bitvector/jain_1_false-no-overflow.i false(no-overflow) .086 26 .87
bitvector/jain_2_false-no-overflow.i false(no-overflow) .083 26 1.1 
bitvector/jain_4_false-no-overflow.i false(no-overflow) .079 26 .84
bitvector/jain_5_false-no-overflow.i out of memory 830     15000 10000   
bitvector/jain_6_false-no-overflow.i false(no-overflow) .088 26 .98
bitvector/jain_7_false-no-overflow.i false(no-overflow) .090 26 1.0 
bitvector/modulus_false-no-overflow.i false(no-overflow) .11  26 .79
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .13  27 1.6 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .13  27 1.4 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .17  27 2.1 
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .52  28 7.9 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 9.2   42 140   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 9.2   43 110   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .084 26 .84
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .095 26 1.2 
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1400 11000   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 900     870 9800   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 900     780 8500   
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 900     13000 11000   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 900     800 10000   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 900     1200 9500   
bitvector/modulus_true-unreach-call_true-no-overflow.i true 76     280 960   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .12  26 .93
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .13  26 1.6 
bitvector/parity_true-unreach-call_true-no-overflow.i true .76  26 8.7 
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900     1600 10000   
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900     1600 10000   
psyco/psyco_abp_1_false-no-overflow.c timeout 900     3700 11000   
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 140000     520000 1600000   
    correct results 198 68     5300 840   
        correct true 30 30     820 390   
        correct false 168 38     4400 440   
    correct-unconfimed results 6 160     560 2100   
        correct-unconfirmed true 5 160     530 2100   
        correct-unconfirmed false 1 .091 26 .78
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]