Tool symbiotic 6.0.3-77d4af47
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-07 21:42:05 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]
Options --witness witness.graphml
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .21 15 2.3
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .19 16 1.9
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .21 16 2.3
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .19 16 2.6
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .19 16 2.1
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .19 16 2.1
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .20 16 2.3
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .18 17 2.0
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .21 17 2.1
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .18 15 2.5
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .14 15 1.7
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .17 16 2.1
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .15 16 2.0
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .16 16 1.9
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .15 16 2.4
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .26 18 2.3
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .28 18 3.3
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .24 18 3.3
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .24 18 3.3
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .26 17 2.7
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .24 19 2.8
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .25 18 2.6
termination-crafted/Cairo_step2_false-no-overflow.c timeout (verification) 900    260 11000  
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .24 18 2.8
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .22 17 2.8
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .24 17 2.0
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .24 19 2.8
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .22 19 2.7
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .24 18 3.3
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .24 18 2.5
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .22 19 2.6
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .18 16 2.0
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .22 17 2.5
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .27 20 2.5
termination-crafted/NonTerminationSimple4_false-no-overflow.c false(no-overflow) .21 18 3.0
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .27 18 2.8
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .23 17 4.6
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .26 17 2.8
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .22 18 3.2
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .24 23 2.7
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .24 17 2.7
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .27 18 3.0
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .28 22 2.3
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .23 17 2.7
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .25 18 2.7
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .22 18 2.8
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .22 18 2.4
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .22 19 2.5
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .26 18 3.4
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .24 18 2.6
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .24 18 3.3
termination-crafted/easy2_false-no-overflow.c timeout (verification) 900    410 7800  
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .13 16 1.6
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    450 7100  
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c timeout (verification) 900    69 11000  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    200 12000  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    78 12000  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 900    74 12000  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .21 18 2.8
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    430 7700  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true .16 17 1.6
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    430 11000  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    250 13000  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    520 8900  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 900    680 10000  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    2700 6200  
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error(unknown, verification-finished) 740    2500 6400  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true .14 15 1.5
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    280 12000  
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    290 12000  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    440 8100  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 900    520 12000  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    280 11000  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    620 12000  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    500 7600  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    550 8100  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 900    4200 10000  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    1000 12000  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true .17 16 1.9
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 900    17 11000  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    3300 11000  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    440 7600  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    280 11000  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout (verification) 900    450 10000  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    530 11000  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    440 7300  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .13 15 1.6
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .17 16 1.6
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .19 18 2.5
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 900    410 7900  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .26 18 2.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .25 18 2.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .24 18 3.7
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .25 19 2.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .26 18 3.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .27 18 3.1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .41 18 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout (verification) 900    430 11000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .24 18 2.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .23 18 2.6
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout (verification) 900    1200 12000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout (verification) 900    3100 9100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .22 19 2.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .27 18 2.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .23 17 3.4
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .27 19 2.8
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .23 18 3.1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .26 18 2.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .24 18 2.7
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .26 18 3.0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .27 18 3.6
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .24 18 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .23 18 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .23 17 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .23 17 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .22 18 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .22 18 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .23 18 2.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .24 23 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .23 18 3.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .23 18 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .22 17 2.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .23 17 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .25 18 3.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .27 18 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .24 18 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .22 19 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .23 20 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .23 18 2.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .22 18 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .22 17 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .23 18 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .23 19 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .25 18 2.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .24 18 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .27 23 2.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .25 18 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .23 18 2.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .23 18 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .23 18 2.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .22 17 2.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .24 17 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .24 19 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .26 18 2.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .23 18 2.6
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .25 18 2.6
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .24 19 2.9
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .22 17 2.6
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .27 18 3.3
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .22 18 3.0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) .29 18 3.4
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .23 17 2.6
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .22 17 2.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .26 18 2.7
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .24 18 2.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .28 18 3.1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .23 18 2.9
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .25 17 2.5
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .23 18 2.4
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .22 19 3.3
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .27 22 2.8
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .23 18 2.8
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .24 17 2.7
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .23 18 3.1
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .24 18 3.3
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .27 18 3.0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .26 18 3.1
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .26 18 3.1
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .27 23 2.5
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .25 18 2.6
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .80 18 12  
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .27 18 3.7
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .25 18 3.3
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .24 18 2.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    3300 10000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout (verification) 900    1400 12000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .21 19 2.1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout (verification) 900    420 7200  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout (verification) 900    310 14000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout (verification) 900    1300 13000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout (verification) 900    3100 7500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c timeout (verification) 900    4000 6800  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout (verification) 900    480 8400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout (verification) 900    1200 12000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout (verification) 900    170 11000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout (verification) 900    220 10000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout (verification) 900    1000 9600  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout (verification) 900    120 8100  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout (verification) 900    380 9000  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout (verification) 900    62 14000  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    62 11000  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    320 13000  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout (verification) 900    140 12000  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout (verification) 900    420 8400  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .19 18 2.0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout (verification) 900    430 7700  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout (verification) 900    3200 9900  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c timeout (verification) 900    4000 7700  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .16 15 2.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout (verification) 900    480 5800  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout (verification) 900    420 9200  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    2800 10000  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout (verification) 900    2700 12000  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout (verification) 900    2900 8500  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout (verification) 900    45 11000  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout (verification) 900    600 12000  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout (verification) 900    50 12000  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .15 15 1.8
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    2800 12000  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout (verification) 900    400 9500  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    430 7900  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout (verification) 900    460 9500  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout (verification) 900    430 6600  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout (verification) 900    77 13000  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout (verification) 900    57 11000  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout (verification) 900    2500 11000  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    390 8900  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    55 12000  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c timeout (verification) 900    380 12000  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout (verification) 900    500 12000  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout (verification) 900    100 10000  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout (verification) 900    220 7300  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .16 15 1.8
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    310 14000  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout (verification) 900    430 7100  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout (verification) 900    980 12000  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout (verification) 900    2900 12000  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .22 18 2.6
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout (verification) 900    410 12000  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout (verification) 900    410 9700  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout (verification) 900    3000 12000  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 170    15000 2700  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout (verification) 900    370 12000  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true .20 17 2.8
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout (verification) 900    330 11000  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout (verification) 900    430 11000  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true .21 17 2.5
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout (verification) 900    450 12000  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .22 15 2.9
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true .23 19 2.1
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .24 18 2.8
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .24 18 3.0
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) .36 18 4.8
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .24 19 3.2
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .23 18 3.1
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .23 18 2.5
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .23 18 2.7
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .43 18 6.3
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 9.8  50 140  
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout (verification) 900    14000 14000  
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout (verification) 900    1300 14000  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout (verification) 900    2900 12000  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout (verification) 900    460 9100  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 23    160 220  
termination-numeric/Parts_true-termination_true-no-overflow.c timeout (verification) 900    10000 13000  
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout (verification) 900    9000 11000  
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout (verification) 900    59 11000  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .42 18 5.4
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true .66 18 8.3
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout (verification) 900    2800 11000  
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout (verification) 900    2800 11000  
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (verification) 900    1200 11000  
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .27 19 3.0
recursive/Addition03_false-no-overflow.c false(no-overflow) .26 18 2.8
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .28 19 3.1
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout (verification) 900    13000 12000  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    15000 11000  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout (verification) 900    13000 12000  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout (verification) 900    13000 14000  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    250 12000  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    250 13000  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    440 11000  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .20 16 2.4
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    1300 11000  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    1300 11000  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 770    15000 12000  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .21 17 1.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c probably out of memory (killed (signal 9, verification)) 710    15000 9800  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    2400 11000  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    3000 10000  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    260 12000  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    260 11000  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    220 11000  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout (verification) 900    120 12000  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    63 12000  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout (verification) 900    62 13000  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c probably out of memory (killed (signal 9, verification)) 830    15000 14000  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true .68 23 8.5
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true .67 18 8.1
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .24 18 2.8
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .29 18 3.2
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .25 18 2.8
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .26 19 2.3
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .26 19 3.2
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true .20 17 2.9
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true .20 16 2.2
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true .19 15 2.6
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true .20 16 1.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true .20 17 2.4
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout (verification) 900    1500 12000  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout (verification) 900    1500 8200  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout (verification) 900    1500 9300  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true .19 17 2.4
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true .20 17 2.1
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true .19 16 2.1
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true .19 16 2.0
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true .19 17 2.3
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true .20 17 2.6
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true .19 16 2.4
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true .20 16 2.1
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .55 18 6.8
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .55 18 6.9
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1.0  18 14  
bitvector/jain_1_false-no-overflow.i false(no-overflow) .25 19 3.6
bitvector/jain_2_false-no-overflow.i false(no-overflow) .27 18 3.1
bitvector/jain_4_false-no-overflow.i false(no-overflow) .25 18 2.7
bitvector/jain_5_false-no-overflow.i false(no-overflow) 1.2  50 15  
bitvector/jain_6_false-no-overflow.i false(no-overflow) .25 17 2.5
bitvector/jain_7_false-no-overflow.i false(no-overflow) .28 19 3.0
bitvector/modulus_false-no-overflow.i false(no-overflow) .27 19 3.3
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .67 18 9.5
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .70 19 11  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2.0  19 27  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .40 21 4.8
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 93    46 1200  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 100    44 1300  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .19 16 2.2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .19 16 2.2
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true .20 17 2.1
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true .22 17 2.1
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true .19 16 2.3
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .18 16 3.1
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true .18 15 2.2
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true .21 16 2.1
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout (verification) 900    140 9900  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .18 17 2.2
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 3.6  19 45  
bitvector/parity_true-unreach-call_true-no-overflow.i true .19 17 2.2
bitvector/sum02_false-unreach-call_true-no-overflow.i true .21 16 3.1
bitvector/sum02_true-unreach-call_true-no-overflow.i true .21 16 2.0
psyco/psyco_abp_1_false-no-overflow.c timeout (verification) 900    2700 7200  
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 110000 270000 1300000
    correct results 230 260 4200 3300
        correct true 59 210 1000 2600
        correct false 171 54 3200 660
    correct-unconfimed results 3 27 190 260
        correct-unconfirmed true 3 27 190 260
        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]