Tool CPAchecker 1.7-svn 29852
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 05:46:16 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 3.9 280 36
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 4.3 280 38
signedintegeroverflow-regression/Division_false-no-overflow.c.i 4.2 290 37
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 3.8 280 34
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 4.0 280 37
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 4.0 280 37
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 4.0 280 35
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 4.0 280 38
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 3.9 280 35
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 4.3 280 36
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i 3.5 270 34
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i 3.7 280 35
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i 3.7 280 34
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i 3.4 270 35
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i 3.6 280 34
termination-crafted/2Nested_false-no-overflow.c 3.0 270 28
termination-crafted/4NestedWith3Variables_false-no-overflow.c 3.1 260 31
termination-crafted/Ackermann_false-no-overflow.c 900   3400 9800
termination-crafted/Bangalore_false-no-overflow.c 3.2 270 28
termination-crafted/Bangalore_v3_false-no-overflow.c 3.0 270 25
termination-crafted/Benghazi_nondet_false-no-overflow.c 2.9 270 27
termination-crafted/Binary_Search_false-no-overflow.c 2.9 270 31
termination-crafted/Cairo_nondet_false-no-overflow.c 3.2 270 29
termination-crafted/Cairo_step2_false-no-overflow.c 910   2500 11000
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 3.3 280 30
termination-crafted/Copenhagen_disj_false-no-overflow.c 3.0 270 31
termination-crafted/Gothenburg_false-no-overflow.c 3.0 270 27
termination-crafted/Gothenburg_v2_false-no-overflow.c 3.0 270 30
termination-crafted/Hanoi_2vars_false-no-overflow.c 3.0 270 26
termination-crafted/Hanoi_3vars_false-no-overflow.c 3.0 270 32
termination-crafted/Hanoi_plus_false-no-overflow.c 3.1 270 27
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 3.0 280 31
termination-crafted/Mysore_false-no-overflow.c 3.0 270 26
termination-crafted/NestedRecursion_1a_false-no-overflow.c 3.1 270 25
termination-crafted/NestedRecursion_2a_false-no-overflow.c 3.1 280 31
termination-crafted/NonTermination1_false-no-overflow.c 3.3 280 34
termination-crafted/NonTermination2_false-no-overflow.c 3.3 280 31
termination-crafted/NonTermination4_false-no-overflow.c 200   1300 1500
termination-crafted/NonTerminationSimple2_false-no-overflow.c 3.1 270 30
termination-crafted/NonTerminationSimple3_false-no-overflow.c 3.1 270 28
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   2000 12000
termination-crafted/NonTerminationSimple5_false-no-overflow.c 3.1 270 27
termination-crafted/NonTerminationSimple6_false-no-overflow.c 3.2 270 30
termination-crafted/NonTerminationSimple8_false-no-overflow.c 3.0 260 25
termination-crafted/NonTerminationSimple9_false-no-overflow.c 3.1 270 27
termination-crafted/Pure2Phase_false-no-overflow.c 3.1 270 29
termination-crafted/Pure3Phase_false-no-overflow.c 3.2 270 32
termination-crafted/RecursiveMultiplication_false-no-overflow.c 3.5 290 38
termination-crafted/RecursiveNonterminating_false-no-overflow.c 3.0 270 28
termination-crafted/Rotation180_false-no-overflow.c 2.9 270 26
termination-crafted/Singapore_false-no-overflow.c 3.1 270 27
termination-crafted/Singapore_plus_false-no-overflow.c 2.8 270 27
termination-crafted/Singapore_v1_false-no-overflow.c 3.0 270 28
termination-crafted/Singapore_v2_false-no-overflow.c 2.9 260 27
termination-crafted/Stockholm_false-no-overflow.c 3.1 270 31
termination-crafted/Thun_false-no-overflow.c 3.1 270 26
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 3.0 270 28
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 3.5 280 35
termination-crafted/aaron2_false-no-overflow.c 3.0 270 26
termination-crafted/aaron3_false-no-overflow.c 2.9 270 27
termination-crafted/easy2_false-no-overflow.c 910   13000 11000
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 27
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 3.1 270 31
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c 3.1 270 29
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 910   6800 11000
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 25
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 3.0 270 28
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 3.1 270 31
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 900   5000 11000
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 2.9 270 25
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 910   2500 12000
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 29
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 26
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 3.1 280 27
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 3.2 270 31
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 910   6800 12000
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 3.0 270 27
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 900   560 12000
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 3.4 280 28
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 3.3 270 34
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 4.6 290 39
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 4.4 300 41
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 900   1200 14000
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 3.7 290 34
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 900   1400 10000
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 900   4100 11000
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 910   4400 12000
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 3.2 270 29
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 3.0 270 28
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 29
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 25
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 29
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 3.0 270 29
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 3.2 270 30
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 25
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2.9 270 29
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 2.8 260 25
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 3.0 270 29
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 910   13000 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 2.9 270 25
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 3.1 270 28
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 3.0 270 28
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 3.0 270 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 3.1 270 31
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 3.1 270 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 3.1 270 32
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 910   13000 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 3.0 270 32
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 3.0 270 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 910   6600 10000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 910   620 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 3.3 280 32
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 3.1 270 32
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 3.1 270 26
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 3.0 270 33
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 3.1 270 28
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 3.1 280 26
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 3.1 270 26
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 2.9 270 27
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 3.0 270 31
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 3.1 270 27
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 3.0 260 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 3.1 270 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 3.0 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 3.2 280 33
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 3.4 280 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 3.3 280 30
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 3.0 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 3.0 270 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 3.0 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 3.1 270 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 3.0 270 32
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 3.0 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 3.3 280 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 3.2 260 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 3.1 270 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 3.1 260 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 3.0 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 3.0 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 3.0 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 3.1 270 30
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 3.1 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 3.0 270 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 3.0 270 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 2.9 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 2.8 270 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 3.1 270 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 3.1 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 3.0 270 28
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 3.0 270 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 3.0 270 25
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 3.1 270 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 3.0 260 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 3.1 270 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 3.0 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 3.3 290 29
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 3.2 270 31
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 2.9 270 26
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 3.1 270 28
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 3.0 270 30
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 3.1 270 26
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 3.0 270 26
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 3.0 260 27
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 3.2 270 27
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 3.6 290 33
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 3.0 270 31
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 3.3 280 29
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 3.1 280 29
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 3.2 280 32
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 3.3 280 30
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 3.4 290 34
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 3.8 290 35
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 3.3 290 28
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 2.9 270 27
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 2.9 270 28
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 3.0 270 32
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 3.0 270 25
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 3.2 280 34
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 3.0 260 28
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 3.0 270 31
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 3.0 270 30
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 3.1 270 27
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 3.1 270 27
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 3.1 270 29
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 3.1 270 29
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 3.0 270 28
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 3.0 270 27
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 3.1 270 30
termination-crafted-lit/cstrncmp_false-no-overflow.c 4.0 320 46
termination-crafted-lit/gcd1_false-no-overflow.c 2.9 270 22
termination-crafted-lit/joey_false-no-overflow.c 3.1 270 29
termination-crafted-lit/min_rf_false-no-overflow.c 3.1 270 28
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 870   15000 12000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 3.2 270 27
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 3.0 270 29
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900   13000 14000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 110   1100 890
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 910   6600 11000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 910   520 14000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 59   550 760
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 3.1 270 25
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 3.1 270 33
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 3.2 270 31
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 4.8 290 46
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 3.1 270 25
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 3.4 280 33
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 910   7000 11000
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 3.1 270 28
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 3.2 270 30
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 910   8200 11000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900   15000 11000
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 900   4100 11000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2.9 270 28
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 910   13000 11000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 910   620 13000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 59   540 830
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 3.1 270 30
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 3.1 260 27
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 2.9 270 26
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 3.0 260 26
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 3.1 270 28
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 3.1 270 30
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 3.2 270 26
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 3.0 270 26
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 3.0 260 28
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 900   7200 10000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   560 13000
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 3.2 270 28
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900   4200 10000
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 3.1 270 27
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 3.2 270 32
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 3.0 270 27
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900   6700 12000
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 3.0 260 28
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 3.1 270 31
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   560 13000
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 3.6 280 31
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 900   4200 10000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 3.0 270 27
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 3.0 270 30
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 3.0 270 28
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 110   1100 780
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 3.0 270 28
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 3.0 270 26
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 3.0 270 28
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 2.9 270 28
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 910   5200 11000
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 4.8 290 46
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 3.1 270 29
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 3.1 270 28
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 910   8200 12000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 3.7 310 35
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 3.6 300 34
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 3.2 280 26
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 3.6 310 37
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 3.6 310 34
termination-crafted-lit/genady_true-termination_true-no-overflow.c 910   4400 10000
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 3.2 280 32
termination-numeric/Addition01_false-no-overflow.c 3.2 280 28
termination-numeric/Avg_true_false-no-overflow.c 3.1 270 29
termination-numeric/Binomial_true-termination_false-no-overflow.c 900   1400 9400
termination-numeric/Et1_true_false-no-overflow.c 3.0 270 27
termination-numeric/Et2_true_false-no-overflow.c 2.9 270 29
termination-numeric/Et3_true_false-no-overflow.c 3.0 270 29
termination-numeric/Et4_true_false-no-overflow.c 3.1 260 27
termination-numeric/MultCommutative_false-no-overflow.c 6.3 300 63
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 900   1300 7900
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 910   6900 10000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900   4300 10000
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 6.1 320 54
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 3.3 280 30
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900   1300 10000
termination-numeric/Parts_true-termination_true-no-overflow.c 900   3000 10000
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900   640 8400
termination-numeric/gcd01_true-termination_true-no-overflow.c 3.6 280 32
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 16   540 160
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 910   4400 10000
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900   4100 10000
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900   4400 11000
termination-numeric/twisted_true-termination_true-no-overflow.c 900   7900 13000
recursive/Addition02WithOverflowBug_false-no-overflow.c 3.2 280 30
recursive/Addition03_false-no-overflow.c 3.3 280 28
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 3.0 270 26
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 910   3800 12000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 910   9400 12000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 910   4400 11000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 900   5300 12000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 900   5600 12000
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900   5600 12000
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 900   1900 9800
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 3.2 280 28
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 910   4400 11000
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 910   4700 9000
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 4.8 300 44
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 680   760 6100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 7.6 400 78
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 5.8 300 61
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 5.7 310 61
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 3.6 280 38
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 3.7 280 32
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 5.0 300 48
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 11   330 110
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 3.5 280 33
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 4.0 290 42
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 910   6600 11000
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 910   4600 11000
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 910   4600 11000
recursive-simple/id_b3_o2_false-no-overflow.c 3.1 280 29
recursive-simple/id_b3_o5_false-no-overflow.c 3.1 280 28
recursive-simple/id_b5_o10_false-no-overflow.c 3.1 270 28
recursive-simple/sum_non_eq_false-no-overflow.c 3.1 280 31
recursive-simple/sum_non_false-no-overflow.c 3.2 280 30
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 3.2 270 31
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 3.1 270 32
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 3.1 280 32
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 3.2 270 29
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 3.1 270 30
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 4.3 300 41
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 4.2 290 42
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 5.2 310 45
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 3.1 280 27
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 3.2 270 27
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 3.2 270 27
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 3.1 280 32
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 3.0 270 28
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 3.1 270 27
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 3.0 270 28
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 3.1 270 29
bitvector/byte_add_1_false-no-overflow.i 6.4 320 58
bitvector/byte_add_2_false-no-overflow.i 7.1 330 63
bitvector/byte_add_false-no-overflow.i 7.4 310 74
bitvector/jain_1_false-no-overflow.i 3.4 310 34
bitvector/jain_2_false-no-overflow.i 3.4 300 30
bitvector/jain_4_false-no-overflow.i 3.4 300 36
bitvector/jain_5_false-no-overflow.i 910   4100 11000
bitvector/jain_6_false-no-overflow.i 3.4 300 30
bitvector/jain_7_false-no-overflow.i 3.4 300 31
bitvector/modulus_false-no-overflow.i 3.0 270 29
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 4.0 280 38
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 3.9 280 41
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 3.9 280 37
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 3.1 280 32
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 3.2 270 26
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 3.1 270 26
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 4.5 300 43
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 3.1 260 29
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2.9 270 27
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2.9 260 30
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 3.1 270 27
bitvector/jain_5_true-unreach-call_true-no-overflow.i 3.0 270 26
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 3.0 270 26
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2.9 270 26
bitvector/modulus_true-unreach-call_true-no-overflow.i 3.2 270 26
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 3.1 270 26
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 3.2 270 32
bitvector/parity_true-unreach-call_true-no-overflow.i 3.1 270 26
bitvector/sum02_false-unreach-call_true-no-overflow.i 2.9 270 29
bitvector/sum02_true-unreach-call_true-no-overflow.i 3.0 270 28
psyco/psyco_abp_1_false-no-overflow.c 910   8000 11000
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 57000 410000 710000
    correct results 283 2100 81000 19000
        correct true 119 1400 35000 13000
        correct false 164 730 46000 6300
    correct-unconfimed results 11 62 3500 600
        correct-unconfirmed true 11 62 3500 600
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]