Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017
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-02 00:52:46 CET
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i .32  11 3.7 
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i .32  12 3.8 
signedintegeroverflow-regression/Division_false-no-overflow.c.i .30  12 4.2 
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i .31  11 2.7 
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i .30  11 3.5 
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i .32  11 3.4 
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i .32  12 3.2 
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i .29  11 4.2 
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i .30  12 4.0 
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i .32  11 3.5 
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i .32  11 3.6 
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i .30  11 4.5 
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i .32  11 3.7 
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i .29  11 3.9 
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i .29  12 4.5 
termination-crafted/2Nested_false-no-overflow.c .69  12 8.0 
termination-crafted/4NestedWith3Variables_false-no-overflow.c 1.1   13 13   
termination-crafted/Ackermann_false-no-overflow.c .50  12 5.7 
termination-crafted/Bangalore_false-no-overflow.c .60  13 7.4 
termination-crafted/Bangalore_v3_false-no-overflow.c .75  13 9.3 
termination-crafted/Benghazi_nondet_false-no-overflow.c .68  12 9.7 
termination-crafted/Binary_Search_false-no-overflow.c .58  12 6.8 
termination-crafted/Cairo_nondet_false-no-overflow.c .67  12 8.9 
termination-crafted/Cairo_step2_false-no-overflow.c 900     1100 11000   
termination-crafted/Collatz_unknown-termination_false-no-overflow.c .43  12 5.1 
termination-crafted/Copenhagen_disj_false-no-overflow.c .49  12 5.7 
termination-crafted/Gothenburg_false-no-overflow.c 3.6   14 43   
termination-crafted/Gothenburg_v2_false-no-overflow.c .41  12 4.5 
termination-crafted/Hanoi_2vars_false-no-overflow.c 26     15000 390   
termination-crafted/Hanoi_3vars_false-no-overflow.c .68  13 8.4 
termination-crafted/Hanoi_plus_false-no-overflow.c .99  13 12   
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c .42  12 5.6 
termination-crafted/Mysore_false-no-overflow.c .83  12 10   
termination-crafted/NestedRecursion_1a_false-no-overflow.c .35  12 4.3 
termination-crafted/NestedRecursion_2a_false-no-overflow.c .38  11 3.4 
termination-crafted/NonTermination1_false-no-overflow.c .39  12 4.8 
termination-crafted/NonTermination2_false-no-overflow.c .48  12 5.3 
termination-crafted/NonTermination4_false-no-overflow.c .30  11 3.8 
termination-crafted/NonTerminationSimple2_false-no-overflow.c .41  12 5.5 
termination-crafted/NonTerminationSimple3_false-no-overflow.c .58  13 8.0 
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900     83 4200   
termination-crafted/NonTerminationSimple5_false-no-overflow.c .42  12 4.8 
termination-crafted/NonTerminationSimple6_false-no-overflow.c 26     15000 370   
termination-crafted/NonTerminationSimple8_false-no-overflow.c .44  12 5.3 
termination-crafted/NonTerminationSimple9_false-no-overflow.c 26     15000 360   
termination-crafted/Pure2Phase_false-no-overflow.c .43  12 5.5 
termination-crafted/Pure3Phase_false-no-overflow.c 1.6   13 22   
termination-crafted/RecursiveMultiplication_false-no-overflow.c .80  12 12   
termination-crafted/RecursiveNonterminating_false-no-overflow.c .33  11 3.6 
termination-crafted/Rotation180_false-no-overflow.c 890     11 14000   
termination-crafted/Singapore_false-no-overflow.c .60  13 7.8 
termination-crafted/Singapore_plus_false-no-overflow.c .64  12 7.6 
termination-crafted/Singapore_v1_false-no-overflow.c .68  12 8.4 
termination-crafted/Singapore_v2_false-no-overflow.c .69  12 8.1 
termination-crafted/Stockholm_false-no-overflow.c 1.8   13 22   
termination-crafted/Thun_false-no-overflow.c 1.1   13 16   
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c .95  12 13   
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 1.4   12 19   
termination-crafted/aaron2_false-no-overflow.c .93  13 12   
termination-crafted/aaron3_false-no-overflow.c .79  13 10   
termination-crafted/easy2_false-no-overflow.c 900     300 11000   
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c .34  11 3.5 
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 890     100 12000   
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 900     32 11000   
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 3.0   140 33   
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 900     60 10000   
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 900     58 12000   
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c .49  12 5.2 
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900     930 12000   
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 900     1200 11000   
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 900     1100 11000   
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 900     1200 12000   
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 900     1100 9900   
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 900     26 12000   
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 900     1900 11000   
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900     1900 12000   
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 890     11 12000   
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900     110 13000   
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 900     140 11000   
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 900     940 12000   
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 900     600 12000   
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900     260 11000   
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900     460 12000   
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 900     460 10000   
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 900     490 13000   
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 900     2400 9200   
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 900     1600 10000   
termination-crafted/NonTermination3_true-no-overflow_false-termination.c .41  12 5.0 
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 890     11 12000   
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 900     650 13000   
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 900     250 11000   
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 900     140 11000   
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 900     460 11000   
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 900     440 12000   
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 900     260 11000   
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c .29  11 3.5 
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 890     11 12000   
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c .38  11 4.3 
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 900     310 9900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c .41  12 6.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c .43  12 6.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c .92  13 13   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c .82  13 10   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c .68  13 7.9 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c .72  12 7.8 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 1.2   13 16   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 900     270 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c .53  13 6.5 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c .30  11 3.6 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 890     620 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 900     350 14000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c .40  12 5.0 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 31     15000 470   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c .50  13 6.5 
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c .61  12 8.0 
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 25     15000 310   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 1.9   20 22   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c .68  12 8.2 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c .98  13 11   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c .81  13 9.6 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c .82  12 11   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 26     15000 360   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c .48  12 6.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 1.1   12 16   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c .37  11 4.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c .38  12 4.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c .36  12 4.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c .54  13 7.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c .58  12 7.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c .52  12 7.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c .93  13 13   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 27     15000 360   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 1.1   12 14   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c .58  12 7.8 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c .72  12 9.7 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 1.0   13 12   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c .49  12 6.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c .87  12 10   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 1.3   13 19   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c .73  12 9.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c .58  12 6.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c .54  12 6.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c .40  12 5.3 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c .44  11 6.0 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c .69  12 9.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c .86  12 9.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c .51  12 6.9 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c .44  12 6.1 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 1.1   13 13   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c .70  15 8.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c .96  13 13   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c .81  13 9.6 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c .68  12 9.5 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 1.7   13 23   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c .85  14 10   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c .78  12 8.4 
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 1.6   14 19   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 1.1   13 13   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c .49  13 5.8 
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c .48  13 5.6 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c .46  12 4.9 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c .49  12 7.0 
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 26     15000 330   
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c .57  12 7.9 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 3.4   15 46   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c .46  12 5.2 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c .052 11 .34
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c .52  12 6.5 
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c .54  12 7.7 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c .41  12 5.9 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c .62  12 6.6 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c .47  12 5.5 
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c .48  12 6.4 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c .53  12 6.1 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c .44  12 4.8 
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c .56  13 6.4 
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 26     15000 350   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c .54  12 7.3 
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c .58  12 7.3 
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c .55  12 7.2 
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c .71  12 8.3 
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c .57  12 6.9 
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c .82  13 10   
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c .52  12 5.1 
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c .48  12 5.5 
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c .50  12 5.5 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c .55  12 6.1 
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c .48  14 5.7 
termination-crafted-lit/cstrncmp_false-no-overflow.c .064 11 .48
termination-crafted-lit/gcd1_false-no-overflow.c 900     120 12000   
termination-crafted-lit/joey_false-no-overflow.c .43  12 5.1 
termination-crafted-lit/min_rf_false-no-overflow.c 1.1   13 16   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900     650 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 900     340 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c .39  11 4.3 
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900     300 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 900     160 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900     640 12000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900     370 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 900     1800 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 900     250 9900   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 900     660 13000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 900     120 10000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 900     230 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 900     310 11000   
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 900     210 12000   
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900     240 11000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 900     75 11000   
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 900     72 12000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 900     500 10000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900     130 10000   
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 900     300 9900   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c .36  11 4.5 
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900     270 11000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900     440 10000   
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 900     1900 13000   
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 890     31 12000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 900     100 11000   
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 900     160 13000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 900     360 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 900     240 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 900     480 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 900     27 11000   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 900     670 9500   
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 900     31 12000   
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c .33  11 3.9 
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900     520 11000   
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 900     290 12000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900     660 13000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 900     260 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 900     940 11000   
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 890     84 12000   
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 890     180 10000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 900     480 11000   
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 900     360 9800   
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900     51 14000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 900     500 11000   
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 900     710 9400   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 900     71 11000   
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 900     190 11000   
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 1.8   12 24   
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 900     170 10000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 900     280 11000   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 890     480 9800   
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 900     370 12000   
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 900     12 12000   
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 890     330 9100   
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 900     760 13000   
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 900     370 11000   
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c .30  11 3.4 
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 900     290 10000   
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c .074 11 .37
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c .073 11 .34
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c .074 11 .37
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c .061 11 .50
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c .071 11 .40
termination-crafted-lit/genady_true-termination_true-no-overflow.c .40  11 4.7 
termination-crafted-lit/strchr_true-no-overflow_true-termination.c .067 11 .45
termination-numeric/Addition01_false-no-overflow.c .45  12 5.9 
termination-numeric/Avg_true_false-no-overflow.c .65  12 7.4 
termination-numeric/Binomial_true-termination_false-no-overflow.c 1.1   12 13   
termination-numeric/Et1_true_false-no-overflow.c 1.3   13 16   
termination-numeric/Et2_true_false-no-overflow.c 1.1   13 15   
termination-numeric/Et3_true_false-no-overflow.c 1.2   13 17   
termination-numeric/Et4_true_false-no-overflow.c .98  13 12   
termination-numeric/MultCommutative_false-no-overflow.c .65  12 6.9 
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 41     39 580   
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 890     17 13000   
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900     770 10000   
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 900     1400 11000   
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 890     380 12000   
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 35     170 440   
termination-numeric/Parts_true-termination_true-no-overflow.c 900     350 12000   
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900     790 8500   
termination-numeric/gcd01_true-termination_true-no-overflow.c 900     89 11000   
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 1.9   12 26   
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 2.1   13 27   
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900     2100 9600   
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900     1900 9300   
termination-numeric/twisted_true-termination_true-no-overflow.c 900     670 11000   
recursive/Addition02WithOverflowBug_false-no-overflow.c .43  12 5.7 
recursive/Addition03_false-no-overflow.c .42  12 5.4 
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c .37  12 4.7 
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 890     17 12000   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 890     19 14000   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 890     18 12000   
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 890     18 12000   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 890     650 9400   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900     640 10000   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c .076 11 .38
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c .38  11 5.5 
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 890     850 12000   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 890     830 11000   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 890     13 13000   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c .29  11 3.2 
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 890     13 13000   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 900     1400 11000   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 900     1300 12000   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 900     140 11000   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 900     160 10000   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 890     80 12000   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 900     53 13000   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 900     88 13000   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 890     36 12000   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 890     13 12000   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2.1   12 27   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 2.1   13 27   
recursive-simple/id_b3_o2_false-no-overflow.c .37  12 4.8 
recursive-simple/id_b3_o5_false-no-overflow.c .37  12 4.0 
recursive-simple/id_b5_o10_false-no-overflow.c .38  12 4.0 
recursive-simple/sum_non_eq_false-no-overflow.c .41  12 4.4 
recursive-simple/sum_non_false-no-overflow.c .47  12 6.2 
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 900     690 10000   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 900     660 12000   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 900     700 11000   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 890     660 8300   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 890     1200 8500   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c .38  12 4.2 
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c .36  12 5.1 
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c .37  12 5.6 
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 890     1000 8900   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 890     1100 9100   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 890     1100 9600   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 890     1000 8100   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 900     1100 8800   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 900     1000 9600   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 900     740 9200   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 890     730 8800   
bitvector/byte_add_1_false-no-overflow.i 4.1   13 49   
bitvector/byte_add_2_false-no-overflow.i 4.1   13 49   
bitvector/byte_add_false-no-overflow.i 39     17 440   
bitvector/jain_1_false-no-overflow.i .44  12 5.1 
bitvector/jain_2_false-no-overflow.i .70  12 9.5 
bitvector/jain_4_false-no-overflow.i .59  12 8.2 
bitvector/jain_5_false-no-overflow.i 2.3   11 29   
bitvector/jain_6_false-no-overflow.i .72  12 8.0 
bitvector/jain_7_false-no-overflow.i .70  12 8.5 
bitvector/modulus_false-no-overflow.i .35  12 4.5 
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 4.1   13 48   
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 4.1   13 55   
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 38     18 460   
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .66  12 8.4 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 28     18 380   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 30     17 380   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i .078 11 .36
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i .37  11 3.7 
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 900     92 9600   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 900     120 7600   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 890     120 12000   
bitvector/jain_5_true-unreach-call_true-no-overflow.i 890     11 11000   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i .48  12 5.7 
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i .49  12 6.5 
bitvector/modulus_true-unreach-call_true-no-overflow.i 790     64 12000   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i .33  11 3.9 
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i .30  11 3.5 
bitvector/parity_true-unreach-call_true-no-overflow.i 9.4   13 120   
bitvector/sum02_false-unreach-call_true-no-overflow.i 900     670 11000   
bitvector/sum02_true-unreach-call_true-no-overflow.i .065 11 .53
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 130000   210000 1600000
    correct results 157 220   1900 2700
        correct true 26 120   320 1600
        correct false 131 94   1600 1200
    correct-unconfimed results 21 880   490 13000
        correct-unconfirmed true 6 830   280 13000
        correct-unconfirmed false 15 49   210 670
    incorrect results 10 50   130 580
        incorrect true 5 48   67 560
        incorrect false 5 2.1 59 27
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]