Tool ULTIMATE Kojak 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-03 11:17:40 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
Options --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 4.3 240 36
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 4.4 260 38
signedintegeroverflow-regression/Division_false-no-overflow.c.i 4.4 250 35
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 4.2 250 37
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 4.1 240 35
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 4.5 270 35
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 4.2 250 38
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 4.4 250 34
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 4.2 240 37
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 4.6 240 42
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i 4.0 240 35
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i 4.4 260 36
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i 3.9 240 31
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i 4.0 230 31
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i 4.0 240 36
termination-crafted/2Nested_false-no-overflow.c 4.1 250 35
termination-crafted/4NestedWith3Variables_false-no-overflow.c 4.3 250 37
termination-crafted/Ackermann_false-no-overflow.c 4.3 250 38
termination-crafted/Bangalore_false-no-overflow.c 4.2 240 38
termination-crafted/Bangalore_v3_false-no-overflow.c 4.0 240 35
termination-crafted/Benghazi_nondet_false-no-overflow.c 4.2 250 37
termination-crafted/Binary_Search_false-no-overflow.c 4.3 260 38
termination-crafted/Cairo_nondet_false-no-overflow.c 5.3 290 40
termination-crafted/Cairo_step2_false-no-overflow.c 900   5200 12000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 4.2 250 36
termination-crafted/Copenhagen_disj_false-no-overflow.c 4.3 250 37
termination-crafted/Gothenburg_false-no-overflow.c 4.2 250 33
termination-crafted/Gothenburg_v2_false-no-overflow.c 4.4 250 33
termination-crafted/Hanoi_2vars_false-no-overflow.c 4.1 250 35
termination-crafted/Hanoi_3vars_false-no-overflow.c 4.3 250 38
termination-crafted/Hanoi_plus_false-no-overflow.c 4.3 250 41
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 6.9 370 51
termination-crafted/Mysore_false-no-overflow.c 4.2 250 39
termination-crafted/NestedRecursion_1a_false-no-overflow.c 4.4 250 39
termination-crafted/NestedRecursion_2a_false-no-overflow.c 4.3 250 36
termination-crafted/NonTermination1_false-no-overflow.c 4.2 240 38
termination-crafted/NonTermination2_false-no-overflow.c 4.1 250 38
termination-crafted/NonTermination4_false-no-overflow.c 350   4900 4900
termination-crafted/NonTerminationSimple2_false-no-overflow.c 4.3 240 34
termination-crafted/NonTerminationSimple3_false-no-overflow.c 4.0 240 35
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   5200 13000
termination-crafted/NonTerminationSimple5_false-no-overflow.c 4.3 250 37
termination-crafted/NonTerminationSimple6_false-no-overflow.c 4.1 240 36
termination-crafted/NonTerminationSimple8_false-no-overflow.c 4.1 250 39
termination-crafted/NonTerminationSimple9_false-no-overflow.c 4.1 240 36
termination-crafted/Pure2Phase_false-no-overflow.c 4.5 250 39
termination-crafted/Pure3Phase_false-no-overflow.c 4.5 250 34
termination-crafted/RecursiveMultiplication_false-no-overflow.c 4.2 250 38
termination-crafted/RecursiveNonterminating_false-no-overflow.c 4.0 250 32
termination-crafted/Rotation180_false-no-overflow.c 4.2 250 36
termination-crafted/Singapore_false-no-overflow.c 4.3 250 34
termination-crafted/Singapore_plus_false-no-overflow.c 4.4 250 38
termination-crafted/Singapore_v1_false-no-overflow.c 4.3 250 36
termination-crafted/Singapore_v2_false-no-overflow.c 4.2 250 34
termination-crafted/Stockholm_false-no-overflow.c 4.2 250 41
termination-crafted/Thun_false-no-overflow.c 4.3 250 33
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 4.5 250 41
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 12   540 120
termination-crafted/aaron2_false-no-overflow.c 4.1 250 36
termination-crafted/aaron3_false-no-overflow.c 4.2 250 39
termination-crafted/easy2_false-no-overflow.c 900   7000 13000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 4.6 260 42
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 900   5200 14000
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 4.5 260 42
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 7.0 470 63
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 7.0 460 58
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 6.2 420 59
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 5.3 290 40
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900   5700 12000
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 4.0 240 32
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 4.9 270 44
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 5.1 270 41
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 6.8 420 51
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 5.8 310 45
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 900   5300 15000
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900   6200 11000
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 3.9 230 35
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900   5300 14000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 6.6 400 52
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 18   670 170
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 900   1200 14000
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900   1200 12000
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900   1500 13000
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 900   1600 14000
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 900   1800 11000
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 900   2000 11000
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 900   5000 12000
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 4.0 240 40
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 6.4 380 52
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 6.3 390 55
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 6.1 380 52
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 6.0 340 50
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 5.8 320 50
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 6.5 380 62
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 5.1 260 47
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 3.8 240 31
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 3.8 230 33
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 5.7 310 45
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 900   7100 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 4.7 260 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 4.9 260 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 4.3 250 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 4.3 250 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 6.2 380 59
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 4.6 250 44
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 5.9 340 51
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 900   7000 10000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 5.9 320 52
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 4.5 250 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 900   6000 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 900   6700 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 4.3 250 35
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 4.1 250 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 5.5 310 48
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 4.7 270 39
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 4.6 250 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 4.3 250 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 4.6 250 35
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 4.3 240 37
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 4.2 260 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 4.3 260 34
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 4.4 260 42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 4.3 250 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 4.3 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 4.4 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 4.2 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 4.2 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 4.2 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 4.3 250 40
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 4.3 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 4.2 250 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 4.3 240 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 4.1 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 4.0 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 4.2 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 5.2 290 42
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 5.7 330 45
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 4.3 250 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 4.3 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 4.4 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 4.2 250 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 4.2 240 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 4.4 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 4.3 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 4.2 240 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 4.4 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 4.2 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 4.2 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 4.3 250 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 4.1 250 40
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 4.7 260 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 4.2 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 4.5 260 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 4.5 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 4.2 250 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 4.4 250 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 4.2 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 4.2 250 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 4.2 260 35
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 5.6 300 48
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 4.2 250 34
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 4.2 250 33
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 4.3 250 35
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 4.9 270 42
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 9.9 480 81
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 4.2 250 40
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 4.9 260 38
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 4.3 250 36
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 4.3 240 38
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 5.7 320 46
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 5.5 320 43
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 4.3 250 39
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 4.4 250 38
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 4.2 250 33
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 4.5 250 36
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 4.1 250 32
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 4.0 250 31
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 6.1 340 46
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 4.1 250 38
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 4.1 250 32
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 4.2 250 38
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 4.3 250 37
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 5.4 270 43
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 6.2 350 51
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 6.1 340 52
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 6.1 340 44
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 4.3 250 37
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 4.3 250 33
termination-crafted-lit/cstrncmp_false-no-overflow.c 6.4 350 54
termination-crafted-lit/gcd1_false-no-overflow.c 4.2 250 37
termination-crafted-lit/joey_false-no-overflow.c 5.3 300 48
termination-crafted-lit/min_rf_false-no-overflow.c 4.4 250 40
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900   6300 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 6.8 470 61
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 5.6 310 45
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900   7100 14000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 7.6 490 68
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 120   2300 1700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900   6600 15000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 900   6400 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 7.5 470 69
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 16   700 160
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 8.5 530 83
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 7.2 440 60
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 7.6 480 68
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 14   630 120
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900   6700 11000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 13   590 130
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 19   690 190
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 14   580 120
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900   6100 13000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 93   2000 1000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 5.6 310 46
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900   7100 14000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900   6700 14000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 900   6400 12000
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 4.1 230 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 5.1 280 46
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 5.8 320 50
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 6.5 380 57
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 8.5 470 78
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 7.5 470 64
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 6.8 460 57
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 6.0 310 47
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 6.7 450 57
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 900   6300 13000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   6400 12000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 5.7 310 47
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 100   2300 1300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 5.1 280 41
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 13   570 120
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 5.3 290 45
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900   5200 13000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 4.7 260 39
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 6.2 380 50
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   6000 12000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 9.3 520 86
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 900   5600 14000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 11   520 100
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 6.8 470 56
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 4.9 270 42
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 7.0 470 63
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 4.6 260 39
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 7.0 480 64
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 6.0 340 52
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 4.4 260 39
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 6.6 420 51
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 6.9 430 57
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 7.8 470 68
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 4.8 260 37
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 900   5800 12000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 5.4 300 50
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 5.7 310 54
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 5.5 300 40
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 5.5 310 47
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 5.6 300 45
termination-crafted-lit/genady_true-termination_true-no-overflow.c 36   1000 410
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 5.7 320 48
termination-numeric/Addition01_false-no-overflow.c 4.4 260 37
termination-numeric/Avg_true_false-no-overflow.c 4.4 260 38
termination-numeric/Binomial_true-termination_false-no-overflow.c 900   2300 8700
termination-numeric/Et1_true_false-no-overflow.c 4.2 250 35
termination-numeric/Et2_true_false-no-overflow.c 4.2 250 36
termination-numeric/Et3_true_false-no-overflow.c 4.4 250 36
termination-numeric/Et4_true_false-no-overflow.c 4.4 250 36
termination-numeric/MultCommutative_false-no-overflow.c 11   600 120
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 900   2100 10000
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 900   1700 11000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900   5000 12000
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 900   1500 10000
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 7.6 490 65
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900   5300 12000
termination-numeric/Parts_true-termination_true-no-overflow.c 900   1900 11000
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900   2500 9500
termination-numeric/gcd01_true-termination_true-no-overflow.c 8.4 470 73
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 170   4700 2200
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 900   4600 13000
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900   5700 15000
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900   5800 12000
termination-numeric/twisted_true-termination_true-no-overflow.c 900   5600 12000
recursive/Addition02WithOverflowBug_false-no-overflow.c 4.4 250 40
recursive/Addition03_false-no-overflow.c 4.5 260 39
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 4.6 270 42
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 900   1700 11000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 900   1800 13000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 900   1700 10000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 900   1700 11000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 900   6000 15000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900   6000 12000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 900   5800 14000
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 4.2 250 31
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 900   4800 13000
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 900   5200 9700
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 900   1300 11000
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 900   1400 11000
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 900   1300 12000
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 900   1500 11000
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 900   1600 11000
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 7.0 440 56
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 7.1 430 60
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 900   2000 13000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 900   1500 12000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 8.3 480 70
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 14   640 130
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 900   2900 11000
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 900   4700 13000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 900   4600 14000
recursive-simple/id_b3_o2_false-no-overflow.c 4.5 270 45
recursive-simple/id_b3_o5_false-no-overflow.c 4.4 260 34
recursive-simple/id_b5_o10_false-no-overflow.c 4.7 260 36
recursive-simple/sum_non_eq_false-no-overflow.c 4.7 260 37
recursive-simple/sum_non_false-no-overflow.c 5.8 330 49
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 4.1 250 32
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 4.4 250 39
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 4.1 250 32
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 4.1 240 36
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 4.2 240 33
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 6.3 350 47
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 6.5 350 52
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 6.7 360 51
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 4.2 240 37
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 4.2 240 35
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 4.0 240 38
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 3.9 240 34
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 4.2 240 36
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 3.9 230 32
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 4.0 240 34
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 4.0 250 35
bitvector/byte_add_1_false-no-overflow.i 900   1200 11000
bitvector/byte_add_2_false-no-overflow.i 900   1300 12000
bitvector/byte_add_false-no-overflow.i 900   1200 12000
bitvector/jain_1_false-no-overflow.i 4.4 250 35
bitvector/jain_2_false-no-overflow.i 4.1 250 32
bitvector/jain_4_false-no-overflow.i 4.3 250 37
bitvector/jain_5_false-no-overflow.i 900   6000 13000
bitvector/jain_6_false-no-overflow.i 6.6 350 51
bitvector/jain_7_false-no-overflow.i 4.3 250 34
bitvector/modulus_false-no-overflow.i 4.3 250 36
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 7.4 370 61
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 7.3 370 60
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 7.4 370 59
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 5.2 300 43
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 5.7 330 45
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 5.9 330 49
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 33   1100 360
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 4.2 250 39
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 3.9 230 32
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 4.2 240 38
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 3.9 240 31
bitvector/jain_5_true-unreach-call_true-no-overflow.i 4.4 250 33
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 4.1 240 33
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 4.1 250 36
bitvector/modulus_true-unreach-call_true-no-overflow.i 4.3 250 35
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 4.3 250 38
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 4.1 250 35
bitvector/parity_true-unreach-call_true-no-overflow.i 4.1 240 35
bitvector/sum02_false-unreach-call_true-no-overflow.i 4.3 240 36
bitvector/sum02_true-unreach-call_true-no-overflow.i 4.3 240 34
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 65000 400000 860000
    correct results 285 2400 100000 25000
        correct true 122 1300 54000 13000
        correct false 163 1100 48000 11000
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]