Tool ULTIMATE Taipan 0.1.23-3204b741
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 08:43:49 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
Options --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) 4.1 240 34
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 4.7 270 41
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 4.1 240 34
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 4.3 240 37
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 4.0 240 35
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 4.4 270 39
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 4.0 240 35
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 4.4 260 34
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 4.1 240 33
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 4.1 250 38
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 4.3 240 33
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 4.7 280 42
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 4.3 250 34
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 4.2 240 32
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 4.1 240 31
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 4.2 240 36
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 4.3 250 37
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 4.2 250 35
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 4.3 250 38
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 4.1 240 32
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 4.6 250 34
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 4.1 240 34
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 4.6 290 35
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900   2400 13000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 5.2 290 41
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 4.5 280 35
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 4.2 250 36
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 4.1 250 34
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 4.0 240 35
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 4.2 250 33
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 4.3 240 32
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 4.7 280 38
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 4.0 240 37
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 4.2 250 33
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 4.7 280 38
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 4.1 250 37
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 6.8 350 44
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 250   2200 2700
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 4.2 240 33
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 4.0 240 37
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900   2500 15000
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 4.6 290 37
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 4.1 230 36
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 4.0 250 39
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 4.2 250 35
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 4.8 280 37
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 4.2 250 33
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 4.3 250 38
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 4.0 250 37
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 4.0 240 33
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 4.4 240 36
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 4.2 240 32
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 4.2 240 38
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 4.3 250 35
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 4.4 250 35
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 4.0 250 33
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 4.8 290 38
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 13   610 100
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 4.6 280 38
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 4.3 250 40
termination-crafted/easy2_false-no-overflow.c timeout 900   5300 13000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 4.5 260 36
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   1500 11000
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 4.8 280 40
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 6.8 330 60
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 5.5 290 49
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 5.5 300 42
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 5.8 300 50
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 24   800 220
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 4.1 240 37
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 5.3 300 43
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 5.1 280 43
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 6.4 300 51
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 7.6 390 50
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   1600 11000
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900   1300 12000
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 4.3 240 34
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   3900 13000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 6.4 310 51
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 7.2 320 55
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c true 16   640 140
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 44   1100 390
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 23   670 180
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 13   580 110
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c true 15   610 110
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c true 9.5 520 76
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c true 14   610 120
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 3.9 230 31
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true 5.8 300 46
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 6.8 360 60
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 4.9 290 38
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 4.9 300 44
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 5.0 280 41
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 5.6 300 46
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 4.7 280 36
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 4.0 240 35
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 4.2 240 31
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 4.8 290 39
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 7.4 350 60
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 4.7 290 40
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 5.1 290 38
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 4.8 280 40
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 4.4 250 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 6.3 290 47
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 4.3 250 35
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 5.2 290 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900   5300 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 4.7 280 40
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 4.7 290 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900   3000 15000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900   3800 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 4.4 250 34
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 4.2 250 32
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 4.9 280 42
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 4.7 290 37
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 4.7 290 40
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 4.3 250 39
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 4.4 250 32
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 4.5 290 34
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 4.3 250 37
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 4.5 260 38
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 4.2 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 4.5 280 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 4.3 240 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 4.4 290 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 4.1 240 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 4.1 240 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 4.3 240 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 4.6 280 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 4.1 240 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 4.2 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 4.2 240 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 4.1 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 4.3 240 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 4.3 240 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 5.3 290 43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 4.9 290 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 4.1 240 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 4.1 240 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 4.4 250 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 4.4 250 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 4.0 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 4.6 280 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 4.3 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 6.3 340 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 4.2 250 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 4.3 240 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 4.0 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 4.2 250 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 6.1 340 45
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 4.1 240 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 3.9 230 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 4.8 280 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 4.1 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 4.1 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 4.1 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 4.3 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 4.2 250 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 4.4 250 36
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 4.7 290 40
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 4.2 250 37
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 4.3 250 34
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 4.2 240 40
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 5.0 290 43
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 5.8 290 48
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 4.2 250 36
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 4.7 280 38
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 4.4 250 36
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 4.3 240 34
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 5.3 290 46
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 5.2 290 41
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 4.3 240 32
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 4.4 240 37
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 4.3 250 32
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 4.6 280 40
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 4.1 240 32
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 3.9 240 30
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 4.2 240 35
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 4.2 240 34
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 4.2 250 32
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 4.4 250 37
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 4.1 250 35
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 4.9 280 36
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 5.3 300 41
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 5.2 280 40
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 4.8 290 39
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 6.5 340 56
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 4.5 270 37
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 5.8 290 51
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 4.0 250 31
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 5.3 300 44
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 4.3 250 34
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900   3800 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 8.6 400 75
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 5.0 290 40
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 7.0 370 57
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 8.1 380 61
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 46   1400 450
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 10   490 76
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 51   1700 470
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 7.0 340 53
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 8.9 490 67
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 6.9 320 53
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 5.0 290 44
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 6.6 320 53
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 6.5 330 56
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 10   520 84
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 10   500 92
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 7.6 360 60
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 6.4 300 50
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900   4900 14000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 8.8 480 68
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 4.6 290 39
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900   5300 11000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900   3800 12000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 50   1500 500
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 4.0 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 4.8 290 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 5.7 300 46
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 5.0 280 43
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 5.2 300 47
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 5.2 290 38
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 5.7 300 45
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 5.7 310 44
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 6.0 300 53
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 120   4000 1500
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900   4800 13000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 4.9 290 40
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 8.6 470 76
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 4.7 290 34
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 7.4 330 53
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 4.6 290 38
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900   5400 11000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 4.6 290 35
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 7.0 360 45
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900   990 12000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 11   540 99
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c true 8.7 450 70
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 5.6 320 48
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 4.9 290 43
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 4.5 280 37
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 6.2 300 52
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 4.8 280 35
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 6.4 300 49
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 4.9 290 35
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 4.6 280 36
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 5.9 300 48
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 5.9 300 46
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 6.9 310 58
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 4.8 290 37
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 7.7 380 63
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 5.1 290 47
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 5.4 290 42
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 5.3 280 45
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 5.1 290 37
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 5.2 290 43
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 6.5 310 49
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 5.4 290 41
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 4.3 250 35
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 4.3 250 32
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 900   4800 12000
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 4.3 250 33
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 4.4 250 36
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 4.2 250 33
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 4.4 250 41
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 9.2 450 80
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c true 60   690 750
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 900   13000 5700
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 7.3 370 64
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c true 58   1600 420
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 5.1 290 45
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 900   1400 11000
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900   13000 6200
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 33   700 390
termination-numeric/gcd01_true-termination_true-no-overflow.c true 5.3 310 42
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 70   1300 690
termination-numeric/recHanoi02_true-termination_true-no-overflow.c timeout 900   2500 11000
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 900   5500 14000
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 900   5500 11000
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900   1300 13000
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 4.1 230 36
recursive/Addition03_false-no-overflow.c false(no-overflow) 4.1 240 39
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 4.8 290 39
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 910   13000 5800
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 910   13000 6500
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 910   13000 6600
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 910   13000 5400
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 900   4400 12000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 900   5100 12000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 900   2600 12000
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 4.4 250 35
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 7.3 380 60
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c true 7.7 380 55
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 900   5000 12000
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 900   13000 7200
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 63   1500 490
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c true 59   1500 450
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c true 58   1600 440
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 6.6 310 53
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 6.8 320 61
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c true 240   4800 2700
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 900   6800 12000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 5.7 300 49
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 32   820 270
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 910   13000 8900
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 900   2700 11000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 900   2500 11000
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 4.5 280 40
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 4.7 280 37
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 4.7 280 39
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 4.7 290 38
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 5.4 310 40
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 4.2 250 32
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 4.1 240 35
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 4.1 250 40
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 4.2 250 34
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 4.1 250 36
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 7.8 370 62
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 8.1 370 63
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 8.1 380 68
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 4.0 250 36
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 4.2 240 32
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 3.9 250 33
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 4.1 240 37
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 4.1 250 34
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 4.2 250 37
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 4.3 250 31
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 4.2 250 38
bitvector/byte_add_1_false-no-overflow.i error 110   4000 1100
bitvector/byte_add_2_false-no-overflow.i error 230   4600 2600
bitvector/byte_add_false-no-overflow.i error 160   2700 1800
bitvector/jain_1_false-no-overflow.i false(no-overflow) 4.2 240 38
bitvector/jain_2_false-no-overflow.i false(no-overflow) 4.2 240 39
bitvector/jain_4_false-no-overflow.i false(no-overflow) 4.4 250 40
bitvector/jain_5_false-no-overflow.i timeout 900   1500 13000
bitvector/jain_6_false-no-overflow.i false(no-overflow) 4.4 250 38
bitvector/jain_7_false-no-overflow.i false(no-overflow) 4.4 250 37
bitvector/modulus_false-no-overflow.i error 4.4 250 30
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 5.1 280 43
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 5.5 280 40
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 5.0 280 37
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 5.5 330 45
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 5.4 280 39
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 5.2 280 38
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 19   640 170
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 4.2 250 35
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 4.2 250 35
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 4.1 250 31
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 3.9 230 32
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 4.2 250 34
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 4.1 240 36
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 4.0 240 33
bitvector/modulus_true-unreach-call_true-no-overflow.i error 4.3 250 34
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i error 4.3 250 36
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i error 4.0 240 33
bitvector/parity_true-unreach-call_true-no-overflow.i true 4.2 250 34
bitvector/sum02_false-unreach-call_true-no-overflow.i true 4.3 240 35
bitvector/sum02_true-unreach-call_true-no-overflow.i true 4.2 250 34
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 38000 340000 460000
    correct results 301 2200 99000 20000
        correct true 138 1200 54000 11000
        correct false 163 980 45000 8700
    correct-unconfimed results 9 520 13000 4800
        correct-unconfirmed true 9 520 13000 4800
        correct-unconfirmed false 0
    incorrect results 1 60 690 750
        incorrect true 1 60 690 750
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]