Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-01-13 07:44:08 CET [[ 2017-01-15 00:24:53 CET ]] [[ 2017-01-15 00:50:42 CET ]] [[ 2017-01-15 00:30:44 CET ]] [[ 2017-01-15 00:56:39 CET ]]
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0744.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 3.2 1.2  27 270 0      0   4.0 2.2 73 250 6.9 3.6 83 310
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 3.0 1.2  23 250 0      0   4.0 2.2 72 240 6.9 3.7 120 320
signedintegeroverflow-regression/Division_false-no-overflow.c.i 2.9 1.2  28 270 0      0   3.9 2.2 60 260 6.9 3.7 86 320
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 2.9 1.1  25 270 0      0   4.3 2.3 65 260 6.8 3.6 95 300
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 3.0 1.2  29 260 0      0   3.9 2.2 65 250 6.6 3.6 120 310
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 2.9 1.1  25 260 0      0   4.1 2.3 65 260 7.2 3.9 130 320
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 3.0 1.2  24 270 0      0   3.8 2.1 55 260 7.1 3.8 140 320
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 3.0 1.2  28 260 0      0   4.0 2.2 67 240 6.7 3.6 100 310
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 2.9 1.2  25 260 0      0   3.9 2.2 73 250 8.2 4.3 96 340
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 3.0 1.2  26 260 0      0   3.9 2.2 58 240 7.3 3.9 92 320
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i 2.8 1.1  23 260 0      0   4.0  2.2  58 260 6.9 3.7 130 310
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i 2.7 1.1  26 250 0      0   4.2  2.3  83 270 7.4 3.9 140 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i 2.9 1.2  26 250 0      0   3.9  2.2  64 250 7.0 3.8 140 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i 2.9 1.1  24 260 0      0   3.8  2.1  67 250 6.9 3.7 130 310
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i 2.9 1.1  24 260 0      0   3.9  2.2  65 270 7.5 4.0 130 310
termination-crafted/2Nested_false-no-overflow.c 2.3 1.0  21 250 0      0   3.1 1.8 57 240 6.8 3.7 110 320
termination-crafted/4NestedWith3Variables_false-no-overflow.c 2.3 1.0  19 250 0      0   3.2 1.8 57 240 7.0 3.7 140 310
termination-crafted/Ackermann_false-no-overflow.c 2.4 1.0  24 240 0      0   3.3 1.9 60 240 6.7 3.6 100 310
termination-crafted/Bangalore_false-no-overflow.c 2.3 1.0  22 250 0      0   2.9 1.6 46 240 6.8 3.6 97 310
termination-crafted/Bangalore_v3_false-no-overflow.c 2.5 1.1  24 260 0      0   2.9 1.6 47 230 7.2 3.8 150 320
termination-crafted/Benghazi_nondet_false-no-overflow.c 2.4 1.1  19 250 0      0   3.3 1.8 55 240 7.2 3.8 140 310
termination-crafted/Binary_Search_false-no-overflow.c 2.5 1.1  19 250 0      0   3.4 1.9 72 240 7.1 3.8 88 320
termination-crafted/Cairo_nondet_false-no-overflow.c 2.9 1.2  24 270 0      0   3.3 1.8 59 250 8.3 4.3 170 330
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 2.4 1.1  24 250 0      0   2.9 1.6 42 240 6.7 3.7 87 310
termination-crafted/Copenhagen_disj_false-no-overflow.c 2.4 1.1  22 250 .0082 0   3.3 1.9 73 240 7.6 4.1 140 320
termination-crafted/Gothenburg_false-no-overflow.c 2.6 1.1  22 260 .0082 0   3.1 1.8 49 240 7.3 3.9 85 330
termination-crafted/Gothenburg_v2_false-no-overflow.c 2.6 1.1  24 260 .0082 0   3.2 1.8 50 230 7.5 4.0 150 310
termination-crafted/Hanoi_2vars_false-no-overflow.c 2.3 1.0  20 240 0      0   3.1 1.8 49 240 6.6 3.5 80 310
termination-crafted/Hanoi_3vars_false-no-overflow.c 2.6 1.1  20 240 0      0   3.5 2.0 65 250 7.2 3.8 130 320
termination-crafted/Hanoi_plus_false-no-overflow.c 2.5 1.1  20 250 0      0   3.2 1.8 53 240 6.7 3.6 79 310
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 2.5 1.1  24 260 0      0   3.3 1.8 64 240 7.2 3.8 82 320
termination-crafted/Mysore_false-no-overflow.c 2.6 1.1  23 260 .0082 0   3.3 1.8 54 230 7.1 3.8 100 310
termination-crafted/NestedRecursion_1a_false-no-overflow.c 2.4 1.0  23 260 0      0   3.4 1.9 53 240 7.6 4.1 150 330
termination-crafted/NestedRecursion_2a_false-no-overflow.c 2.4 1.0  20 250 0      0   3.4 1.9 57 250 7.6 4.1 150 320
termination-crafted/NonTermination1_false-no-overflow.c 2.3 1.0  21 250 0      0   2.9 1.7 58 240 6.6 3.5 79 310
termination-crafted/NonTermination2_false-no-overflow.c 2.4 1.1  21 250 .0082 0   3.0 1.7 41 240 6.9 3.7 110 320
termination-crafted/NonTermination4_false-no-overflow.c 3.8 1.4  30 270 0      0   3.7 2.1 40 250 7.6 4.1 95 310
termination-crafted/NonTerminationSimple2_false-no-overflow.c 2.4 1.0  21 250 0      0   2.9 1.7 33 240 7.7 4.0 140 330
termination-crafted/NonTerminationSimple3_false-no-overflow.c 2.4 1.0  19 250 0      0   2.9 1.6 65 240 6.9 3.7 110 320
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   850    12000 760 0      0   3.7 2.1 62 280 97   62   810 1600
termination-crafted/NonTerminationSimple5_false-no-overflow.c 2.5 1.1  20 260 0      0   3.1 1.8 54 250 6.7 3.6 110 320
termination-crafted/NonTerminationSimple6_false-no-overflow.c 2.5 1.1  22 250 0      0   2.9 1.7 40 240 6.8 3.6 86 320
termination-crafted/NonTerminationSimple8_false-no-overflow.c 2.7 1.2  24 260 .025  0   2.9 1.7 55 230 7.6 4.0 150 330
termination-crafted/NonTerminationSimple9_false-no-overflow.c 2.3 1.0  22 250 0      0   3.2 1.8 69 250 6.6 3.6 88 310
termination-crafted/Pure2Phase_false-no-overflow.c 2.5 1.1  24 260 0      0   3.1 1.8 46 240 7.7 4.1 130 320
termination-crafted/Pure3Phase_false-no-overflow.c 2.6 1.1  22 260 .0082 0   3.6 2.0 78 250 7.1 3.8 130 320
termination-crafted/RecursiveMultiplication_false-no-overflow.c 2.3 1.0  19 250 0      0   3.3 1.9 54 250 7.5 4.0 110 330
termination-crafted/RecursiveNonterminating_false-no-overflow.c 2.4 1.0  24 240 0      0   3.2 1.8 61 250 7.3 3.8 110 320
termination-crafted/Rotation180_false-no-overflow.c 2.4 1.1  19 240 0      0   3.0 1.7 50 240 6.6 3.6 100 310
termination-crafted/Singapore_false-no-overflow.c 2.5 1.0  23 250 .0082 0   3.1 1.8 46 240 7.0 3.7 86 330
termination-crafted/Singapore_plus_false-no-overflow.c 2.4 1.1  20 250 .0082 0   3.1 1.8 55 230 7.5 4.0 120 320
termination-crafted/Singapore_v1_false-no-overflow.c 2.5 1.1  25 260 .0082 0   3.3 1.9 57 230 7.1 3.8 120 320
termination-crafted/Singapore_v2_false-no-overflow.c 2.6 1.1  23 260 .0082 0   3.1 1.8 50 240 7.1 3.8 120 320
termination-crafted/Stockholm_false-no-overflow.c 2.5 1.1  21 260 0      0   3.0 1.7 66 230 7.1 3.8 100 310
termination-crafted/Thun_false-no-overflow.c 2.4 1.0  19 250 0      0   3.2 1.9 58 240 7.3 3.9 120 320
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 2.5 1.1  21 260 .0082 0   3.4 1.9 54 250 7.3 3.9 120 310
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 2.8 1.2  27 270 .012  0   3.6 2.1 62 250 9.3 5.0 120 350
termination-crafted/aaron2_false-no-overflow.c 2.8 1.1  22 280 .0082 0   3.1 1.8 50 250 7.9 4.2 110 330
termination-crafted/aaron3_false-no-overflow.c 2.8 1.1  24 270 .0082 0   3.2 1.8 53 240 8.3 4.3 140 330
termination-crafted/4BitCounterPointer_true-no-overflow.c 910   880    8900 8900 0      0   4.5  2.5  96 280 7.0 3.8 140 310
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c 2.4 1.1  23 260 0      0   250    230    3000 7000 960   800   12000 4600
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c 2.3 1.0  22 240 0      0   3.9  2.2  84 290 9.2 4.8 160 330
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c 2.5 1.0  22 250 0      0   900    860    13000 5100 8.8 4.7 140 330
termination-crafted/Bangalore_true-no-overflow.c 900   890    9800 2400 0      0   3.8  2.2  73 280 8.5 4.5 150 330
termination-crafted/Bangalore_v2_true-no-overflow.c 2.5 1.1  23 250 0      0   2.9  1.7  50 230 8.4 4.5 150 310
termination-crafted/Bangalore_v4_true-no-overflow.c 2.6 1.1  22 260 0      0   2.9  1.7  30 240 8.1 4.4 160 320
termination-crafted/Benghazi_true-no-overflow.c 900   850    12000 5700 0      0   4.0  2.3  88 280 89   56   780 1200
termination-crafted/Cairo_step2_true-no-overflow.c 900   860    12000 4200 0      0   3.9  2.2  90 280 960   810   13000 4000
termination-crafted/Cairo_true-no-overflow.c 900   850    11000 3200 0      0   3.8  2.2  86 280 7.7 4.1 140 330
termination-crafted/Copenhagen_true-no-overflow.c 910   860    10000 8700 0      0   4.0  2.2  66 280 8.6 4.6 160 330
termination-crafted/Division_true-no-overflow.c 900   890    11000 2400 0      0   3.9  2.2  66 280 7.0 3.8 130 320
termination-crafted/LexIndexValue-Array_true-no-overflow.c 2.5 1.0  20 260 0      0   500    470    5200 7000 960   790   11000 4800
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 2.5 1.1  22 250 0      0   900    880    21000 3700 9.2 4.9 150 350
termination-crafted/Madrid_true-no-overflow.c 900   860    12000 1900 0      0   3.5  2.0  58 280 6.9 3.7 130 310
termination-crafted/McCarthy91_Iteration_true-no-overflow.c 900   850    12000 4800 0      0   4.1  2.3  89 280 960   850   11000 4600
termination-crafted/McCarthy91_Recursion_true-no-overflow.c 2.5 1.0  23 250 0      0   3.4  1.9  53 250 9.4 5.1 170 340
termination-crafted/MenloPark_true-no-overflow.c 910   860    12000 8900 0      0   .55 .35 11 44 7.4 3.8 140 330
termination-crafted/MutualRecursion_1a_true-no-overflow.c 2.5 1.0  23 250 0      0   3.5  2.0  67 240 12   6.9 210 390
termination-crafted/MutualRecursion_1b_true-no-overflow.c 2.5 1.1  23 260 0      0   3.5  1.9  46 260 19   11   290 580
termination-crafted/NestedRecursion_1b_true-no-overflow.c 2.4 1.0  22 250 0      0   3.5  1.9  59 260 18   9.7 310 530
termination-crafted/NestedRecursion_1c_true-no-overflow.c 2.3 .99 19 240 0      0   3.4  1.9  57 250 15   8.0 200 400
termination-crafted/NestedRecursion_1d_true-no-overflow.c 2.4 1.0  23 250 0      0   3.4  1.9  58 250 18   9.7 310 580
termination-crafted/NestedRecursion_2b_true-no-overflow.c 2.3 1.0  19 250 0      0   3.2  1.8  59 240 960   800   13000 4000
termination-crafted/NestedRecursion_2c_true-no-overflow.c 2.3 1.0  19 250 0      0   3.3  1.9  63 240 960   800   12000 4000
termination-crafted/NonTermination3_true-no-overflow.c 2.4 1.0  21 240 0      0   4.0  2.3  66 280 6.5 3.5 120 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c 900   850    13000 780 0      0   3.9  2.2  73 300 7.9 4.2 130 330
termination-crafted/Nyala-2lex_true-no-overflow.c 910   890    8800 11000 0      0   4.3  2.4  95 270 7.8 4.1 140 320
termination-crafted/Parallel_true-no-overflow.c 900   870    12000 4000 0      0   4.2  2.4  67 280 7.4 4.0 160 320
termination-crafted/Piecewise_true-no-overflow.c 900   890    11000 1500 0      0   4.8  2.6  77 280 8.1 4.3 150 320
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c 910   870    9900 11000 0      0   3.9  2.2  61 300 8.5 4.6 160 330
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c 900   880    9400 1700 0      0   4.8  2.6  70 280 8.2 4.4 170 310
termination-crafted/Waldkirch_true-no-overflow.c 910   860    10000 9500 0      0   3.9  2.2  80 270 7.2 3.9 140 320
termination-crafted/WhileFalse_true-no-overflow.c 2.3 1.0  19 240 0      0   2.8  1.5  35 190 5.8 3.1 110 300
termination-crafted/WhileTrue_true-no-overflow.c 900   860    12000 850 0      0   2.5  1.4  48 190 6.1 3.2 130 300
termination-crafted/easy1_true-no-overflow.c 7.9 2.6  60 330 0      0   4.1  2.3  71 280 7.6 4.2 140 320
termination-crafted/easy2_true-no-overflow.c 910   870    10000 9000 0      0   3.9  2.2  82 270 960   820   11000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 2.3 1.1  19 250 0      0   2.9 1.7 57 240 6.8 3.7 140 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 2.4 1.1  23 250 0      0   3.1 1.8 52 230 7.4 4.0 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 2.4 1.1  22 250 .0082 0   3.0 1.7 63 230 7.3 3.9 110 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 2.5 1.1  21 250 .0082 0   3.3 1.9 57 240 6.8 3.7 79 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 2.4 1.1  23 250 0      0   3.1 1.8 52 240 7.8 4.2 120 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 2.6 1.1  24 250 0      0   3.3 1.8 58 240 7.4 3.9 140 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 2.5 1.1  23 250 0      0   3.4 2.0 63 250 8.4 4.5 150 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 2.4 1.1  22 250 0      0   3.3 1.8 67 230 7.5 4.0 93 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c 18   5.8  130 510 0      0   4.1 2.3 77 260 73   43   500 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 2.2 1.0  19 240 0      0   3.0 1.7 57 240 8.2 4.3 96 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 2.3 1.0  19 250 0      0   3.3 1.9 75 240 7.9 4.2 91 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 2.6 1.1  24 260 .0082 0   3.1 1.7 49 240 7.2 3.8 120 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 2.4 1.1  21 250 0      0   3.1 1.7 34 240 7.4 3.9 91 320
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 2.6 1.1  21 260 .0082 0   3.3 1.8 52 240 7.8 4.1 91 320
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 2.4 1.1  24 240 .0082 0   3.3 1.9 54 240 8.0 4.2 120 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 2.7 1.1  21 270 .0082 0   3.7 2.0 83 260 7.0 3.8 83 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 3.0 1.2  28 270 .025  0   3.3 1.9 63 240 7.4 3.9 110 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 2.4 1.1  25 250 .0082 0   2.9 1.7 51 230 7.1 3.8 85 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 2.4 1.1  21 250 .0082 0   3.2 1.8 57 240 7.5 4.0 74 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 2.8 1.2  28 280 .0082 0   3.7 2.0 86 240 8.0 4.2 110 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 2.3 1.1  21 250 .0082 0   3.5 1.9 72 240 7.6 4.0 92 350
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 2.5 1.0  22 260 0      0   3.1 1.8 63 240 7.9 4.2 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 2.3 1.1  20 250 .0082 0   3.2 1.8 52 240 7.3 3.9 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 2.7 1.1  22 260 .0082 0   3.5 1.9 47 240 8.5 4.5 160 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 2.4 1.1  23 250 .0082 0   3.1 1.8 48 230 7.0 3.7 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 2.4 1.1  21 250 .0082 0   3.1 1.8 51 230 7.2 3.8 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 2.3 1.0  23 250 0      0   3.2 1.8 60 240 6.7 3.6 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 2.3 1.0  19 250 0      0   3.0 1.7 52 230 7.2 3.9 88 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 2.4 1.0  21 250 0      0   3.4 1.9 67 230 6.7 3.6 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 2.8 1.1  22 270 0      0   3.1 1.7 53 240 7.1 3.8 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 2.5 1.0  22 250 0      0   3.2 1.8 51 240 6.9 3.7 79 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 2.5 1.1  26 260 .0082 0   3.2 1.8 59 230 7.1 3.8 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 2.3 1.0  19 240 0      0   3.1 1.8 54 240 6.4 3.4 77 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 2.3 1.0  19 240 0      0   3.2 1.8 50 230 7.0 3.7 81 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 2.5 1.1  21 260 0      0   3.2 1.8 63 240 8.3 4.5 100 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 2.4 1.1  22 250 0      0   3.0 1.7 49 230 6.9 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 2.5 1.1  21 250 .0082 0   3.1 1.8 48 230 7.0 3.8 88 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 2.4 1.0  19 250 0      0   3.1 1.8 41 240 7.1 3.8 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 2.4 1.1  21 240 .0082 0   3.1 1.7 48 230 6.6 3.6 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 2.3 1.1  20 240 0      0   3.0 1.7 49 240 7.1 3.8 88 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 2.3 1.1  21 250 0      0   2.8 1.6 38 240 6.8 3.7 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 2.4 1.1  22 250 0      0   3.0 1.7 50 240 7.6 4.1 120 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 2.4 1.1  23 250 0      0   3.2 1.8 59 240 6.6 3.6 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 2.4 1.0  23 250 0      0   3.2 1.8 52 240 7.0 3.7 100 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 2.4 1.0  21 250 .0082 0   3.2 1.8 57 230 7.2 3.9 110 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 2.4 1.0  20 250 0      0   3.1 1.8 55 240 6.5 3.5 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 2.6 1.1  23 250 .0082 0   3.1 1.8 48 240 7.4 3.9 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 2.3 1.0  19 240 0      0   3.2 1.8 47 240 7.2 3.9 88 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 2.4 1.1  22 250 0      0   3.2 1.8 52 230 7.3 3.9 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 2.4 1.1  23 250 .0082 0   3.2 1.8 45 240 6.9 3.7 82 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 2.6 1.1  19 250 0      0   3.5 2.0 78 240 6.9 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 2.4 1.0  20 250 0      0   3.3 1.8 54 240 7.7 4.1 120 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 2.4 1.0  20 250 0      0   3.2 1.8 54 230 7.4 3.9 130 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 2.4 1.1  20 250 .0082 0   3.1 1.8 62 240 7.1 3.8 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 2.5 1.1  24 250 .0082 0   3.2 1.8 53 230 6.6 3.5 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 2.5 1.0  21 250 .0082 0   3.5 2.0 77 240 7.6 4.0 85 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 2.5 1.1  22 250 .0082 0   3.3 1.8 51 230 6.7 3.6 80 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 2.4 1.1  21 250 0      0   3.2 1.8 52 240 6.5 3.5 110 320
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 2.4 1.1  25 250 0      0   3.3 1.9 69 230 7.5 4.0 110 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 2.5 1.1  23 260 0      0   3.3 1.9 60 230 7.2 3.8 89 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 2.5 1.1  23 240 .0082 0   3.1 1.8 56 230 6.7 3.6 80 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 2.4 1.1  20 250 0      0   3.1 1.8 53 230 7.5 4.0 160 320
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 2.6 1.1  23 260 0      0   3.4 1.9 59 250 7.9 4.2 130 330
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 12   3.9  110 430 .23   0   3.8 2.1 63 240 8.5 4.5 91 330
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 2.3 1.0  21 240 0      0   2.9 1.6 54 240 7.8 4.1 96 340
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 2.5 1.1  24 260 0      0   3.8 2.1 69 290 7.1 3.9 140 310
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 2.5 1.0  20 250 0      0   3.1 1.7 66 230 7.2 3.8 85 310
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 2.5 1.1  22 260 .0082 0   3.3 1.9 58 250 7.2 3.8 130 310
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 2.3 1.0  19 250 0      0   3.7 2.0 53 260 8.8 4.8 170 330
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 2.4 1.0  22 240 0      0   3.2 1.9 56 250 7.7 4.1 88 310
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 2.3 1.1  19 250 0      0   3.2 1.8 61 250 7.2 3.8 130 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 2.3 1.0  20 240 0      0   3.3 1.9 53 240 7.5 4.0 110 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 2.4 1.1  21 240 0      0   3.1 1.8 60 240 7.1 3.8 130 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 2.4 1.0  20 260 0      0   3.1 1.8 47 240 7.8 4.1 120 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 2.4 1.1  20 250 0      0   3.2 1.8 57 240 6.5 3.5 97 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 2.3 1.0  19 250 0      0   3.0 1.7 50 230 6.8 3.6 90 310
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 2.3 1.1  24 250 0      0   3.4 1.9 71 250 7.2 3.8 110 330
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 2.6 1.1  23 250 0      0   3.1 1.7 38 240 6.9 3.7 81 320
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 2.5 1.1  20 260 0      0   3.3 1.9 67 240 7.4 3.9 120 320
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 2.6 1.1  21 260 .0082 0   3.3 1.9 52 250 7.2 3.8 140 310
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 2.4 1.1  23 250 .0082 0   3.4 1.9 37 240 7.0 3.7 110 310
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 2.5 1.1  21 260 .0082 0   3.0 1.7 38 240 7.4 4.0 130 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c 17   5.4  150 510 0      0   4.0 2.3 50 260 78   46   510 7000
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 2.6 1.1  25 260 0      0   3.4 1.9 56 250 7.6 4.1 110 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 2.3 1.1  22 240 0      0   3.2 1.9 58 260 7.0 3.7 92 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 2.4 1.1  22 250 0      0   3.4 1.9 54 250 7.3 3.9 120 320
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 2.5 1.1  23 250 .0082 0   3.2 1.8 61 230 6.6 3.5 91 310
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 2.3 1.0  21 240 0      0   3.0 1.7 66 230 7.3 3.9 140 320
termination-crafted-lit/cstrncmp_false-no-overflow.c 2.6 1.1  25 260 0      0   4.6 2.6 82 300 9.0 4.9 120 350
termination-crafted-lit/gcd1_false-no-overflow.c 2.5 1.1  25 260 .0082 0   3.0 1.7 37 240 6.9 3.7 94 310
termination-crafted-lit/joey_false-no-overflow.c 2.3 1.0  20 250 0      0   3.2 1.8 58 240 7.4 4.1 99 310
termination-crafted-lit/min_rf_false-no-overflow.c 2.6 1.1  22 250 .025  0   3.5 2.0 73 240 6.8 3.6 80 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900   860    12000 4900 0      0   900    880    13000 5300 960   870   15000 4000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 900   870    12000 4200 0      0   4.4  2.4  86 280 8.6 4.6 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 8.0 2.6  62 330 0      0   4.1  2.3  84 280 7.8 4.2 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 910   870    10000 9000 0      0   4.0  2.2  76 270 960   820   16000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900   790    13000 5600 0      0   900    880    21000 4700 960   790   12000 3100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900   850    11000 4500 0      0   4.0  2.3  72 280 450   360   4300 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 230   210    2800 2800 0      0   900    880    12000 3900 48   28   640 2600
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 900   840    10000 3500 0      0   4.5  2.5  91 280 8.7 4.7 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 900   860    11000 4300 0      0   4.3  2.4  80 280 9.0 4.9 160 340
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 900   880    7400 2600 0      0   4.1  2.3  70 280 8.6 4.7 140 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 900   850    13000 5900 0      0   900    870    12000 4600 7.8 4.2 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 900   850    10000 4600 0      0   900    860    10000 4800 8.6 4.6 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 900   890    6500 4700 0      0   4.1  2.3  72 270 10   5.5 170 370
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900   810    13000 5800 0      0   900    840    13000 6100 960   840   18000 4900
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 2.8 1.2  24 270 .025  0   2.9  1.6  47 230 15   8.9 260 380
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 2.8 1.1  21 250 .0082 0   3.1  1.8  54 240 12   6.5 210 420
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 910   860    9500 13000 0      0   4.4  2.4  70 280 9.7 5.2 150 340
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 910   870    8000 11000 0      0   900    840    9800 5600 960   820   17000 4800
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 910   870    10000 8900 0      0   3.8  2.1  83 280 23   13   260 590
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 8.5 2.7  67 340 0      0   4.3  2.4  90 280 7.1 3.9 130 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 910   870    8500 9000 0      0   3.8  2.1  70 270 960   820   11000 4700
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900   850    13000 4500 0      0   4.1  2.3  68 270 430   330   4400 7000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 230   210    3200 2700 0      0   900    880    19000 3800 45   27   390 2400
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 900   860    10000 7700 0      0   3.8  2.1  53 280 6.7 3.6 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 2.4 1.1  22 250 0      0   3.2  1.8  54 240 7.4 4.0 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 910   880    10000 9100 0      0   3.9  2.2  65 270 7.8 4.2 140 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 900   860    13000 4500 0      0   4.4  2.4  72 280 8.5 4.5 160 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 900   860    10000 4600 0      0   4.6  2.6  84 280 8.1 4.3 150 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 900   870    13000 4500 0      0   5.2  2.9  77 300 7.9 4.2 130 310
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 2.4 1.1  21 250 .0082 0   3.0  1.7  51 230 8.3 4.5 140 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 910   880    7600 5900 0      0   4.2  2.3  85 270 8.3 4.4 160 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 2.5 1.1  21 260 0      0   3.1  1.8  59 230 8.7 4.7 150 350
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 16   5.3  140 440 0      0   4.1  2.3  87 280 120   78   1200 3100
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   830    11000 4900 0      0   900    870    14000 5000 960   850   18000 4800
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 900   870    12000 5000 0      0   4.7  2.6  89 280 7.5 4.0 130 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 910   860    12000 8900 0      0   3.8  2.2  77 270 20   12   270 590
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 910   870    8600 9000 0      0   3.8  2.1  62 270 8.6 4.5 180 340
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 910   860    13000 8700 0      0   3.8  2.2  71 280 9.1 4.9 170 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 900   880    11000 2500 0      0   4.0  2.2  70 280 7.2 3.9 140 320
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 910   790    9000 6900 0      0   900    850    14000 6700 960   800   11000 4700
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 900   860    11000 4500 0      0   4.3  2.4  65 270 7.6 4.0 150 320
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 2.4 1.1  21 260 .0082 0   3.1  1.8  53 240 8.1 4.3 150 320
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   880    8900 2200 0      0   4.2  2.3  66 280 960   820   12000 2600
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 2.4 1.0  21 250 0      0   3.4  1.9  61 240 12   6.4 200 420
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 2.2 1.0  20 240 0      0   3.4  1.9  75 250 960   800   11000 3400
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 900   890    5600 1200 0      0   4.0  2.2  60 280 8.7 4.7 170 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 900   880    8100 4700 0      0   4.7  2.6  83 280 7.9 4.2 140 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 5.9 2.3  47 290 0      0   3.8  2.1  87 270 8.4 4.4 150 330
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 910   860    11000 9500 0      0   3.9  2.2  73 280 8.1 4.3 140 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 900   850    10000 6200 0      0   4.1  2.3  66 280 9.0 4.8 170 330
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 900   870    10000 5900 0      0   4.4  2.5  76 280 8.3 4.4 150 340
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 900   860    11000 700 0      0   4.0  2.2  76 280 7.2 3.9 150 310
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 900   850    11000 800 0      0   330    320    4400 7000 8.2 4.5 150 320
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 900   850    12000 2800 0      0   350    330    4000 7000 8.1 4.4 140 320
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 900   870    13000 5100 0      0   5.6  3.0  93 290 7.8 4.2 140 310
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 910   860    10000 8500 0      0   4.4  2.5  75 280 7.5 4.0 87 330
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 45   31    430 670 0      0   4.4  2.4  73 280 960   810   19000 5000
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 2.6 1.1  22 260 0      0   5.6  3.1  78 290 8.3 4.5 150 330
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 2.6 1.1  22 260 0      0   4.5  2.6  60 300 8.2 4.3 160 330
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 2.5 1.1  23 250 0      0   4.4  2.4  95 290 8.3 4.5 130 330
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 2.5 1.1  22 240 0      0   6.8  3.7  110 320 7.8 4.3 150 330
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 2.5 1.1  24 250 0      0   4.8  2.8  91 300 8.3 4.5 150 330
termination-crafted-lit/genady_true-termination_true-no-overflow.c 900   860    12000 740 0      0   3.7  2.1  63 270 12   6.7 170 450
termination-crafted-lit/strchr_true-no-overflow.c 2.5 1.1  21 260 0      0   5.1  2.8  86 290 8.0 4.3 160 320
termination-numeric/Addition01_false-no-overflow.c 2.3 1.0  20 240 0      0   3.4 1.9 49 250 7.2 3.8 86 320
termination-numeric/Avg_true_false-no-overflow.c 2.4 1.1  21 240 0      0   3.3 1.9 62 240 7.1 3.8 140 310
termination-numeric/Binomial_true-termination_false-no-overflow.c 2.7 1.1  25 250 0      0   3.1 1.7 61 220 96   64   1900 1200
termination-numeric/Et1_true_false-no-overflow.c 2.5 1.1  22 250 .016  0   3.3 1.9 60 240 8.6 4.7 160 340
termination-numeric/Et2_true_false-no-overflow.c 2.4 1.1  21 240 0      0   3.8 2.1 66 250 6.9 3.7 87 320
termination-numeric/Et3_true_false-no-overflow.c 2.5 1.1  22 250 .016  0   3.5 2.0 73 240 7.3 3.9 94 320
termination-numeric/Et4_true_false-no-overflow.c 2.6 1.1  26 250 .041  0   3.5 2.0 77 240 8.9 4.8 160 340
termination-numeric/MultCommutative_false-no-overflow.c 2.3 1.0  21 240 0      0   3.4 1.9 73 240 12   7.0 170 400
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 2.4 1.0  23 250 0      0   3.5 1.9 53 260 97   87   1100 1100
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 2.4 1.1  21 240 0      0   3.6  2.0  69 250 800   640   8800 7000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 2.3 1.0  22 250 0      0   3.4  1.9  60 250 960   800   19000 4400
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 2.2 1.0  18 250 0      0   3.4  1.9  80 240 960   890   15000 5700
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 2.4 1.1  22 240 0      0   3.3  1.9  53 250 7.8 4.3 130 330
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 2.3 1.0  18 240 0      0   3.2  1.8  43 250 960   790   17000 4800
termination-numeric/Parts_true-termination_true-no-overflow.c 3.2 1.3  30 260 0      0   2.8  1.6  50 190 960   800   17000 4800
termination-numeric/TwoWay_true-termination_true-no-overflow.c 2.4 1.1  23 250 0      0   3.3  1.9  76 240 19   12   270 480
termination-numeric/gcd01_true-termination_true-no-overflow.c 2.3 1.0  20 250 0      0   3.2  1.8  48 240 8.2 4.5 140 330
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 7.0 2.8  61 300 0      0   3.9  2.2  69 280 63   38   590 1100
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 2.3 1.0  23 250 0      0   3.3  1.9  66 240 960   800   13000 4400
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 2.2 .99 20 250 0      0   2.7  1.5  53 190 960   810   11000 5200
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 2.3 1.0  21 240 0      0   2.9  1.6  62 200 960   810   12000 4900
termination-numeric/twisted_true-termination_true-no-overflow.c 900   830    10000 5100 0      0   6.0  3.2  97 300 960   800   12000 2800
recursive/Addition02WithOverflowBug_false-no-overflow.c 2.3 1.0  18 240 0      0   3.3 1.9 42 250 6.9 3.7 87 320
recursive/Addition03_false-no-overflow.c 2.3 1.0  22 240 0      0   3.4 2.0 59 260 7.1 3.8 110 320
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 2.4 1.1  22 250 0      0   3.8 2.1 76 260 7.1 3.8 110 310
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 2.3 1.1  20 240 0      0   3.4  1.9  53 250 460   340   6600 7000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 2.4 1.0  20 240 0      0   3.5  2.0  67 250 560   440   6600 7000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 2.4 1.0  21 240 0      0   3.4  1.9  56 250 490   400   5300 7000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 2.4 1.1  21 240 0      0   3.4  1.9  55 240 680   550   7400 7000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  21 240 0      0   3.4  1.9  59 240 960   810   12000 4700
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  18 240 0      0   3.5  2.0  73 250 960   810   13000 4700
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  19 240 0      0   3.5  2.0  58 240 960   800   12000 4200
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  21 240 0      0   3.3  1.9  62 240 7.0 3.7 120 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 2.4 1.0  19 250 0      0   3.5  2.0  72 250 960   800   11000 4100
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  20 240 0      0   3.4  1.9  60 250 960   800   11000 4100
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 2.3 1.0  20 240 0      0   3.4  1.9  76 250 960   890   14000 5800
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  18 240 0      0   3.3  1.9  53 250 42   24   600 1200
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  19 250 0      0   3.3  1.8  52 250 960   890   15000 5700
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 2.4 1.0  21 240 0      0   3.3  1.9  54 240 960   890   20000 5800
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  21 240 0      0   3.3  1.9  59 250 960   890   13000 5800
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 2.4 1.0  22 240 0      0   3.2  1.8  51 240 9.7 5.3 150 360
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  19 250 0      0   3.1  1.8  51 250 9.8 5.3 160 360
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.1  22 240 0      0   3.4  1.9  56 240 960   840   12000 2000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 2.5 1.1  26 250 0      0   3.9  2.1  65 250 960   840   19000 2000
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  20 240 0      0   3.6  2.0  77 240 8.0 4.3 140 320
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 2.4 1.1  24 250 0      0   3.5  2.0  60 240 18   9.9 260 490
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 2.4 1.0  21 240 0      0   3.8  2.2  67 260 960   810   18000 4800
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  21 240 0      0   3.1  1.8  50 250 960   800   14000 4200
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 2.3 1.0  23 240 0      0   3.3  1.9  57 250 960   790   11000 4300
bitvector/jain_1_false-no-overflow.i 2.4 1.1  22 240 0      0   3.2 1.8 54 250 7.1 3.8 140 310
bitvector/jain_2_false-no-overflow.i 2.3 1.0  22 250 0      0   3.4 1.9 47 250 7.4 3.9 86 310
bitvector/jain_4_false-no-overflow.i 2.4 1.1  19 240 0      0   3.7 2.1 79 250 7.4 4.0 160 310
bitvector/jain_5_false-no-overflow.i 900   850    11000 1400 0      0   3.7 2.1 59 280 97   65   1800 1500
bitvector/jain_6_false-no-overflow.i 2.5 1.1  23 250 0      0   3.5 2.0 67 250 6.6 3.6 100 310
bitvector/jain_7_false-no-overflow.i 2.5 1.1  20 250 0      0   3.5 2.0 58 260 6.7 3.6 99 310
bitvector/modulus_false-no-overflow.i 2.8 1.1  27 280 0      0   3.3 1.8 61 240 7.0 3.7 75 310
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 23   6.3  180 590 0      0   12    6.1  170 360 8.3 4.5 180 330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 21   6.1  170 570 0      0   11    6.0  140 350 8.7 4.7 160 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i 85   64    900 1400 0      0   17    8.8  170 600 7.8 4.2 150 320
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 5.2 3.2  55 290 0      0   5.9  3.4  72 330 9.2 4.9 130 340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 74   69    700 440 0      0   5.2  2.9  110 300 7.9 4.3 140 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 76   71    570 430 0      0   5.0  2.9  91 300 7.9 4.3 180 310
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2.9 1.2  25 250 0      0   4.7  2.6  100 280 13   7.2 230 440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 4.1 1.6  36 260 0      0   4.8  2.6  97 290 8.3 4.4 160 330
bitvector/jain_1_true-unreach-call_true-no-overflow.i 910   880    7900 8800 0      0   4.2  2.3  74 280 7.0 3.7 140 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i 910   890    8200 9500 0      0   4.2  2.3  72 270 7.2 3.8 130 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i 910   890    9400 10000 0      0   4.8  2.7  94 280 6.6 3.5 120 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i 900   850    11000 990 0      0   4.2  2.3  83 270 7.0 3.8 140 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i 910   890    10000 10000 0      0   4.4  2.5  77 280 6.9 3.7 130 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i 910   890    5300 5600 0      0   4.4  2.4  75 270 6.7 3.6 130 320
bitvector/modulus_true-unreach-call_true-no-overflow.i 900   860    9100 4200 0      0   5.6  3.0  88 290 6.9 3.7 140 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 3.1 1.3  28 260 0      0   4.7  2.6  81 280 7.4 4.0 160 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 32   15    260 730 0      0   4.6  2.6  88 280 8.2 4.4 120 350
bitvector/parity_true-unreach-call_true-no-overflow.i 16   4.4  110 430 0      0   5.1  2.8  91 280 7.2 3.8 130 320
bitvector/sum02_false-unreach-call_true-no-overflow.i 900   850    10000 1800 0      0   4.8  2.6  76 280 7.2 3.8 130 310
bitvector/sum02_true-unreach-call_true-no-overflow.i 900   840    11000 1800 0      0   4.8  2.6  77 280 7.1 3.8 160 310
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 328 68000   65000   790000 480000 .80  0   328 550   310   9500 40000   328 1700 990 24000 70000   328 13000   12000   200000 130000   328 44000   37000   620000 270000  
    correct results 168 1300   870   13000 52000 .75  0   143 470   260   8100 34000   142 1000 550 16000 46000   23 1900   1800   33000 15000   24 1400   1100   25000 21000  
        correct true 25 920   710   10000 15000 0     0   47 0   0   0 0   0 0 0 0 0   23 1900   1800   33000 15000   24 1400   1100   25000 21000  
        correct false 143 370   160   3300 36000 .75  0   96 470   260   8100 34000   142 1000 550 16000 46000   0 0   0   0 0   0 0   0   0 0  
    correct-unconfimed results 3 38   12   290 1300 0     0   2 8.2 4.6 130 510   0 150 89 1000 14000   0 2.8 1.5 35 190   0 5.8 3.1 110 300  
        correct-unconfirmed true 1 2.3 1.0 19 240 0     0   2 0   0   0 0   0 0 0 0 0   0 2.8 1.5 35 190   0 5.8 3.1 110 300  
        correct-unconfirmed false 2 35   11   270 1000 0     0   0 8.2 4.6 130 510   0 150 89 1000 14000   0 0   0   0 0   0 0   0   0 0  
    incorrect results 9 23   9.9 200 2300 .049 0   0 0   0   0 0   0 0 0 0 0   8 930   890   21000 5600   9 85   47   1500 3100  
        incorrect true 0
        incorrect false 9 23   9.9 200 2300 .049 0   0 0   0   0 0   0 0 0 0 0   2 930   890   21000 5600   0 85   47   1500 3100  
score (328 tasks, max score: 491) 50
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]