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