Tool ULTIMATE Automizer 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.1 240 32
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 4.8 260 40
signedintegeroverflow-regression/Division_false-no-overflow.c.i 4.1 240 38
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 4.2 240 37
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 4.1 230 32
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 4.7 270 44
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 4.2 240 39
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 4.5 270 38
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 4.1 250 36
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 4.1 240 35
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i 4.0 240 34
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i 4.6 290 38
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i 4.0 230 34
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i 4.1 240 35
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i 4.4 240 34
termination-crafted/2Nested_false-no-overflow.c 6.1 340 49
termination-crafted/4NestedWith3Variables_false-no-overflow.c 4.1 250 38
termination-crafted/Ackermann_false-no-overflow.c 4.0 240 38
termination-crafted/Bangalore_false-no-overflow.c 4.0 240 37
termination-crafted/Bangalore_v3_false-no-overflow.c 4.2 240 36
termination-crafted/Benghazi_nondet_false-no-overflow.c 4.0 230 36
termination-crafted/Binary_Search_false-no-overflow.c 4.2 250 34
termination-crafted/Cairo_nondet_false-no-overflow.c 4.4 280 36
termination-crafted/Cairo_step2_false-no-overflow.c 900   4400 14000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 5.0 290 40
termination-crafted/Copenhagen_disj_false-no-overflow.c 4.4 270 36
termination-crafted/Gothenburg_false-no-overflow.c 4.2 250 37
termination-crafted/Gothenburg_v2_false-no-overflow.c 4.3 250 38
termination-crafted/Hanoi_2vars_false-no-overflow.c 4.0 240 35
termination-crafted/Hanoi_3vars_false-no-overflow.c 4.2 240 36
termination-crafted/Hanoi_plus_false-no-overflow.c 4.3 230 39
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 4.4 270 35
termination-crafted/Mysore_false-no-overflow.c 6.3 340 47
termination-crafted/NestedRecursion_1a_false-no-overflow.c 4.2 250 35
termination-crafted/NestedRecursion_2a_false-no-overflow.c 4.5 280 44
termination-crafted/NonTermination1_false-no-overflow.c 3.9 240 34
termination-crafted/NonTermination2_false-no-overflow.c 4.1 240 37
termination-crafted/NonTermination4_false-no-overflow.c 23   780 200
termination-crafted/NonTerminationSimple2_false-no-overflow.c 4.0 230 36
termination-crafted/NonTerminationSimple3_false-no-overflow.c 4.2 240 38
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   3900 15000
termination-crafted/NonTerminationSimple5_false-no-overflow.c 4.5 280 37
termination-crafted/NonTerminationSimple6_false-no-overflow.c 4.0 240 36
termination-crafted/NonTerminationSimple8_false-no-overflow.c 6.1 330 45
termination-crafted/NonTerminationSimple9_false-no-overflow.c 4.3 240 36
termination-crafted/Pure2Phase_false-no-overflow.c 4.7 280 36
termination-crafted/Pure3Phase_false-no-overflow.c 4.2 240 33
termination-crafted/RecursiveMultiplication_false-no-overflow.c 4.4 250 34
termination-crafted/RecursiveNonterminating_false-no-overflow.c 4.3 240 34
termination-crafted/Rotation180_false-no-overflow.c 4.1 240 34
termination-crafted/Singapore_false-no-overflow.c 4.0 240 36
termination-crafted/Singapore_plus_false-no-overflow.c 4.1 240 34
termination-crafted/Singapore_v1_false-no-overflow.c 4.2 240 35
termination-crafted/Singapore_v2_false-no-overflow.c 4.1 240 36
termination-crafted/Stockholm_false-no-overflow.c 4.3 240 39
termination-crafted/Thun_false-no-overflow.c 4.0 240 33
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 4.9 280 41
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 13   660 120
termination-crafted/aaron2_false-no-overflow.c 4.7 280 43
termination-crafted/aaron3_false-no-overflow.c 6.0 320 40
termination-crafted/easy2_false-no-overflow.c 900   5300 14000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 7.3 360 56
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 30   940 320
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 4.6 280 36
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 5.7 300 51
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 5.2 300 44
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 5.3 300 42
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 5.0 300 43
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 17   720 150
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 4.1 230 38
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 4.9 300 40
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 4.6 290 46
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 5.5 310 53
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 4.7 290 39
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 900   4900 13000
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900   2000 11000
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 3.8 240 37
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900   5200 11000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 6.3 310 53
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 9.8 540 79
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 8.5 450 66
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 19   790 170
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 12   560 93
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 8.4 480 71
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 12   530 99
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 11   550 83
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 14   610 120
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 4.1 240 33
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 5.3 300 45
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 4.9 280 44
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 4.9 280 42
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 5.0 290 41
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 5.5 300 46
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 5.7 300 45
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 4.8 290 38
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 4.1 240 33
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 4.1 240 37
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 4.8 290 37
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 900   5300 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 4.7 300 43
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 5.1 280 46
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 4.6 280 38
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 4.4 240 36
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 5.9 300 49
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 4.0 240 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 7.1 370 56
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 900   5300 15000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 5.0 290 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 4.5 280 38
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 900   5000 13000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 900   8500 9900
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 4.1 250 35
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 4.4 240 39
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 4.9 290 41
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 4.9 300 39
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 4.8 280 37
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 4.4 250 37
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 4.5 250 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 4.5 280 38
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 4.2 240 40
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 4.2 240 36
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 4.3 250 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 4.5 280 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 4.3 240 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 4.4 280 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 4.2 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 4.1 230 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 3.9 230 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 4.5 280 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 4.2 240 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 4.2 240 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 4.1 250 41
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 4.3 240 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 4.0 240 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 4.2 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 4.9 290 43
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 4.7 300 39
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 6.2 330 45
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 4.0 250 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 4.1 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 4.2 240 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 4.2 240 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 4.4 270 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 4.1 230 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 4.0 240 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 4.2 240 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 4.1 250 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 4.0 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 4.4 250 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 6.5 340 48
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 4.3 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 4.2 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 4.6 280 35
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 4.3 240 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 4.1 240 34
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 4.2 240 38
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 4.2 250 37
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 4.2 250 36
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 4.3 250 32
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 4.9 290 39
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 4.1 240 33
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 4.2 240 37
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 4.1 240 38
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 4.8 280 42
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 6.1 300 56
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 4.2 240 32
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 4.9 290 43
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 4.1 240 32
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 4.1 240 37
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 5.7 310 53
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 5.1 290 42
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 4.3 240 34
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 4.0 240 35
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 4.2 240 37
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 4.5 280 39
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 4.3 240 33
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 4.0 240 34
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 4.2 240 35
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 4.0 240 32
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 4.0 250 36
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 4.2 250 36
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 4.2 250 37
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 4.8 290 37
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 5.1 290 40
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 5.3 280 45
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 5.2 300 48
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 4.3 250 39
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 4.5 280 40
termination-crafted-lit/cstrncmp_false-no-overflow.c 8.0 370 61
termination-crafted-lit/gcd1_false-no-overflow.c 4.4 250 37
termination-crafted-lit/joey_false-no-overflow.c 5.0 290 48
termination-crafted-lit/min_rf_false-no-overflow.c 4.4 250 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900   5100 15000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 5.3 300 42
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 4.6 280 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900   5300 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 5.6 290 45
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 15   640 130
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900   4700 14000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 160   4700 1900
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 5.9 300 45
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 7.0 330 52
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 5.9 300 50
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 4.9 290 37
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 6.6 320 56
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 8.4 380 65
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900   5300 12000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 8.0 450 70
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 7.8 420 63
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 6.0 310 51
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900   2500 12000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 8.0 440 63
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 4.8 290 42
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900   5400 13000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900   8100 8900
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 160   4900 1800
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 4.3 230 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 4.8 280 44
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 4.8 290 49
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 5.0 290 40
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 5.1 300 39
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 5.1 290 44
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 5.4 300 42
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 5.5 300 51
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 6.0 300 53
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 110   3500 1400
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   5100 12000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 5.0 290 40
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 8.0 450 69
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 4.6 280 38
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 6.1 310 52
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 4.8 280 43
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900   5300 13000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 4.7 270 38
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 5.0 300 40
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   1200 12000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 9.0 510 67
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 17   700 160
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 5.4 300 45
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 4.9 290 38
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 4.8 280 43
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 5.5 290 50
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 4.5 280 41
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 6.0 300 53
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 4.9 290 40
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 4.5 290 37
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 5.4 300 46
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 5.5 300 50
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 5.8 300 46
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 4.8 280 39
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 350   5700 4500
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 5.1 280 41
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 5.2 280 45
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 4.9 290 40
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 5.2 280 42
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 5.2 290 41
termination-crafted-lit/genady_true-termination_true-no-overflow.c 8.1 420 71
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 5.1 290 40
termination-numeric/Addition01_false-no-overflow.c 4.3 250 37
termination-numeric/Avg_true_false-no-overflow.c 4.2 250 35
termination-numeric/Binomial_true-termination_false-no-overflow.c 900   1100 6600
termination-numeric/Et1_true_false-no-overflow.c 4.1 240 38
termination-numeric/Et2_true_false-no-overflow.c 4.3 240 35
termination-numeric/Et3_true_false-no-overflow.c 4.2 250 37
termination-numeric/Et4_true_false-no-overflow.c 4.5 250 38
termination-numeric/MultCommutative_false-no-overflow.c 8.1 450 74
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 900   740 6400
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 900   13000 9900
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 10   540 86
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 900   4700 11000
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 5.6 290 43
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900   490 11000
termination-numeric/Parts_true-termination_true-no-overflow.c 900   5300 13000
termination-numeric/TwoWay_true-termination_true-no-overflow.c 12   530 120
termination-numeric/gcd01_true-termination_true-no-overflow.c 5.7 300 50
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 44   1200 460
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 59   1500 640
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900   5600 14000
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900   5600 13000
termination-numeric/twisted_true-termination_true-no-overflow.c 900   1300 11000
recursive/Addition02WithOverflowBug_false-no-overflow.c 6.0 330 42
recursive/Addition03_false-no-overflow.c 4.4 240 35
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 4.8 290 44
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 900   12000 10000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 900   13000 10000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 910   13000 9400
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 910   13000 8200
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 900   5200 13000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900   5200 12000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 900   5200 11000
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 4.2 240 34
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 10   520 90
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 11   510 98
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 900   5000 11000
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 36   3800 410
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 900   5400 11000
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 900   5000 13000
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 900   4800 11000
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 6.8 310 53
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 6.5 310 54
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 900   3100 12000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 900   5000 14000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 5.7 300 47
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 11   530 100
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 900   4700 14000
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 60   1500 600
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 57   1700 520
recursive-simple/id_b3_o2_false-no-overflow.c 4.6 290 37
recursive-simple/id_b3_o5_false-no-overflow.c 4.8 280 35
recursive-simple/id_b5_o10_false-no-overflow.c 4.7 280 39
recursive-simple/sum_non_eq_false-no-overflow.c 4.8 280 40
recursive-simple/sum_non_false-no-overflow.c 5.2 300 46
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 4.2 250 38
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 4.2 250 34
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 4.0 240 33
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 4.1 250 39
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 4.0 230 35
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 6.2 310 53
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 6.0 310 52
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 5.9 300 55
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 4.1 250 35
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 4.3 240 35
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 4.1 240 38
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 4.1 240 37
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 4.1 240 34
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 4.2 250 35
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 3.8 240 34
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 3.9 240 32
bitvector/byte_add_1_false-no-overflow.i 25   650 250
bitvector/byte_add_2_false-no-overflow.i 38   800 370
bitvector/byte_add_false-no-overflow.i 69   810 790
bitvector/jain_1_false-no-overflow.i 4.2 250 37
bitvector/jain_2_false-no-overflow.i 4.1 240 34
bitvector/jain_4_false-no-overflow.i 4.2 240 33
bitvector/jain_5_false-no-overflow.i 900   5200 12000
bitvector/jain_6_false-no-overflow.i 4.3 250 37
bitvector/jain_7_false-no-overflow.i 4.2 250 35
bitvector/modulus_false-no-overflow.i 4.2 240 36
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 5.0 280 41
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 5.5 290 45
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 5.1 290 41
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 5.5 310 44
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 5.5 290 46
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 5.3 290 44
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 11   540 92
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 4.3 250 34
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 4.2 250 35
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 6.6 340 48
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 4.0 240 33
bitvector/jain_5_true-unreach-call_true-no-overflow.i 4.2 250 40
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 4.1 240 34
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 4.0 240 32
bitvector/modulus_true-unreach-call_true-no-overflow.i 4.3 240 36
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 4.2 250 35
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 4.5 250 32
bitvector/parity_true-unreach-call_true-no-overflow.i 4.3 250 35
bitvector/sum02_false-unreach-call_true-no-overflow.i 4.1 240 33
bitvector/sum02_true-unreach-call_true-no-overflow.i 4.1 240 34
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 358 42000 360000 550000
    correct results 304 2500 110000 24000
        correct true 141 1700 68000 18000
        correct false 163 760 44000 6500
    correct-unconfimed results 3 180 4700 1800
        correct-unconfirmed true 3 180 4700 1800
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other]