Tool CBMC Path 5.10 ()
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-04 22:45:10 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]
Options --graphml-witness witness.graphml
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .081 9.2 .43
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .095 10   .51
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .061 9.3 .79
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .062 8.9 .60
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .076 8.9 .56
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .063 9.1 .60
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .065 9.1 .55
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .064 8.7 .50
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .13  8.8 .41
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .058 9.4 .58
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i witness invalid (true) .045 7.3 .33
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .087 6.4 .37
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .095 7.0 .32
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .051 7.3 .37
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .054 7.1 .34
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .12  7.4 .37
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .087 9.0 .70
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .058 9.4 .58
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .067 9.2 .54
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .063 9.8 .48
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .062 10   .62
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .068 9.1 .60
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .068 9.4 .43
termination-crafted/Cairo_step2_false-no-overflow.c error (42) 880     110   11000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .075 9.5 .44
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .063 9.6 .54
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .12  9.1 .40
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .057 9.6 .59
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .068 9.2 .45
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .077 9.8 .42
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .066 8.9 .54
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .092 9.2 .36
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .13  8.9 .34
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .11  8.7 .47
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .066 10   .51
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .079 9.2 .34
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .070 9.6 .46
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .15  9.7 1.2 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .070 8.5 .39
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .067 8.9 .48
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (42) 880     100   9500   
termination-crafted/NonTerminationSimple5_false-no-overflow.c out of memory 860     15000   11000   
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .061 9.3 .58
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .058 9.2 .55
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .12  8.3 .30
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .068 9.3 .49
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .12  8.6 .33
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .13  8.1 .31
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .065 9.4 .43
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .080 9.5 .46
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .068 9.0 .35
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .074 8.8 .71
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .070 8.8 .43
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .16  8.6 .30
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .094 9.1 .54
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .067 9.0 .70
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .065 9.1 .61
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .082 8.8 .51
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .075 8.8 .49
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .072 8.9 .42
termination-crafted/easy2_false-no-overflow.c error (42) 880     160   11000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c witness invalid (true) .18  7.4 1.5 
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1300   12000   
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c error (42) 870     780   12000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     920   9600   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     200   12000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     190   11000   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .058 6.2 .47
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     170   11000   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     380   6000   
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     110   10000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     120   11000   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     220   10000   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870     350   11000   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     13000   11000   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error (134) .059 15   .52
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 140     15000   1800   
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870     4100   11000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870     5900   13000   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     170   11000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     5000   11000   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     5000   11000   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     500   7200   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     340   5600   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     500   6700   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     690   10000   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870     180   11000   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c error (42) 880     880   6500   
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     210   10000   
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870     8200   13000   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 850     15000   13000   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 520     15000   6900   
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c error (42) 880     160   9800   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 450     15000   5900   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     150   11000   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c witness invalid (true) .042 6.1 .29
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c witness invalid (true) .047 6.1 .24
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 180     15000   2800   
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     170   12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .12  8.0 .33
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .067 9.0 .56
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .067 9.2 .38
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .066 9.7 .59
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .072 9.2 .50
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .12  8.5 .37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c out of memory 310     15000   4600   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c error (42) 880     160   10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .12  7.8 .45
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .067 9.0 .46
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c out of memory 210     15000   3400   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c out of memory 330     15000   4200   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .061 9.3 .42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .068 8.9 .52
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .071 10   .47
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c error (42) 880     8100   12000   
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .070 9.0 .44
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .071 9.1 .46
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .10  8.6 .41
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .076 9.1 .48
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .055 9.4 .42
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .093 9.4 .36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .065 9.4 .67
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .068 8.9 .47
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .069 8.9 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .071 9.2 .44
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .075 9.6 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .067 9.2 .46
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .085 8.9 .40
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .15  7.8 .35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .077 8.3 .48
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .070 9.2 .51
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .064 8.6 .53
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .072 8.9 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .067 9.1 .53
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .087 8.8 .46
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .071 9.3 .56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .065 9.6 .49
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .074 9.1 .47
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .069 9.3 .47
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .13  8.6 .35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .070 9.8 .48
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .12  8.5 .32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .064 9.7 .62
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .060 9.6 .62
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .078 9.2 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .059 9.8 .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .066 9.2 .46
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .073 9.1 .41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .062 9.2 .47
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .080 9.0 .42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .072 9.1 .40
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .11  9.6 .36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .076 9.6 .40
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .069 9.2 .44
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .061 10   .59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .13  8.9 .34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .062 9.7 .49
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .061 9.1 .56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .064 9.6 .53
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .074 9.1 .46
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .064 9.0 .53
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .059 9.2 .62
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .077 8.7 .39
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .076 9.1 .36
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 110     4500   1300   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .075 9.6 .34
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c error (42) 880     1400   10000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .10  8.7 .44
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .060 9.5 .52
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .084 9.0 .34
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .066 9.1 .47
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .12  9.3 .30
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .066 9.2 .64
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .072 9.0 .45
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .063 9.2 .48
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .15  8.5 .36
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .063 9.3 .67
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .075 9.1 .59
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .13  8.0 .32
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .061 9.0 .47
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .066 9.6 .70
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .071 9.2 .45
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .087 8.9 .40
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c error (42) 880     12000   11000   
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c error (42) 880     13000   12000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c error (42) 880     13000   12000   
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .071 9.0 .41
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .087 8.8 .32
termination-crafted-lit/cstrncmp_false-no-overflow.c error (134) .049 8.5 .37
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .068 9.0 .39
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .065 9.4 .53
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .065 9.2 .55
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c out of memory 560     15000   8000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c error (42) 880     15000   13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c out of memory 190     15000   2900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c error (42) 880     220   10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c error (42) 870     8000   14000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c out of memory 340     15000   4600   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c out of memory 330     15000   3800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c out of memory 340     15000   4800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c out of memory 380     15000   4300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c out of memory 290     15000   4500   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c error (42) 880     8800   12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c error (42) 870     5100   11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c error (42) 870     4400   13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c error (42) 880     1900   13000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c error (42) 870     440   12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c error (42) 880     4000   12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c error (42) 880     4100   14000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c error (42) 870     4900   12000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c error (42) 870     2500   10000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c error (42) 880     200   11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c out of memory 190     15000   2200   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c error (42) 880     210   10000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c out of memory 330     15000   4200   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c out of memory 340     15000   4900   
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c error (42) 880     410   7000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c error (42) 870     180   10000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c error (42) 880     100   11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c error (42) 880     14000   13000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c error (42) 880     11000   10000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c out of memory 540     15000   7200   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c error (42) 880     9700   11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c error (42) 870     14000   11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c out of memory 300     15000   4800   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .26  7.5 1.7 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 870     9800   14000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c out of memory 790     15000   11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c error (42) 880     200   12000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c error (42) 870     170   9400   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c error (42) 880     200   10000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c error (42) 870     200   11000   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c error (42) 870     4800   11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c out of memory 830     15000   13000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c error (42) 880     4400   12000   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c error (42) 880     3100   12000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (42) 880     13000   13000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (42) 880     13000   11000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c error (42) 880     6300   11000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c out of memory 500     15000   6500   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c witness invalid (true) .39  15   5.1 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c error (42) 870     4800   13000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c error (42) 870     150   9800   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c error (42) 870     4800   13000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c error (42) 880     14000   12000   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c out of memory 440     15000   5000   
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c error (42) 880     1400   8800   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c error (42) 880     200   10000   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c out of memory 370     15000   4800   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c error (42) 880     150   12000   
termination-crafted-lit/aviad_true-termination_true-no-overflow.c error (42) 880     3200   9300   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (134) .051 8.1 .30
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (134) .050 6.8 .25
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (134) .050 7.2 .34
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (134) .047 8.2 .41
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (134) .055 8.1 .38
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 4.6   170   64   
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (134) .050 7.9 .27
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .093 8.7 .40
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .067 9.6 .58
termination-numeric/Binomial_true-termination_false-no-overflow.c out of memory 430     15000   5400   
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .069 9.9 .45
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .058 9.4 .59
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .068 9.4 .50
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .066 9.0 .58
termination-numeric/MultCommutative_false-no-overflow.c error (42) 870     6500   13000   
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 2.9   67   44   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (42) 870     10000   13000   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (42) 880     280   11000   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (42) 880     12000   11000   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (42) 880     350   9100   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 25     79   310   
termination-numeric/Parts_true-termination_true-no-overflow.c error (42) 880     14000   11000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (42) 880     930   7900   
termination-numeric/gcd01_true-termination_true-no-overflow.c error (42) 880     12000   11000   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 1.4   16   22   
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2.5   16   38   
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (42) 880     500   11000   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (42) 880     500   11000   
termination-numeric/twisted_true-termination_true-no-overflow.c error (42) 870     5100   11000   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .069 9.2 .52
recursive/Addition03_false-no-overflow.c false(no-overflow) .066 9.5 .47
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .12  8.8 .31
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 880     10000   12000   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     10000   11000   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 870     11000   12000   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 880     11000   11000   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     3600   11000   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (42) 870     3600   12000   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     7100   11000   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c witness invalid (true) .054 6.7 .48
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     280   10000   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     280   12000   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 880     13000   11000   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .19  8.1 1.1 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     13000   12000   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     13000   11000   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     13000   12000   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 870     6200   12000   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     6300   13000   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 870     6100   10000   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 860     15000   12000   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     12000   8100   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 870     6900   11000   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     14000   13000   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2.5   16   35   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2.6   16   32   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .088 8.6 .38
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .066 9.6 .50
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .14  8.1 .31
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .068 9.1 .40
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .061 9.8 .64
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     550   10000   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     550   11000   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 870     550   10000   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     540   9700   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     540   11000   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     380   10000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     380   12000   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 870     390   10000   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c error (42) 870     790   10000   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     790   12000   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     780   10000   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     790   11000   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     800   9100   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     790   9800   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     730   10000   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     720   9000   
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .30  12   3.1 
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .29  12   3.3 
bitvector/byte_add_false-no-overflow.i false(no-overflow) .68  24   9.0 
bitvector/jain_1_false-no-overflow.i false(no-overflow) .065 9.0 .37
bitvector/jain_2_false-no-overflow.i false(no-overflow) .067 9.3 .48
bitvector/jain_4_false-no-overflow.i false(no-overflow) .10  9.2 .46
bitvector/jain_5_false-no-overflow.i out of memory 190     15000   2800   
bitvector/jain_6_false-no-overflow.i false(no-overflow) .084 9.4 .48
bitvector/jain_7_false-no-overflow.i false(no-overflow) .075 9.1 .49
bitvector/modulus_false-no-overflow.i false(no-overflow) .061 9.7 .69
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .34  12   5.1 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .35  14   4.3 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 1.5   42   21   
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .24  8.4 2.4 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .72  21   9.0 
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .76  21   11   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .073 6.9 .48
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i witness invalid (true) .11  6.4 .89
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i out of memory 110     15000   1700   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i out of memory 120     15000   1700   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i out of memory 120     15000   1600   
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 190     15000   2800   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i out of memory 130     15000   1800   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i out of memory 130     15000   1600   
bitvector/modulus_true-unreach-call_true-no-overflow.i error (42) 880     12000   8800   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .10  6.4 .77
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1.4   71   22   
bitvector/parity_true-unreach-call_true-no-overflow.i witness invalid (true) .41  8.1 5.4 
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 880     250   6400   
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 870     260   8800   
psyco/psyco_abp_1_false-no-overflow.c out of memory 840     15000   9300   
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 120000 1100000 1600000
    correct results 178 140 6400 1700
        correct true 19 18 400 250
        correct false 159 120 6000 1400
    correct-unconfimed results 3 27 160 330
        correct-unconfirmed true 3 27 160 330
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]