Tool CBMC 5.8
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 11:16:27 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.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) .25 34 2.5
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .26 34 2.5
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .27 34 2.1
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .25 34 2.5
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .25 34 2.4
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .26 34 2.1
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .24 34 2.3
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .24 34 2.0
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .26 34 2.2
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .27 34 2.2
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .44 34 5.1
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .47 34 4.4
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .44 34 4.1
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .47 34 4.3
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .46 34 4.3
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .24 33 2.0
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .28 36 2.6
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .25 33 2.5
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .24 33 2.8
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .24 33 2.3
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .27 33 2.2
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .28 34 2.6
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .26 33 2.1
termination-crafted/Cairo_step2_false-no-overflow.c error (42) 870    5100 5000  
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .26 33 2.3
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .26 35 2.0
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .29 33 2.4
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .23 33 2.2
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .25 33 2.3
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .24 33 2.3
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .25 33 2.6
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .24 33 2.1
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .24 33 2.2
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1.8  35 20  
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .23 33 2.5
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (42) 880    5100 4300  
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .23 33 1.9
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .28 33 2.0
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .23 33 2.4
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .25 35 2.4
termination-crafted/RecursiveMultiplication_false-no-overflow.c witness invalid (false(no-overflow)) .25 33 2.2
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .27 33 2.2
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .26 33 2.1
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .28 35 2.1
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .27 33 2.3
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .27 33 2.2
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .24 33 2.0
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .27 33 2.5
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .24 35 2.5
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .26 33 2.2
termination-crafted/easy2_false-no-overflow.c error (42) 870    2200 3100  
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2.2  34 28  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    3000 3200  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c error (42) 870    3900 4200  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    3800 3000  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    5300 4700  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    5500 5800  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .45 33 3.8
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    2200 3200  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    8400 3400  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    4600 5900  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    4500 4000  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    3200 4900  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    3900 3500  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c error (134) 50    14000 600  
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error (134) 58    14000 730  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 210    15000 2800  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    1200 8200  
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    2000 2900  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    3200 4100  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    310 3700  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    290 2400  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    710 3800  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    480 3200  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    700 3600  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    810 6200  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    4100 5400  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c error (42) 870    2700 5600  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 870    5300 4400  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    2200 6500  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    2100 6800  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    830 9100  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c error (42) 870    4500 4000  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    1300 9500  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    5100 4100  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .39 33 5.0
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .41 33 4.3
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 4.2  61 55  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 870    2400 4200  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .27 33 1.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .28 36 2.6
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .24 33 2.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .29 33 2.6
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .28 33 2.3
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .26 33 2.7
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c error (42) 870    2400 3400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .26 33 1.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .25 33 1.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c error (42) 870    1500 5000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c error (42) 870    590 9400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .25 33 2.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .25 33 2.2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .25 33 2.3
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .25 33 2.6
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .35 38 2.6
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .28 35 2.4
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .27 33 2.2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .25 33 2.2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .28 33 2.2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .27 33 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .25 33 1.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .24 33 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .23 33 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .24 33 1.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .26 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .27 33 1.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .24 33 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .26 33 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .25 33 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .27 34 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .27 33 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .26 33 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .25 33 2.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .27 34 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .25 33 2.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .28 33 2.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .26 33 1.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .24 33 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .25 33 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .23 33 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .28 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .24 33 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .23 33 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .26 33 1.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .27 33 2.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .25 33 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .24 33 2.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .24 35 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .25 33 1.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .28 33 2.2
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .24 33 2.1
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .24 33 2.1
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .28 33 2.1
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .28 33 2.0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .29 33 2.0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .24 33 2.6
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .24 33 2.4
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .26 33 2.3
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .24 33 2.6
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .29 33 2.4
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .28 33 2.1
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .24 33 2.3
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .23 33 2.5
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .24 33 2.6
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .27 33 2.1
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .27 33 2.0
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .25 35 2.0
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .26 33 2.1
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .28 33 1.9
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .25 33 2.7
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .25 33 2.2
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .28 33 2.2
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .23 33 2.4
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .26 33 2.0
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .25 33 2.6
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .44 34 4.6
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .25 35 2.3
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .30 34 3.1
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .27 35 2.1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 870    590 8400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c error (42) 870    1800 6000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 4.3  61 44  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c error (42) 870    2300 3900  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c error (42) 870    1700 5400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c error (42) 870    1500 4800  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c error (42) 870    610 8700  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 1.4  34 15  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c error (42) 870    1400 7400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c error (42) 870    1200 8500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c error (42) 870    1300 5500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c error (42) 870    2700 7200  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c error (42) 870    5500 5100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c error (42) 870    1100 7300  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c error (42) 870    1400 5700  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c error (42) 870    360 7500  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c error (42) 870    360 6900  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c error (42) 870    2400 4400  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c error (42) 870    7000 3600  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c error (42) 870    3100 4400  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 4.3  62 47  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c error (42) 870    2300 3900  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c error (42) 870    610 10000  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 1.4  35 18  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c error (42) 880    8400 3900  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c error (42) 870    1100 7600  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c error (42) 870    1200 5600  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c error (42) 870    1200 7100  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c error (42) 870    1600 7700  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c error (42) 870    2000 5700  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c error (42) 870    520 6500  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c error (42) 870    1100 6900  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c error (42) 870    1300 7200  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2.7  35 32  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 870    1600 8700  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c error (42) 870    1000 5700  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c error (42) 870    3100 4400  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c error (42) 880    4500 3700  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c error (42) 870    3400 4500  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c error (42) 870    770 4900  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c error (42) 870    3000 7900  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c error (42) 870    1300 7400  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c error (42) 870    1700 6300  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c error (42) 870    640 8300  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (42) 870    7400 6500  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (134) 490    15000 5000  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c error (42) 870    980 5900  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c error (42) 870    1800 5700  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2.5  37 27  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c error (42) 870    1700 4300  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c error (42) 870    4400 3300  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c error (42) 870    2400 3400  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c error (42) 870    1300 5700  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c error (42) 870    2800 5700  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c error (42) 870    13000 12000  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c error (42) 870    780 4400  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c error (42) 870    2600 7900  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c error (42) 870    2900 5600  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 8.1  180 93  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (42) 870    8400 3400  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (42) 870    1200 3900  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (42) 870    7500 3700  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (42) 870    1200 3400  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (42) 870    1200 4400  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 9.4  160 110  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (6) 730    8500 3800  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .27 33 2.4
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .27 35 2.2
termination-numeric/Binomial_true-termination_false-no-overflow.c witness invalid (false(no-overflow)) 23    250 280  
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .27 33 1.8
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .28 33 2.3
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .25 33 2.1
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .27 34 2.5
termination-numeric/MultCommutative_false-no-overflow.c witness invalid (false(no-overflow)) .30 34 2.5
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 2.0  78 25  
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (42) 870    330 2600  
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (42) 870    2800 6600  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (42) 870    260 3000  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c out of memory 730    15000 5200  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 5.0  91 55  
termination-numeric/Parts_true-termination_true-no-overflow.c error (42) 870    840 5700  
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (42) 870    2500 4600  
termination-numeric/gcd01_true-termination_true-no-overflow.c error (42) 880    5000 4800  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2.7  38 29  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2.6  36 25  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (42) 870    5800 4000  
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (42) 870    5800 4600  
termination-numeric/twisted_true-termination_true-no-overflow.c error (134) 170    13000 1900  
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .28 35 2.1
recursive/Addition03_false-no-overflow.c false(no-overflow) .27 33 2.2
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .25 33 2.5
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 870    330 2900  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 870    360 3500  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 870    350 3400  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 870    340 3000  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 860    15000 8000  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (42) 880    15000 9100  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 880    6800 4600  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .43 33 3.9
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    2800 6500  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 870    2800 7400  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 870    260 3700  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 1.3  33 13  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    260 3000  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 870    250 2500  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 870    260 2900  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 870    2000 3500  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    2000 3700  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    450 2100  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 870    310 4100  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    5000 4200  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 880    7200 5900  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 870    1400 2900  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2.6  36 27  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2.6  36 28  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .24 33 2.0
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .27 33 2.1
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .26 33 2.2
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .26 33 2.1
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .24 33 2.2
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 870    5200 5200  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 870    5200 5900  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 870    5200 5700  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 870    5200 4800  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 870    9200 4300  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 880    5200 7500  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 870    5200 7600  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 880    6100 5000  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 640    15000 3900  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 660    15000 3800  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 560    15000 5600  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 670    15000 3700  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 650    15000 3600  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 660    15000 3400  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c out of memory 780    15000 6300  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 870    15000 4000  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .66 33 6.1
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .66 34 6.6
bitvector/byte_add_false-no-overflow.i false(no-overflow) .68 33 5.9
bitvector/jain_1_false-no-overflow.i false(no-overflow) .24 33 1.8
bitvector/jain_2_false-no-overflow.i false(no-overflow) .23 33 2.5
bitvector/jain_4_false-no-overflow.i false(no-overflow) .24 34 2.5
bitvector/jain_5_false-no-overflow.i out of memory 370    15000 5400  
bitvector/jain_6_false-no-overflow.i false(no-overflow) .26 34 2.4
bitvector/jain_7_false-no-overflow.i false(no-overflow) .27 33 2.2
bitvector/modulus_false-no-overflow.i false(no-overflow) .24 33 2.0
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .86 34 8.4
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .86 33 7.8
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .88 33 8.8
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .53 35 5.4
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 1.6  42 19  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 1.6  42 17  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .81 33 7.0
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 1.6  33 16  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i error (42) 870    910 4200  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i error (42) 870    1300 4700  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i error (42) 870    1600 5300  
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 380    15000 4500  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i error (42) 870    1600 4300  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i error (42) 870    1600 3700  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 120    1000 660  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1.2  33 12  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1.2  33 12  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2.5  34 25  
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 870    6800 5100  
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 870    6400 3800  
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 130000   650000 770000
    correct results 192 100   6800 1100
        correct true 29 59   1400 660
        correct false 163 46   5500 410
    correct-unconfimed results 11 140   1400 840
        correct-unconfirmed true 8 130   1300 820
        correct-unconfirmed false 3 2.0 100 19
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]