Tool ULTIMATE Automizer 0.1.23-635dfa2a
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-08 07:42:40 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.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) 8.7 370 70
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 9.2 380 62
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 8.4 360 65
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 7.7 340 59
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 7.9 340 64
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 8.9 370 68
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 8.9 370 62
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 9.0 380 65
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 8.9 370 63
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 9.2 380 78
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 7.1 330 60
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 8.7 380 71
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 8.8 370 64
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 8.3 350 62
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 8.7 370 64
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 7.7 360 61
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 7.8 370 64
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 7.2 360 56
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 7.6 360 65
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 7.3 340 55
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 7.8 370 61
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 7.5 370 60
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 7.7 350 58
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900   1200 14000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 7.3 330 65
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 7.2 340 56
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 7.8 350 58
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 7.4 350 61
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 7.4 360 58
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 7.2 340 63
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 7.1 340 55
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 8.2 370 67
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 7.6 370 66
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 8.3 360 64
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 7.8 360 62
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 6.4 340 57
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 7.9 360 67
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 27   800 270
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 7.6 350 57
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 8.6 370 64
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900   1200 13000
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 7.1 340 56
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 6.4 330 54
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 8.1 360 62
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 7.6 360 63
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 7.9 370 65
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 7.2 340 60
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 6.7 330 52
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 7.2 330 63
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 8.0 370 63
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 8.0 370 58
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 7.8 360 63
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 7.2 350 59
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 7.9 370 63
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 7.8 370 61
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 7.8 370 61
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 7.4 340 50
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 16   540 140
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 7.7 360 53
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 7.7 370 65
termination-crafted/easy2_false-no-overflow.c timeout 900   2600 11000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 7.4 350 59
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 28   620 250
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c true 8.0 350 65
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 9.8 390 70
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 9.0 350 64
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 9.1 380 65
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 8.2 360 73
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 81   620 1000
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 6.8 320 55
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 8.4 360 70
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 8.1 350 59
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 8.6 350 66
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 7.2 350 56
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   990 10000
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900   1000 13000
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 7.0 340 57
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   1900 13000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 11   380 84
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 12   550 100
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c true 12   510 91
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 21   730 170
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 16   570 120
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 13   570 99
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c true 15   550 130
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c true 13   490 120
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c true 17   520 160
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 8.1 340 61
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true 9.1 370 72
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 8.5 360 70
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 8.6 370 66
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 8.1 370 60
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 7.7 360 65
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 9.0 360 76
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 7.6 350 69
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 7.4 360 60
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 7.7 370 62
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 7.3 340 56
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900   3100 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 8.2 370 69
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 8.4 370 69
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 7.8 370 60
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 8.2 370 60
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 9.2 380 70
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 7.4 340 67
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 8.4 360 71
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900   2500 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 7.6 360 63
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 8.5 370 71
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900   1300 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900   8200 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 8.1 370 65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 7.5 360 61
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 8.2 360 61
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 7.7 340 59
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 8.2 380 58
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 6.8 360 60
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 8.0 360 58
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 7.6 350 65
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 7.1 340 53
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 8.3 380 61
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 7.2 350 56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 8.2 370 57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 7.6 360 57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 8.4 370 69
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 8.1 370 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 8.0 370 56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 7.5 350 64
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 8.1 380 67
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 8.1 360 60
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 7.4 350 57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 7.8 370 63
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 7.9 370 67
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 7.7 350 61
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 8.0 370 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 8.7 360 67
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 8.6 350 78
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 7.8 370 61
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 6.8 340 61
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 7.7 340 59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 7.9 350 59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 7.7 370 61
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 7.4 350 64
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 7.0 360 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 7.5 340 58
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 7.8 360 60
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 7.2 330 52
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 7.6 350 60
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 6.6 330 57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 6.6 340 53
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 7.7 370 64
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 7.2 340 57
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 8.4 360 62
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 7.7 350 62
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 7.1 330 59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 7.8 370 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 7.8 360 60
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 7.8 360 56
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 7.9 360 65
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 8.4 370 62
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 7.4 340 64
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 8.0 360 57
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 7.5 350 62
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 8.3 360 62
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 10   390 78
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 6.7 330 55
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 11   450 84
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 7.6 340 56
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 8.2 360 61
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 8.7 380 69
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 8.3 350 74
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 7.3 350 64
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 8.4 360 62
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 7.2 340 63
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 7.9 340 54
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 7.8 360 62
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 7.7 360 64
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 7.1 350 60
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 7.9 370 56
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 7.6 370 66
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 7.7 350 59
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 7.6 360 58
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 8.9 360 74
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 8.3 360 64
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 8.4 380 72
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 8.3 360 66
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 8.0 360 60
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 6.7 330 61
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 9.1 370 69
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 7.4 360 57
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 8.6 370 64
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 8.1 360 56
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900   1500 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 8.5 370 65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 8.1 370 65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900   2500 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 8.2 340 65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 19   550 150
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900   5400 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 180   4700 2100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 9.4 380 81
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 10   420 77
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 8.7 360 70
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 7.6 360 63
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 7.4 330 65
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 10   410 75
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900   1800 12000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 11   510 83
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 11   490 90
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 9.7 380 72
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 900   2000 13000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 12   500 92
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 8.2 380 71
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900   3200 14000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900   7800 8400
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 180   4800 2000
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 7.6 350 55
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 8.0 370 59
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 8.6 380 69
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 8.5 360 67
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 8.2 350 66
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 8.8 370 65
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 8.7 370 69
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 8.2 360 60
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 8.3 340 70
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 120   1400 1300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900   2900 12000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 8.5 360 68
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 10   490 78
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 7.2 340 52
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 8.8 360 64
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 8.4 370 59
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900   4100 10000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 6.8 340 58
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 8.7 380 72
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 12   500 88
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c true 19   730 150
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 8.1 360 62
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 8.6 380 61
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 8.0 360 66
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 8.1 340 64
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 8.2 370 74
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 9.6 380 71
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 8.0 360 63
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 8.4 360 63
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 9.0 380 69
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 9.0 370 75
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 8.6 350 72
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 8.4 370 58
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout 900   7100 7500
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 8.9 360 70
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 8.7 370 72
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 7.9 350 61
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 8.6 340 70
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 7.5 340 65
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 11   510 86
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 9.1 380 66
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 7.6 370 58
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 7.3 340 59
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 900   930 11000
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 7.6 350 63
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 7.4 350 58
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 7.9 370 69
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 8.2 370 57
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 11   510 85
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 900   1100 7000
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 900   8900 7200
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 13   530 110
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 900   6600 11000
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 8.6 360 67
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 900   770 12000
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900   4600 13000
termination-numeric/TwoWay_true-termination_true-no-overflow.c true 16   610 140
termination-numeric/gcd01_true-termination_true-no-overflow.c true 9.5 370 69
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 49   990 490
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 66   1100 650
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 900   4400 9600
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 900   4600 9600
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900   1000 11000
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 8.5 360 67
recursive/Addition03_false-no-overflow.c false(no-overflow) 7.9 360 63
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 8.3 370 62
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 900   6800 10000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 900   8300 7100
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 900   8000 6800
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 900   6600 8300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 900   2800 11000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 900   2600 13000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 900   1500 13000
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 8.2 360 59
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 14   490 110
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c true 14   520 120
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 900   5500 12000
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 31   1100 300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 900   5800 11000
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 900   5400 12000
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 900   5600 14000
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 9.3 390 80
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 9.8 390 75
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 900   960 6800
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 900   950 8000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 8.8 370 72
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 15   610 120
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 900   2000 10000
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 63   1200 620
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 64   1000 660
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 7.2 330 57
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 8.1 370 64
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 8.1 370 59
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 8.6 360 63
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 8.7 380 62
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 7.1 350 54
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 8.1 360 55
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 7.7 350 68
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 8.2 370 65
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 7.9 350 58
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 8.3 370 62
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 8.6 360 64
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 9.0 370 75
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 6.9 320 50
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 7.2 350 54
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 7.4 350 57
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 6.6 330 57
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 7.2 350 60
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 7.1 330 62
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 8.0 360 60
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 8.4 370 67
bitvector/byte_add_1_false-no-overflow.i error 29   610 280
bitvector/byte_add_2_false-no-overflow.i error 31   750 250
bitvector/byte_add_false-no-overflow.i error 42   630 400
bitvector/jain_1_false-no-overflow.i false(no-overflow) 7.3 360 51
bitvector/jain_2_false-no-overflow.i false(no-overflow) 7.7 360 57
bitvector/jain_4_false-no-overflow.i false(no-overflow) 8.0 360 57
bitvector/jain_5_false-no-overflow.i timeout 900   1500 9300
bitvector/jain_6_false-no-overflow.i false(no-overflow) 7.2 350 56
bitvector/jain_7_false-no-overflow.i false(no-overflow) 7.3 340 60
bitvector/modulus_false-no-overflow.i error 8.5 360 60
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 9.3 380 69
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 9.3 380 70
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 7.9 340 66
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 8.6 380 74
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 8.9 370 76
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 8.8 370 65
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 15   510 130
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 7.6 370 63
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 8.0 370 59
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 7.3 340 55
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 7.3 330 59
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 7.3 330 54
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 7.4 350 62
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 8.3 360 58
bitvector/modulus_true-unreach-call_true-no-overflow.i error 7.7 360 66
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i error 7.9 360 61
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i error 6.9 340 58
bitvector/parity_true-unreach-call_true-no-overflow.i true 7.7 330 50
bitvector/sum02_false-unreach-call_true-no-overflow.i true 7.8 360 68
bitvector/sum02_true-unreach-call_true-no-overflow.i true 7.7 370 60
psyco/psyco_abp_1_false-no-overflow.c timeout 900   5800 13000
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 45000 300000 530000
    correct results 306 3400 130000 30000
        correct true 143 2100 70000 19000
        correct false 163 1300 59000 10000
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]