Tool Pinaka 0.1
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-06 20:14:43 CET
Run set [sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other]
Options --graphml-witness witness.graphml
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i false(no-overflow) .38 61 3.4
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) .39 61 3.5
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) .38 61 3.7
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) .40 61 4.4
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) .38 61 3.1
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) .38 61 4.1
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) .39 61 4.2
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) .39 61 3.5
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) .37 61 4.3
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) .39 61 3.7
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true .39 61 3.4
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true .38 61 3.7
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true .38 61 4.1
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true .38 61 3.6
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true .40 61 3.0
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) .38 59 3.2
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) .35 58 4.4
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) .38 59 3.4
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) .35 59 3.1
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) .40 59 3.3
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) .36 59 3.7
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) .35 59 3.1
termination-crafted/Cairo_step2_false-no-overflow.c timeout 900    410 4100  
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) .43 60 3.5
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) .35 59 3.7
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) .37 59 4.0
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) .40 59 3.2
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) .35 59 4.3
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) .38 59 3.0
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) .36 59 3.7
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) .35 59 4.0
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) .37 59 4.1
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) .36 58 3.6
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) .40 59 3.1
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) .39 59 3.9
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) .37 59 3.1
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) .35 59 4.1
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 900    400 3800  
termination-crafted/NonTerminationSimple5_false-no-overflow.c timeout 900    360 4600  
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) .37 58 2.7
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) .34 59 3.1
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) .37 59 3.0
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) .36 59 3.3
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) .37 59 2.9
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) .36 59 3.3
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) .36 59 3.1
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) .40 59 3.2
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) .37 59 3.8
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) .38 58 3.3
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) .37 59 2.7
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) .35 59 3.2
termination-crafted/Thun_false-no-overflow.c false(no-overflow) .35 58 3.5
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) .36 59 3.7
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) .36 59 3.9
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) .40 59 3.7
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) .39 59 3.1
termination-crafted/easy2_false-no-overflow.c timeout 900    410 4000  
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true .77 60 6.4
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    770 6700  
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c timeout 900    1400 5300  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    920 5200  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    460 5400  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900    410 4100  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true .36 59 3.5
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    390 6500  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900    420 6300  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    420 4600  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    390 3700  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    440 4600  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900    1900 6100  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    14000 9600  
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 900    14000 9300  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 840    15000 11000  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 43    15000 610  
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 43    15000 660  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    390 4800  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 40    15000 570  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 42    15000 620  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 320    15000 3800  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 250    15000 3300  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 320    15000 4100  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900    4600 14000  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 290    15000 3600  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 900    880 4400  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout 900    3400 3400  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    520 5000  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    300 6300  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    210 4500  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 900    380 4600  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    300 7600  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    350 4300  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true .34 59 3.5
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 60    15000 870  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true .38 59 4.5
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 900    410 4900  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) .35 59 4.4
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) .40 59 3.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) .35 59 4.1
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) .37 59 3.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) .36 59 4.4
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c timeout 900    360 4900  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 900    420 4500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) .41 59 3.2
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) .37 59 3.3
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 900    410 3700  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 900    540 8000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) .37 59 3.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) .38 59 3.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) .38 59 3.6
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) .37 58 3.7
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) .38 59 3.2
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) .39 59 3.6
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) .38 59 3.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) .36 59 3.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) .37 59 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) .36 59 3.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) .38 59 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) .36 59 3.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) .37 59 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) .37 59 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) .35 59 3.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) .37 59 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) .36 59 3.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) .36 58 3.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) .37 59 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) .37 58 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) .34 58 4.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) .38 59 3.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) .36 59 3.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) .37 59 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) .36 59 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) .36 59 3.5
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) .41 59 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) .35 59 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) .36 59 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) .36 59 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) .38 58 3.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) .38 59 3.1
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) .37 59 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) .38 59 3.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) .37 58 3.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) .40 59 3.6
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) .37 59 2.7
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) .39 59 3.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) .40 59 3.0
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) .37 59 3.4
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) .36 59 3.2
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) .38 59 3.3
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) .37 59 2.9
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) .36 59 3.3
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) .39 59 4.4
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) .37 58 3.2
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) .36 59 4.0
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) .39 59 3.3
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) .38 59 3.2
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) .38 59 3.5
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) .37 58 3.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c timeout 900    8000 7000  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) .40 59 3.0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) .36 59 3.1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) .37 59 3.3
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) .35 59 4.1
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) .37 59 3.2
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) .38 59 3.5
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c timeout 900    410 4900  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) .35 59 3.9
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) .36 59 2.7
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) .37 58 3.4
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) .36 59 3.0
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) .37 59 3.6
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) .35 59 3.8
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) .38 59 3.4
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) .38 59 2.6
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c timeout 900    430 4800  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c timeout 900    450 6100  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c timeout 900    460 5800  
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) .36 59 3.2
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) .37 58 3.3
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) .70 61 6.4
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) .38 59 3.0
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) .37 58 3.8
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) .37 59 3.5
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900    490 6400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 900    320 4300  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true .41 59 3.6
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 900    410 4500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c out of memory 38    15000 470  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 900    380 4000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 900    550 7100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c out of memory 130    15000 1800  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 900    350 4800  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 900    320 4900  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 900    400 4100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c out of memory 40    15000 590  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 900    360 4100  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 900    520 5500  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 900    380 4500  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 900    420 5700  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 900    550 8300  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 900    390 4800  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c out of memory 38    15000 460  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 900    410 6100  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true .39 59 4.1
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 900    410 3800  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 900    470 8500  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c out of memory 120    15000 1400  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 900    510 8200  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout 900    430 6400  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 900    330 5900  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 900    390 5000  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 900    380 5100  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 900    400 6800  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 900    300 5900  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 900    320 4500  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c out of memory 290    15000 2900  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true .44 59 3.7
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 900    400 5300  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 900    350 5000  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 900    440 4500  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 900    400 6000  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 900    380 4000  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 900    620 6400  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 900    970 12000  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 900    400 4300  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c out of memory 42    15000 520  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 900    540 5500  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c timeout 900    4500 5400  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 98    15000 1400  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 900    320 5800  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 900    410 4700  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true .66 130 7.0
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c out of memory 38    15000 520  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 900    360 6000  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 900    490 3600  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 900    370 5200  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 900    3200 4600  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c out of memory 770    15000 8100  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 900    730 4900  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 900    370 5900  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c out of memory 540    15000 7000  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c out of memory 52    15000 830  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 900    890 7400  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 900    710 5500  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout 900    1100 11000  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 900    690 5100  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 900    700 5200  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2.6  85 30  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout 900    630 6300  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) .35 59 3.5
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) .36 59 3.9
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) .56 59 5.9
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) .38 59 4.0
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) .39 59 3.2
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) .39 59 3.6
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) .36 59 3.6
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) .39 59 3.3
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 900    3000 4300  
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 55    15000 800  
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c out of memory 100    15000 1500  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c out of memory 45    15000 700  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 900    1800 7800  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 4.9  620 67  
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 900    680 5500  
termination-numeric/TwoWay_true-termination_true-no-overflow.c out of memory 54    15000 770  
termination-numeric/gcd01_true-termination_true-no-overflow.c out of memory 180    15000 2600  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true .66 120 7.3
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true .59 62 7.4
termination-numeric/rec_counter1_true-termination_true-no-overflow.c out of memory 840    15000 11000  
termination-numeric/rec_counter3_true-termination_true-no-overflow.c out of memory 850    15000 12000  
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 900    500 5100  
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) .37 58 3.1
recursive/Addition03_false-no-overflow.c false(no-overflow) .36 58 3.4
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) .37 59 3.2
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 55    15000 690  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 55    15000 770  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 55    15000 760  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 55    15000 620  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 73    15000 850  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 69    15000 830  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 47    15000 640  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true .35 59 3.6
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 89    15000 1300  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c out of memory 90    15000 1200  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 47    15000 670  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true .44 59 3.7
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 47    15000 620  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 45    15000 730  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 45    15000 680  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory 43    15000 660  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 43    15000 620  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 43    15000 560  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 850    15000 5600  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 180    15000 2500  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 230    15000 3200  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 900    4500 6300  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true .62 62 6.3
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true .67 68 6.6
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) .36 58 3.7
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) .38 59 3.4
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) .36 59 3.3
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) .37 59 3.1
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) .37 59 3.1
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 200    15000 2500  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c out of memory 200    15000 2500  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 200    15000 2500  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c out of memory 200    15000 2800  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 190    15000 2400  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c out of memory 480    15000 6600  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 480    15000 6700  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c out of memory 480    15000 6100  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2000  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2000  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2100  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2000  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2300  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 170    15000 2200  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c out of memory 90    15000 1100  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 86    15000 1200  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .44 59 4.1
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .47 59 4.0
bitvector/byte_add_false-no-overflow.i false(no-overflow) .41 59 4.2
bitvector/jain_1_false-no-overflow.i false(no-overflow) .36 58 3.3
bitvector/jain_2_false-no-overflow.i false(no-overflow) .35 58 3.1
bitvector/jain_4_false-no-overflow.i false(no-overflow) .37 58 3.3
bitvector/jain_5_false-no-overflow.i false(no-overflow) 67    1300 840  
bitvector/jain_6_false-no-overflow.i false(no-overflow) .36 58 3.2
bitvector/jain_7_false-no-overflow.i false(no-overflow) .36 58 2.8
bitvector/modulus_false-no-overflow.i false(no-overflow) .35 59 3.1
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .54 60 5.6
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .57 59 6.1
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 1.3  96 17  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .47 60 4.3
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 6.0  680 83  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 6.0  690 77  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .37 58 3.2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .37 58 3.2
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i out of memory 32    15000 410  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i out of memory 32    15000 440  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i out of memory 31    15000 410  
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 600    15000 7700  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i out of memory 32    15000 420  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i out of memory 39    15000 500  
bitvector/modulus_true-unreach-call_true-no-overflow.i out of memory 59    15000 970  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .40 58 2.4
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .96 61 13  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2.6  93 32  
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 900    510 5400  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 900    490 6100  
psyco/psyco_abp_1_false-no-overflow.c out of memory 62    15000 810  
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 359 97000   1200000 690000
    correct results 191 160   14000 1700
        correct true 29 30   3200 350
        correct false 162 130   11000 1400
    correct-unconfimed results 3 6.2 740 83
        correct-unconfirmed true 3 6.2 740 83
        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]