Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213
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-03 04:09:48 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.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) .17  11 1.8 
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .17  11 1.5 
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .16  11 1.7 
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .16  11 1.7 
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .17  11 1.5 
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .14  11 1.9 
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .14  11 1.7 
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .15  11 1.7 
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .14  11 1.8 
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .17  11 1.7 
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .15  11 1.4 
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .16  11 1.4 
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .15  11 1.3 
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .15  11 1.6 
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .15  11 1.5 
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .18  12 1.6 
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .17  12 1.9 
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .18  12 2.7 
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted/Cairo_step2_false-no-overflow.c timeout (timeout) 900     170 13000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .17  12 2.0 
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .18  12 1.6 
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .19  12 1.7 
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .18  12 1.6 
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .16  12 1.8 
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .15  12 2.1 
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .16  11 2.0 
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .15  11 1.7 
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .15  12 1.7 
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (1) .099 11 1.2 
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) .17  11 1.7 
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .18  12 1.9 
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .18  11 1.7 
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .19  12 1.4 
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .16  12 2.6 
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .17  12 1.9 
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .16  14 1.8 
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .16  12 1.8 
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .20  12 1.9 
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .16  12 2.3 
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .19  12 2.4 
termination-crafted/easy2_false-no-overflow.c timeout (timeout) 900     210 13000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .13  11 1.5 
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     250 11000   
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout (timeout) 900     70 11000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     180 12000   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     52 12000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 900     55 14000   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .20  12 2.0 
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     100 13000   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (1) .080 11 .63
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     270 13000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     170 11000   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     230 13000   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 900     15 14000   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c unknown 300     2900 2500   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout (timeout) 900     3800 7900   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true .13  11 1.3 
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     76 12000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     72 12000   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     100 12000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 900     92 12000   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     130 11000   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     360 13000   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     290 14000   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     400 12000   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 900     980 11000   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     270 10000   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true .13  11 1.6 
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true .16  11 1.6 
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     4000 10000   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     250 12000   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     170 12000   
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout (timeout) 900     250 12000   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     330 11000   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     210 13000   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .14  11 1.3 
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true .13  11 1.4 
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .15  11 1.5 
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 900     180 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .20  12 1.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .22  12 2.4 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .21  12 2.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) .25  12 2.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout (timeout) 900     200 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .19  12 1.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout (timeout) 900     1900 9800   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout (timeout) 900     4000 8700   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .18  12 1.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .19  12 2.0 
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .20  12 1.9 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .17  12 2.3 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .21  12 2.1 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .20  12 1.8 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .20  12 2.3 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .21  12 2.0 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .20  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .17  12 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .17  12 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .17  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .17  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .20  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .17  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .17  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .17  12 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .18  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .16  12 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .17  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .19  12 1.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .16  12 2.2 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .16  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .15  12 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .16  12 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .17  12 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .17  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .17  12 2.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .16  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .20  12 1.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .17  12 1.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .21  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .16  12 2.2 
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .18  12 2.4 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c unknown 2.4   4300 25   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .18  12 1.6 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .16  12 1.7 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .16  12 1.6 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .18  12 1.8 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) .16  12 1.8 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .18  12 2.0 
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .19  12 1.7 
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .16  12 2.0 
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .16  12 1.8 
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .18  12 1.9 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .19  12 2.1 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) .21  12 2.0 
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) .20  12 2.0 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .19  12 1.9 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .16  12 2.1 
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .24  13 2.6 
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .20  12 2.2 
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     4000 9000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout (timeout) 900     360 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .15  11 1.4 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout (timeout) 900     210 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout (timeout) 900     350 8700   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout (timeout) 900     1900 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout (timeout) 900     4300 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c timeout (timeout) 900     3200 8000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout (timeout) 900     200 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout (timeout) 900     1800 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout (timeout) 900     31 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout (timeout) 900     190 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout (timeout) 900     320 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout (timeout) 900     68 12000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout (timeout) 900     210 12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout (timeout) 900     66 12000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     65 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     430 10000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout (timeout) 900     170 11000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout (timeout) 900     130 11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .14  11 1.6 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout (timeout) 900     190 12000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout (timeout) 900     4200 9700   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c timeout (timeout) 900     3100 7200   
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true .13  11 1.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout (timeout) 900     230 11000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout (timeout) 900     210 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     3900 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout (timeout) 900     3400 13000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout (timeout) 900     3800 8000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout (timeout) 900     23 13000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout (timeout) 900     81 12000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout (timeout) 900     51 11000   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .17  11 1.6 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     3900 13000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout (timeout) 900     190 12000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     120 12000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout (timeout) 900     190 13000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout (timeout) 900     250 13000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout (timeout) 900     75 12000   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout (timeout) 900     67 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout (timeout) 900     230 10000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     210 11000   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     45 14000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c timeout (timeout) 900     240 14000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout (timeout) 900     160 12000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout (timeout) 900     44 11000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout (timeout) 900     40 12000   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .15  11 1.7 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     190 11000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout (timeout) 900     240 12000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout (timeout) 900     680 12000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout (timeout) 900     3900 8100   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true .16  12 2.0 
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout (timeout) 900     190 11000   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout (timeout) 900     210 12000   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout (timeout) 900     3700 11000   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout (timeout) 900     15000 12000   
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout (timeout) 900     330 8500   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c unknown .22  13 2.3 
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c unknown .22  13 2.6 
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown .18  12 2.1 
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c unknown .22  13 2.0 
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c unknown .22  13 2.4 
termination-crafted-lit/genady_true-termination_true-no-overflow.c true .19  12 2.5 
termination-crafted-lit/strchr_true-no-overflow_true-termination.c unknown .19  12 2.2 
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .16  12 2.0 
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .19  12 1.7 
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) .24  12 3.1 
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .18  12 1.7 
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .19  12 1.8 
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .16  12 1.9 
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .19  12 1.7 
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .27  12 2.8 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 12     39 160   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout (timeout) 900     2000 11000   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout (timeout) 900     300 14000   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout (timeout) 900     250 13000   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout (timeout) 900     230 12000   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 20     170 290   
termination-numeric/Parts_true-termination_true-no-overflow.c timeout (timeout) 900     3200 11000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout (timeout) 900     350 9700   
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout (timeout) 900     49 12000   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .31  12 4.1 
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true .65  16 7.7 
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout (timeout) 900     500 12000   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout (timeout) 900     480 13000   
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (timeout) 900     1800 9700   
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .19  12 2.1 
recursive/Addition03_false-no-overflow.c false(no-overflow) .17  12 1.9 
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .20  12 1.8 
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout (timeout) 900     2100 12000   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     2500 11000   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout (timeout) 900     2100 11000   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout (timeout) 900     2100 13000   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     29 11000   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     72 14000   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     63 12000   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .15  11 1.4 
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     320 12000   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     300 11000   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout (timeout) 900     220 9700   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .18  11 1.7 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     220 11000   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     280 12000   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     270 11000   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     74 11000   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     74 12000   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     330 14000   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout (timeout) 900     44 11000   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     49 14000   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     29 12000   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 900     1200 12000   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true .64  14 8.4 
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true .71  14 10   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .16  12 2.4 
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .18  12 1.9 
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .17  12 2.2 
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .19  12 2.0 
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .17  12 1.9 
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true .14  11 1.4 
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true .15  11 1.4 
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true .15  11 1.4 
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true .15  11 1.4 
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true .13  11 1.3 
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 900     2300 12000   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 900     2300 9300   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 900     2500 9100   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true .15  11 1.3 
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true .15  11 1.5 
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true .13  11 1.2 
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true .15  11 1.4 
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true .13  11 1.5 
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true .15  11 1.5 
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true .16  11 1.3 
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true .13  11 1.4 
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .25  12 2.7 
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .25  12 2.2 
bitvector/byte_add_false-no-overflow.i false(no-overflow) .28  13 3.4 
bitvector/jain_1_false-no-overflow.i false(no-overflow) .19  12 1.7 
bitvector/jain_2_false-no-overflow.i false(no-overflow) .20  12 2.0 
bitvector/jain_4_false-no-overflow.i false(no-overflow) .18  12 2.2 
bitvector/jain_5_false-no-overflow.i false(no-overflow) .50  40 8.0 
bitvector/jain_6_false-no-overflow.i false(no-overflow) .19  12 1.8 
bitvector/jain_7_false-no-overflow.i false(no-overflow) .19  12 1.9 
bitvector/modulus_false-no-overflow.i false(no-overflow) .18  11 2.4 
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .33  12 4.3 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .36  12 4.1 
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .84  13 10   
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .31  12 4.3 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 21     16 260   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 25     16 340   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .17  11 1.7 
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .15  11 1.6 
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true .15  11 1.5 
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true .14  11 1.5 
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true .14  11 1.5 
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .13  11 1.3 
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true .15  11 1.5 
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true .15  11 1.6 
bitvector/modulus_true-unreach-call_true-no-overflow.i true 660     62 8800   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .17  11 1.8 
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .99  13 9.3 
bitvector/parity_true-unreach-call_true-no-overflow.i true .13  11 1.5 
bitvector/sum02_false-unreach-call_true-no-overflow.i true .13  11 1.4 
bitvector/sum02_true-unreach-call_true-no-overflow.i true .15  11 1.5 
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 110000 130000 1400000
    correct results 222 98 2700 1200
        correct true 53 55 590 700
        correct false 169 43 2100 500
    correct-unconfimed results 7 680 300 9100
        correct-unconfirmed true 7 680 300 9100
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]