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