Tool CBMC
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:48:40 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) .074 9.2 .62
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .062 9.3 .57
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .12  9.4 .42
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .059 9.7 .60
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .061 9.7 .55
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .068 9.8 .55
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .071 9.7 .53
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .062 9.8 .69
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .15  7.6 .33
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .064 9.6 .51
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .078 6.4 .32
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .069 5.9 .30
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .052 6.5 .38
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .048 7.4 .47
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .059 6.4 .40
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .077 9.2 .44
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .091 9.2 .80
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .095 9.9 .91
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .067 9.8 .48
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .083 9.4 .42
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .080 9.4 .56
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .10  9.4 .97
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .12  8.4 .28
termination-crafted/Cairo_step2_false-no-overflow.c error (42) 880     4500   4100   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .086 9.4 .73
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .078 8.9 .49
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .071 9.4 .61
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .081 9.6 .69
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .057 9.5 .46
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .074 9.9 .65
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .071 9.6 .62
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .074 9.3 .47
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .071 11   .50
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .084 9.7 .84
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .065 9.9 .59
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .066 9.4 .70
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .089 9.3 .51
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .14  9.9 1.7 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .075 9.0 .55
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .091 8.4 .33
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (42) 880     4400   4400   
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .089 9.1 .39
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .076 10   .41
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .077 9.6 .51
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .072 9.4 .43
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .077 9.7 .47
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .073 9.5 .58
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .078 9.5 .65
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .095 9.0 .52
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .072 8.7 .33
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .066 9.5 .51
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .11  9.2 .49
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .076 10   .50
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .10  9.7 .38
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .078 9.3 .50
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .078 10   .46
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .075 9.5 .52
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .14  10   .63
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .086 9.3 .45
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .071 9.4 .51
termination-crafted/easy2_false-no-overflow.c error (42) 880     2200   4800   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .13  8.2 1.5 
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     2800   4600   
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c error (42) 880     3100   5000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4600   4200   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4300   5000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     4100   4200   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .061 6.5 .41
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     2500   5100   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     6800   6300   
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4100   4500   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4500   4800   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     3200   5000   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     3600   6500   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 52     13000   710   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c out of memory 55     13000   680   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 180     15000   2200   
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1400   7600   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1600   3700   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     3100   3100   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     220   3700   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     220   2900   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     460   3600   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     320   3500   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     460   4500   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870     860   5300   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4200   6800   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c error (42) 880     2300   10000   
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 880     4700   4800   
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1200   8500   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1200   9700   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     1800   9400   
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c error (42) 880     4500   4000   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     2100   7200   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     4800   4300   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .056 7.0 .26
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .053 6.8 .34
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 1.6   50   21   
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 880     2300   4300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .077 10   .63
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .10  9.7 1.1 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .079 9.3 .60
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .075 9.6 .51
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .084 9.1 .79
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .13  9.4 .43
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .081 9.7 .68
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c error (42) 880     2400   4300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .067 9.9 .70
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .062 9.3 .62
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c error (42) 880     1500   5900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c error (42) 880     1300   9300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .069 9.8 .61
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .071 9.6 .63
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .14  8.9 .48
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .071 9.6 .64
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .079 9.5 .73
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .16  15   1.1 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .091 9.4 .48
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .098 9.7 .41
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .080 9.5 .48
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .11  9.7 .66
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .14  9.3 .56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .13  8.7 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .15  8.6 .39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .082 9.4 .54
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .080 9.7 .46
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .096 8.6 .38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .064 9.5 .71
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .072 10   .51
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .068 9.1 .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .064 9.3 .56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .071 9.3 .50
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .080 9.7 .89
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .074 9.6 .53
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .070 8.9 .49
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .072 9.3 .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .068 9.3 .55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .092 9.7 .78
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .066 9.3 .86
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .065 9.4 .50
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .12  9.8 .51
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .079 10   .45
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .11  9.3 .34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .061 10   .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .12  8.9 .37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .062 10   .68
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .080 9.8 .38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .071 9.5 .41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .068 9.3 .59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .072 9.5 .50
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .077 9.5 .54
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .11  8.2 .42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .072 8.9 .54
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .068 9.7 .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .096 8.4 .42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .097 9.3 .43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .080 9.5 .54
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .085 9.5 .57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .068 9.6 .54
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .063 9.4 .60
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .073 8.8 .56
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .071 9.6 .53
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .12  8.9 .39
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .14  9.4 .41
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .080 9.5 .57
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .088 10   .67
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .078 9.5 .81
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .12  8.9 .42
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .069 9.1 .61
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .078 8.9 .54
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .083 10   .50
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .083 9.2 .76
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .075 9.7 .73
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .074 9.4 .61
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .069 9.5 .46
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .13  9.4 .53
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .075 9.6 .45
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .14  9.8 .58
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .064 9.5 .47
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .077 9.6 .49
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .077 9.4 .77
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .066 9.5 .56
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .080 9.4 .51
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .082 9.7 .42
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .085 9.7 .72
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .12  9.6 .48
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .081 9.6 .60
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .079 9.3 .50
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .083 9.2 .69
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .068 9.0 .61
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .12  11   1.2 
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .12  9.3 .51
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 880     1300   8900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c error (42) 880     1200   8800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 1.7   50   21   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c error (42) 880     2300   4000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c error (42) 880     1300   5100   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c error (42) 880     1500   5900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c error (42) 880     1400   9300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true .32  9.7 3.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c error (42) 880     1300   7700   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c error (42) 880     1400   8300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c error (42) 880     1500   9300   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c error (42) 880     2600   12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c error (42) 880     5000   5100   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c error (42) 880     1200   7800   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c error (42) 880     1100   6900   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c error (42) 880     660   6700   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c error (42) 880     660   8300   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c error (42) 880     2200   5300   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c error (42) 880     6400   7000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c error (42) 880     3100   4400   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 1.8   50   22   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c error (42) 880     2400   4800   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c error (42) 880     1400   10000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true .33  10   3.6 
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c error (42) 880     7000   3600   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c error (42) 880     2000   6800   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c error (42) 880     430   6500   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c error (42) 880     1300   8200   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c error (42) 880     1600   8100   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c error (42) 880     2200   10000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c error (42) 880     550   6500   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c error (42) 880     1200   9200   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c error (42) 880     1000   7900   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .22  7.0 2.1 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 880     1900   9000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c error (42) 880     1200   7600   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c error (42) 880     3300   4000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c error (42) 880     4500   4600   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c error (42) 880     3200   2800   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c error (42) 880     3500   5700   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c error (42) 880     2100   8900   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c error (42) 870     1400   10000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c error (42) 880     1700   8400   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c error (42) 880     910   9800   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 520     14000   6200   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 410     14000   4300   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c error (42) 880     1900   8100   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c error (42) 880     1700   9200   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .42  15   3.9 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c error (42) 870     1300   4600   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c error (42) 880     4500   3900   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c error (42) 880     2100   5500   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c error (42) 880     1300   11000   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c error (42) 880     1400   11000   
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c error (42) 870     10000   12000   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c error (42) 880     890   4900   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c error (42) 880     2900   11000   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c error (42) 880     2100   9700   
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 5.1   140   72   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (42) 880     5300   5800   
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (42) 880     1000   6100   
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (42) 880     6300   3400   
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (42) 880     1000   5200   
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (42) 880     1000   6900   
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 4.4   130   57   
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (42) 880     5500   5800   
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .096 9.1 .64
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .082 9.6 .77
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 25     210   240   
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .078 9.5 .54
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .079 9.8 .84
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .079 9.5 .55
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .13  9.1 .62
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .081 9.8 1.1 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1.0   63   12   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (42) 870     240   3400   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (42) 880     2800   9200   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (42) 880     180   3300   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c out of memory 690     15000   4500   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 2.6   71   29   
termination-numeric/Parts_true-termination_true-no-overflow.c error (42) 880     730   4500   
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (42) 880     5500   5700   
termination-numeric/gcd01_true-termination_true-no-overflow.c error (42) 880     4800   5600   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .52  15   6.4 
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true .47  12   4.3 
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (42) 870     5000   6400   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (42) 880     5000   6900   
termination-numeric/twisted_true-termination_true-no-overflow.c out of memory 290     14000   3600   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .14  9.6 .62
recursive/Addition03_false-no-overflow.c false(no-overflow) .083 9.7 .87
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .079 9.6 .62
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 880     240   4200   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     230   3200   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 880     230   3200   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 880     230   3100   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 760     15000   9000   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 770     15000   7400   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     15000   9800   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .092 6.2 .42
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     2800   9300   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     2800   7900   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 880     200   7500   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .12  7.6 1.2 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     190   5100   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     180   3500   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     180   4000   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 880     1600   4100   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     1600   3400   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     330   3500   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 880     200   3100   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     4800   8100   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     6800   9700   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 880     1400   3500   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true .37  12   4.3 
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true .44  12   4.2 
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .097 9.2 .39
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .073 9.0 .51
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .11  8.5 .37
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .15  9.1 .42
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .074 9.3 .63
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     5000   4800   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     5000   5400   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     5000   6700   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     5000   5900   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     9900   6100   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     640   13000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     640   13000   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 880     5000   6600   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 640     15000   4500   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 700     15000   3900   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 660     15000   4200   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 690     15000   4100   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 720     15000   3700   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 710     15000   4700   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (42) 880     11000   4700   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 820     15000   8000   
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .13  9.8 1.0 
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .14  10   1.1 
bitvector/byte_add_false-no-overflow.i false(no-overflow) .13  9.5 1.5 
bitvector/jain_1_false-no-overflow.i false(no-overflow) .070 9.3 .38
bitvector/jain_2_false-no-overflow.i false(no-overflow) .095 9.9 .78
bitvector/jain_4_false-no-overflow.i false(no-overflow) .086 9.3 .72
bitvector/jain_5_false-no-overflow.i out of memory 260     15000   3200   
bitvector/jain_6_false-no-overflow.i false(no-overflow) .084 9.4 .73
bitvector/jain_7_false-no-overflow.i false(no-overflow) .081 9.2 .71
bitvector/modulus_false-no-overflow.i false(no-overflow) .071 10   .56
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .12  6.3 1.2 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .12  6.5 1.1 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .12  6.8 1.7 
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .25  8.3 2.1 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .49  21   6.2 
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .52  21   7.0 
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .062 6.9 .58
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .16  6.4 .93
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i error (42) 880     650   3500   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i error (42) 880     960   4500   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i error (42) 880     1300   5000   
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 250     15000   2900   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i error (42) 880     1300   3800   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i error (42) 880     1300   4300   
bitvector/modulus_true-unreach-call_true-no-overflow.i true 45     1100   430   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .099 6.7 .67
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .11  6.8 .78
bitvector/parity_true-unreach-call_true-no-overflow.i true .22  7.2 2.2 
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 880     5200   3400   
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 880     5300   3700   
psyco/psyco_abp_1_false-no-overflow.c error (42) 880     1600   6000   
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 130000 620000 920000
    correct results 200 56 2400 530
        correct true 31 15 530 180
        correct false 169 40 1900 350
    correct-unconfimed results 6 53 1300 540
        correct-unconfirmed true 6 53 1300 540
        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]