Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 13:07:37 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) 4.1  410 30  
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 3.8  420 33  
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 4.2  420 27  
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 3.9  420 39  
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 4.2  420 29  
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 4.0  410 32  
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 3.9  420 30  
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 4.1  420 30  
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 4.0  420 31  
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 4.0  420 32  
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i unknown 1.3  48 15  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i unknown 1.6  49 20  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i unknown 1.7  48 21  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i false(no-overflow) 480    420 5400  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i unknown 480    110 6200  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .53 75 6.6
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .60 75 6.7
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .61 49 7.3
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .55 75 6.7
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .54 75 6.0
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .56 75 6.9
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .40 48 5.0
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .85 75 12  
termination-crafted/Cairo_step2_false-no-overflow.c unknown 77    75 1000  
termination-crafted/Collatz_unknown-termination_false-no-overflow.c unknown 21    75 260  
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .40 75 4.7
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .61 75 7.4
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .57 75 7.7
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .53 75 6.4
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .54 75 6.9
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .55 75 6.0
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .37 75 4.3
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .56 75 6.6
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .57 49 6.5
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .52 48 5.6
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .55 75 6.2
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .38 75 4.3
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 12    75 140  
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .55 75 5.6
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .55 75 6.4
termination-crafted/NonTerminationSimple4_false-no-overflow.c unknown 76    75 950  
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .55 75 6.3
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .54 75 6.5
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .57 75 7.2
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .53 75 7.7
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .55 75 6.0
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .58 75 6.6
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .57 49 7.7
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .56 49 7.0
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .36 75 4.1
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .56 75 6.7
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .56 75 6.5
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .54 75 8.1
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .55 75 7.0
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .57 75 7.5
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .54 75 6.2
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .57 75 6.9
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .62 77 7.9
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .41 75 4.6
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .39 75 4.6
termination-crafted/easy2_false-no-overflow.c unknown 160    390 2300  
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.2  76 14  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c unknown 60    100 790  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c unknown 1.3  75 14  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  100 18  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c unknown 7.6  75 92  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 7.2  75 89  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.5  75 15  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c unknown 380    560 4700  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 1.2  75 18  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 68    75 850  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  75 20  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.3  75 16  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c unknown 1.5  75 17  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c unknown 38    100 500  
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c unknown 120    160 1500  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c unknown 1.2  75 12  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c unknown 900    120 9700  
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 510    15000 7100  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  75 16  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c unknown 450    15000 6300  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c unknown 440    15000 6000  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 440    15000 5900  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 390    15000 4400  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 440    15000 6000  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 500    15000 5300  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 500    15000 7300  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c unknown 1.2  75 13  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c unknown 1.4  75 16  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  75 17  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.3  75 17  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.2  75 16  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c unknown 72    75 1000  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.3  75 15  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  75 14  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.2  48 12  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c unknown 1.2  75 13  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c unknown 1.4  75 17  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 120    240 1600  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .58 100 6.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .60 130 6.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .40 75 4.7
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .39 75 4.4
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .63 100 6.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .38 75 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .58 130 6.7
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c unknown 160    390 2100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .39 75 4.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .54 75 6.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c unknown 900    710 6100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c unknown 900    140 12000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .56 75 6.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .55 75 6.6
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .39 75 4.8
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .38 75 4.7
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .61 76 7.1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 480    130 6900  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .40 75 4.7
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .41 75 4.5
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .39 75 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .44 76 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .42 76 4.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .55 75 6.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .37 75 5.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .39 75 4.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .39 75 4.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .38 75 5.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .54 75 7.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .54 75 6.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .56 75 6.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .56 75 6.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .56 75 7.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .40 75 4.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .37 75 4.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .55 75 6.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .39 75 5.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .39 75 4.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .40 75 4.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .55 75 6.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .39 75 4.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .40 75 4.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .54 75 5.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .38 75 4.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .36 75 4.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .54 75 6.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .36 75 4.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .56 75 7.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .37 75 4.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .55 75 6.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .55 75 5.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .37 75 4.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .38 75 5.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .54 75 7.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .56 75 7.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .39 75 4.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .39 75 4.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .37 75 5.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .38 75 3.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .55 75 6.6
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .39 75 4.8
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .56 75 6.8
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .56 100 6.6
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .55 75 6.6
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .57 75 7.6
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .65 79 8.1
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .55 75 7.2
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .58 75 6.4
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .56 75 6.4
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .57 75 6.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .56 49 6.5
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .56 49 7.7
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .57 49 6.3
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .56 51 7.4
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .55 75 6.1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .56 75 5.9
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .55 75 7.0
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .55 75 6.4
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .36 75 4.5
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .54 75 7.2
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .53 75 6.5
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .55 75 8.4
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .56 76 6.5
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .56 75 7.7
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .40 75 4.3
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .37 75 4.7
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .40 75 4.6
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .41 75 4.7
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .55 75 7.2
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .68 76 8.3
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .57 100 6.5
termination-crafted-lit/joey_false-no-overflow.c out of memory (false(no-overflow)) 630    15000 8800  
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .42 75 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 890    120 9800  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c unknown 1.4  75 15  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c unknown 1.4  75 18  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c unknown 120    240 1700  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c unknown 900    710 12000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c unknown 900    1200 8000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c unknown 890    130 11000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c unknown 7.3  76 89  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c unknown 1.5  75 17  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c unknown 1.5  75 17  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c unknown 1.4  75 14  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c unknown 1.5  100 17  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c unknown 1.8  100 25  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c unknown 890    110 13000  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c unknown 200    270 2800  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c unknown 43    75 540  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c unknown 30    75 340  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c unknown 1.9  100 24  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c unknown 900    5300 13000  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c unknown 130    230 1800  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c unknown 1.4  75 16  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c unknown 160    390 2000  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c unknown 900    130 12000  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c unknown 13    76 150  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c unknown 1.2  75 13  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c unknown 1.5  75 20  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c unknown 1.2  75 16  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c unknown 1.2  75 13  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c unknown 1.3  75 16  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c unknown 1.3  75 17  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c unknown 2.0  75 25  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c unknown 1.2  75 14  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c unknown 1.5  75 18  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c unknown 1.4  75 16  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 900    160 11000  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c unknown 1.3  75 14  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c unknown 270    190 3600  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c unknown 1.4  75 17  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 1.4  75 18  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c unknown 890    320 11000  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c unknown 140    100 1700  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c unknown 1.5  75 19  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c unknown 500    110 6300  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c unknown 890    130 9500  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c unknown 580    15000 7300  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c unknown 450    15000 6000  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c unknown 2.1  75 25  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c unknown 1.3  75 14  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c unknown 1.4  75 15  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c unknown 1.8  100 20  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c unknown 1.4  75 15  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c unknown 1.7  100 18  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c unknown 1.2  75 14  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c unknown 1.4  75 17  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c unknown 1.4  100 16  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c unknown 1.4  100 20  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c unknown 1.3  75 17  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c unknown 1.3  75 14  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c unknown 22    75 260  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c unknown 1.4  75 20  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout (false(no-overflow)) 900    590 11000  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 1.4  75 14  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout (false(no-overflow)) 900    530 11000  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout (false(no-overflow)) 900    560 11000  
termination-crafted-lit/genady_true-termination_true-no-overflow.c unknown 54    75 780  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c false(no-overflow) .54 75 5.6
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .54 49 6.3
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .59 49 6.6
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 27    140 330  
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .45 49 5.3
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .58 49 8.0
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .54 49 7.3
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .49 49 5.3
termination-numeric/MultCommutative_false-no-overflow.c unknown 480    15000 5900  
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1.7  140 21  
termination-numeric/Ackermann01_true-termination_true-no-overflow.c unknown 460    15000 6400  
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c unknown 1.6  49 21  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c unknown 380    15000 4700  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c unknown 1.3  49 14  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c unknown 2.0  77 24  
termination-numeric/Parts_true-termination_true-no-overflow.c unknown 900    430 8100  
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 5.8  150 52  
termination-numeric/gcd01_true-termination_true-no-overflow.c unknown 430    15000 5400  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c unknown 1.4  75 17  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c unknown 1.8  49 20  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c unknown 2.5  97 30  
termination-numeric/rec_counter3_true-termination_true-no-overflow.c unknown 2.4  99 28  
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (false(no-overflow)) 900    6600 13000  
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .56 49 7.6
recursive/Addition03_false-no-overflow.c false(no-overflow) .56 49 7.1
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 64    73 750  
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 450    15000 5400  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 460    15000 5300  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 460    15000 5500  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 460    15000 5900  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 400    15000 5400  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c unknown 400    15000 5100  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 400    15000 5000  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 1.2  49 14  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 64    74 900  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 64    75 710  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 860    15000 11000  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 1.4  49 16  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 380    15000 5100  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 380    15000 4700  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 380    15000 5100  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 510    15000 6900  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 510    15000 6100  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 480    15000 6400  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 530    15000 6700  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 420    15000 4600  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 420    15000 5400  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 410    15000 4700  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 1.9  49 21  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 1.8  49 20  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .54 49 8.3
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .56 49 7.3
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .57 49 6.4
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .56 49 6.4
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .57 49 8.8
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 1.5  49 16  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 1.5  49 17  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 1.5  49 17  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 1.5  49 20  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 1.4  49 17  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(no-overflow) .53 49 5.9
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) .56 49 7.0
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) .56 49 6.3
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 16  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 15  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 13  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 13  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 14  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 13  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 14  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 1.2  49 14  
bitvector/byte_add_1_false-no-overflow.i unknown 1.8  100 23  
bitvector/byte_add_2_false-no-overflow.i unknown 1.8  100 21  
bitvector/byte_add_false-no-overflow.i unknown 2.1  110 23  
bitvector/jain_1_false-no-overflow.i false(no-overflow) .56 75 6.5
bitvector/jain_2_false-no-overflow.i false(no-overflow) .63 75 8.3
bitvector/jain_4_false-no-overflow.i false(no-overflow) 29    80 330  
bitvector/jain_5_false-no-overflow.i unknown 900    2300 11000  
bitvector/jain_6_false-no-overflow.i false(no-overflow) 24    80 320  
bitvector/jain_7_false-no-overflow.i false(no-overflow) 93    97 1300  
bitvector/modulus_false-no-overflow.i false(no-overflow) .50 100 5.3
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 1.9  100 21  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 1.8  100 23  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unknown 2.0  110 25  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 500    99 6600  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 20    75 270  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 21    75 250  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unknown 500    110 7100  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 1.4  76 16  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 1.2  75 16  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 1.2  75 13  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 1.2  75 15  
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 1.2  75 13  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 1.2  75 13  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 1.2  75 13  
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 900    630 6900  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 1.4  75 15  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 1.4  75 16  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 1.4  76 19  
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 1.2  75 13  
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 1.2  75 17  
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 40000 540000 490000
    correct results 13 150 850 2000
        correct true 0
        correct false 13 150 850 2000
    correct-unconfimed results 149 630 15000 8500
        correct-unconfirmed true 0
        correct-unconfirmed false 149 630 15000 8500
    incorrect results 5 490 650 5400
        incorrect true 0
        incorrect false 5 490 650 5400
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]