Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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 08:59:26 CET [[ 2017-01-15 01:13:08 CET ]] [[ 2017-01-15 01:19:20 CET ]] [[ 2017-01-15 01:18:26 CET ]] [[ 2017-01-15 01:22:10 CET ]]
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0859.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0859.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 .094 .094 .91 24 .99 0   4.2  2.3  88 260 6.9 3.7 89 310
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i .085 .085 1.0  24 .99 0   4.2  2.3  86 260 7.2 3.8 140 310
signedintegeroverflow-regression/Division_false-no-overflow.c.i .11  .11  .85 24 .99 0   4.3  2.4  76 260 6.9 3.7 77 310
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i .088 .087 1.1  24 .99 0   4.3  2.4  83 250 6.2 3.3 72 310
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i .12  .12  .99 24 .99 0   4.4  2.4  85 250 6.6 3.5 78 310
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i .12  .12  .76 24 .99 0   4.3  2.4  92 250 6.6 3.5 72 310
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i .099 .098 .84 24 .99 0   4.0  2.3  68 250 7.0 3.7 150 300
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i .084 .085 .94 24 .99 0   4.3  2.4  87 250 6.9 3.7 83 320
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i .082 .082 1.0  24 .84 0   4.3  2.4  88 250 6.7 3.5 73 320
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i .097 .097 1.1  24 .99 0   4.1  2.3  90 250 7.1 3.8 110 310
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i 900     810     11000    2500 .84 0   .51 .32 10   40 5.9 3.2 110 290
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i 71     64     860    15000 .99 0   .52 .34 11   41 6.5 3.4 130 300
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i 62     58     700    15000 .99 0   .52 .32 11   40 5.8 3.1 120 290
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i 66     59     690    15000 .99 0   .51 .32 11   40 5.8 3.1 110 300
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i 68     61     860    15000 .99 0   .50 .32 12   39 6.1 3.3 130 320
termination-crafted/2Nested_false-no-overflow.c .080 .079 .87 23 .99 0   3.2  1.8  70 240 6.9 3.7 100 310
termination-crafted/4NestedWith3Variables_false-no-overflow.c .086 .086 .85 23 .84 0   2.9  1.7  66 230 7.7 4.1 140 320
termination-crafted/Ackermann_false-no-overflow.c .092 .092 .75 23 .84 0   3.1  1.8  70 240 7.0 3.8 90 310
termination-crafted/Bangalore_false-no-overflow.c .074 .075 .84 23 .84 0   3.3  1.9  72 240 6.7 3.6 76 320
termination-crafted/Bangalore_v3_false-no-overflow.c .091 .091 .72 23 .99 0   3.2  1.8  70 240 7.2 3.8 110 320
termination-crafted/Benghazi_nondet_false-no-overflow.c .10  .10  .82 23 .84 0   3.1  1.7  70 240 6.9 3.7 110 300
termination-crafted/Binary_Search_false-no-overflow.c .094 .093 .91 23 .84 0   3.2  1.8  74 240 6.9 3.7 86 320
termination-crafted/Cairo_nondet_false-no-overflow.c .079 .079 .98 23 .99 0   3.4  1.9  70 240 7.0 3.8 91 320
termination-crafted/Collatz_unknown-termination_false-no-overflow.c .074 .076 .80 23 .99 0   .52 .34 13 41 5.8 3.1 95 300
termination-crafted/Copenhagen_disj_false-no-overflow.c .087 .087 .76 23 .84 0   3.2  1.8  69 240 7.9 4.2 100 330
termination-crafted/Gothenburg_false-no-overflow.c .077 .077 .80 23 .99 0   3.3  1.9  65 240 7.2 3.8 98 320
termination-crafted/Gothenburg_v2_false-no-overflow.c .11  .11  .76 23 .99 0   3.3  1.9  74 240 7.1 3.9 150 310
termination-crafted/Hanoi_2vars_false-no-overflow.c .074 .074 .86 23 .99 0   3.2  1.8  64 240 6.9 3.6 110 310
termination-crafted/Hanoi_3vars_false-no-overflow.c .077 .076 .98 23 .99 0   3.2  1.8  63 230 7.0 3.7 86 310
termination-crafted/Hanoi_plus_false-no-overflow.c .079 .079 .87 23 .84 0   2.9  1.7  68 230 7.2 3.8 130 320
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c .11  .11  .70 23 .99 0   3.0  1.7  59 240 7.0 3.8 88 320
termination-crafted/Mysore_false-no-overflow.c .078 .078 .77 23 .99 0   3.2  1.8  66 230 6.9 3.7 92 320
termination-crafted/NestedRecursion_1a_false-no-overflow.c .081 .080 .79 23 .84 0   3.5  1.9  71 250 7.4 3.9 150 310
termination-crafted/NestedRecursion_2a_false-no-overflow.c .076 .075 .89 23 .99 0   3.2  1.8  71 250 7.5 4.0 140 320
termination-crafted/NonTermination1_false-no-overflow.c .077 .077 .80 23 .99 0   3.1  1.7  58 230 7.2 3.8 150 320
termination-crafted/NonTermination2_false-no-overflow.c .077 .077 .75 23 .99 0   3.3  1.9  70 240 7.3 3.8 89 310
termination-crafted/NonTermination4_false-no-overflow.c .10  .099 1.2  23 .84 0   3.8  2.1  77 240 6.0 3.3 80 300
termination-crafted/NonTerminationSimple2_false-no-overflow.c .075 .075 .75 23 .99 0   3.1  1.8  65 240 6.9 3.7 110 320
termination-crafted/NonTerminationSimple3_false-no-overflow.c .11  .11  .71 23 .99 0   3.1  1.8  70 240 7.6 4.0 88 330
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900     900     11000    8800 .99 0   .49 .33 11 39 5.3 2.8 80 290
termination-crafted/NonTerminationSimple5_false-no-overflow.c .10  .10  .88 23 .99 0   3.2  1.8  62 240 6.8 3.7 110 320
termination-crafted/NonTerminationSimple6_false-no-overflow.c .11  .11  .59 23 .99 0   3.1  1.8  72 240 6.6 3.5 100 310
termination-crafted/NonTerminationSimple8_false-no-overflow.c .080 .079 .86 23 .99 0   3.2  1.8  64 240 7.5 4.0 120 320
termination-crafted/NonTerminationSimple9_false-no-overflow.c .11  .11  .68 23 .99 0   3.1  1.8  57 230 6.7 3.6 85 320
termination-crafted/Pure2Phase_false-no-overflow.c .080 .080 .75 23 .84 0   3.1  1.8  67 240 7.1 3.8 130 310
termination-crafted/Pure3Phase_false-no-overflow.c .096 .096 .74 23 .99 0   3.3  1.9  65 240 7.2 3.8 110 320
termination-crafted/RecursiveMultiplication_false-no-overflow.c .11  .11  .60 23 .99 0   3.3  1.9  64 250 6.7 3.5 90 310
termination-crafted/RecursiveNonterminating_false-no-overflow.c .098 .098 .78 23 .99 0   2.9  1.6  49 240 7.1 3.8 110 320
termination-crafted/Rotation180_false-no-overflow.c .087 .087 .75 23 .99 0   3.1  1.8  71 240 6.1 3.3 85 310
termination-crafted/Singapore_false-no-overflow.c .078 .078 .82 23 .99 0   3.1  1.8  72 230 6.7 3.6 84 310
termination-crafted/Singapore_plus_false-no-overflow.c .088 .087 .87 23 .84 0   3.1  1.8  64 230 6.7 3.6 84 320
termination-crafted/Singapore_v1_false-no-overflow.c .079 .078 .78 23 .99 0   3.3  1.9  68 240 7.8 4.1 120 330
termination-crafted/Singapore_v2_false-no-overflow.c .11  .11  .70 23 .84 0   3.3  1.8  71 240 7.1 3.8 90 320
termination-crafted/Stockholm_false-no-overflow.c .084 .084 .87 23 .99 0   3.2  1.8  67 240 7.0 3.7 130 320
termination-crafted/Thun_false-no-overflow.c .078 .078 .80 23 .99 0   3.3  1.9  71 240 7.4 3.9 130 330
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c .089 .089 .90 23 .84 0   3.2  1.8  64 240 7.2 3.9 76 320
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c .11  .11  1.1  23 .99 0   3.8  2.1  86 240 11   6.2 150 400
termination-crafted/aaron2_false-no-overflow.c .11  .11  .62 23 .99 0   3.2  1.8  61 240 7.3 3.9 90 320
termination-crafted/aaron3_false-no-overflow.c .11  .11  .85 23 .84 0   3.2  1.8  62 240 7.8 4.1 160 310
termination-crafted/4BitCounterPointer_true-no-overflow.c 900     840     9500    3800 .99 0   .55 .36 12   41 6.2 3.3 140 300
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c 900     900     8500    12000 .99 0   .53 .34 12   41 5.6 3.0 110 300
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c 310     310     3800    15000 .99 0   .54 .36 11   39 6.2 3.3 130 300
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c 900     900     5300    4700 .86 0   .54 .36 11   40 6.1 3.2 120 300
termination-crafted/Bangalore_true-no-overflow.c 900     900     12000    280 .99 0   .59 .38 12   45 5.6 3.0 110 290
termination-crafted/Bangalore_v2_true-no-overflow.c 900     900     11000    290 .99 0   .51 .33 11   40 5.5 2.9 110 290
termination-crafted/Bangalore_v4_true-no-overflow.c 360     360     4200    15000 .99 0   .56 .35 12   44 5.6 3.0 110 290
termination-crafted/Benghazi_true-no-overflow.c 900     900     12000    10000 .99 0   .52 .35 12   40 5.8 3.1 130 300
termination-crafted/Cairo_step2_true-no-overflow.c 900     900     12000    8600 .99 0   .52 .34 10   40 6.7 3.5 130 300
termination-crafted/Cairo_true-no-overflow.c 900     900     11000    8600 .99 0   .50 .32 12   40 6.2 3.3 120 300
termination-crafted/Copenhagen_true-no-overflow.c 900     900     10000    5100 .99 0   .51 .33 10   39 5.7 3.1 120 300
termination-crafted/Division_true-no-overflow.c 850     850     10000    15000 .99 0   .51 .33 10   40 5.8 3.1 110 300
termination-crafted/LexIndexValue-Array_true-no-overflow.c 900     900     7100    8900 .99 0   .52 .35 12   42 5.6 3.1 120 300
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900     900     7200    10000 .84 0   .66 .42 12   40 6.0 3.2 120 300
termination-crafted/Madrid_true-no-overflow.c 900     660     10000    12000 .99 0   .51 .32 11   43 6.0 3.2 120 300
termination-crafted/McCarthy91_Iteration_true-no-overflow.c 900     900     8600    650 .84 0   .50 .31 11   39 6.3 3.3 110 300
termination-crafted/McCarthy91_Recursion_true-no-overflow.c 900     900     8800    7200 .99 0   .50 .33 13   39 5.9 3.1 130 300
termination-crafted/MenloPark_true-no-overflow.c 900     900     11000    9400 .99 0   .51 .33 12   41 5.5 3.0 120 290
termination-crafted/MutualRecursion_1a_true-no-overflow.c 900     900     7700    14000 .99 0   .58 .37 13   42 5.9 3.2 120 290
termination-crafted/MutualRecursion_1b_true-no-overflow.c 900     900     9600    4800 .99 0   .51 .34 12   39 6.3 3.3 120 300
termination-crafted/NestedRecursion_1b_true-no-overflow.c 900     900     8700    9700 .99 0   .54 .36 11   41 6.0 3.2 110 300
termination-crafted/NestedRecursion_1c_true-no-overflow.c 770     770     9100    15000 .99 0   .48 .32 12   40 6.0 3.2 120 300
termination-crafted/NestedRecursion_1d_true-no-overflow.c 900     900     12000    3700 .99 0   .55 .35 13   41 6.1 3.2 130 300
termination-crafted/NestedRecursion_2b_true-no-overflow.c 760     760     6700    15000 .99 0   .52 .33 10   41 5.7 3.1 120 290
termination-crafted/NestedRecursion_2c_true-no-overflow.c 700     700     6300    15000 .84 0   .70 .45 10   40 5.9 3.2 120 290
termination-crafted/NonTermination3_true-no-overflow.c 900     880     8200    1700 .99 0   .55 .37 12   43 5.8 3.1 110 290
termination-crafted/NonTerminationSimple7_true-no-overflow.c 250     250     2600    15000 .99 0   .52 .32 11   42 6.1 3.3 120 310
termination-crafted/Nyala-2lex_true-no-overflow.c 900     900     8900    8600 .99 0   .56 .36 12   42 6.7 3.5 120 300
termination-crafted/Parallel_true-no-overflow.c 900     900     8300    5100 .84 0   .51 .32 10   40 6.0 3.2 120 300
termination-crafted/Piecewise_true-no-overflow.c 350     340     4300    15000 .99 0   .54 .37 12   39 5.5 3.0 110 290
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c 900     900     11000    9600 .84 0   .53 .34 12   42 5.4 3.0 110 290
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c 190     190     2600    15000 .84 0   .52 .34 12   39 6.0 3.2 120 290
termination-crafted/Waldkirch_true-no-overflow.c 900     900     9300    9600 .99 0   .59 .38 8.6 41 6.3 3.3 110 300
termination-crafted/WhileFalse_true-no-overflow.c 900     800     11000    13000 .99 0   .49 .32 10   39 6.2 3.3 120 300
termination-crafted/WhileTrue_true-no-overflow.c 520     300     5500    15000 .99 0   .50 .31 9.6 40 6.0 3.2 130 300
termination-crafted/easy1_true-no-overflow.c 180     180     2100    15000 .99 0   .52 .35 11   40 5.7 3.0 120 290
termination-crafted/easy2_true-no-overflow.c 190     180     2400    15000 .84 0   .52 .33 11   42 6.2 3.4 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c .11  .11  .75 23 .99 0   3.3  1.8  66 230 12   6.2 120 430
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c .078 .077 1.1  23 .99 0   3.2  1.8  68 240 11   5.8 170 380
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c .080 .079 .87 23 .84 0   3.2  1.8  64 240 7.6 4.1 110 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c .077 .076 .83 23 .99 0   3.5  2.0  76 230 7.4 3.9 92 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c .093 .092 .95 23 .99 0   3.4  2.0  59 250 8.4 4.6 150 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c .075 .075 .84 23 .99 0   3.5  2.0  78 240 7.0 3.8 87 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c .10  .10  .83 23 .99 0   93    80    1100 3700 7.6 4.1 120 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c .097 .098 .88 23 .84 0   3.2  1.8  60 240 7.7 4.1 89 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c 12     12     170    230 .99 0   92    81    1200 3200 7.4 4.0 89 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c .079 .079 .76 23 .99 0   2.8  1.6  48 240 7.8 4.2 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c .075 .074 1.1  23 .99 0   3.2  1.8  64 240 9.2 5.0 96 350
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c .089 .089 .79 23 .99 0   3.3  1.9  67 240 6.5 3.5 87 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c .076 .076 .91 23 .99 0   3.4  1.9  70 240 6.6 3.6 87 310
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c .076 .075 .76 23 .99 0   3.5  2.0  76 240 7.5 4.0 97 320
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c .094 .093 .79 23 .99 0   3.3  1.9  72 240 7.6 4.0 91 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c .11  .11  .83 23 .84 0   3.4  1.9  75 230 7.4 3.9 92 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c .088 .088 .86 23 .84 0   3.4  1.9  71 240 7.2 3.8 88 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c .12  .12  .75 23 .99 0   3.3  1.8  66 240 7.2 3.9 130 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c .11  .11  .77 23 .84 0   3.3  1.9  79 240 6.9 3.7 76 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c .11  .11  .74 23 .99 0   3.8  2.1  75 240 7.5 4.0 98 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c .11  .11  .70 23 .84 0   3.3  1.9  54 240 7.0 3.8 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c .11  .11  .61 23 .88 0   3.0  1.7  64 240 7.2 3.9 83 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c .099 .098 .79 23 .99 0   3.2  1.8  66 240 8.3 4.4 140 350
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c .075 .075 .73 23 .99 0   3.0  1.7  59 230 7.5 4.0 120 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c .10  .10  .85 23 .99 0   3.4  2.0  53 240 6.9 3.6 83 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c .075 .075 .75 23 .99 0   3.1  1.8  65 240 6.8 3.6 86 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c .087 .087 1.0  23 .99 0   3.3  1.9  72 240 8.3 4.4 61 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c .089 .088 .75 23 .99 0   3.4  1.9  67 240 6.9 3.7 98 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c .077 .077 .82 23 .99 0   3.2  1.8  65 240 6.7 3.6 86 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c .081 .081 .74 23 .99 0   3.2  1.8  66 240 6.9 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c .11  .11  .70 23 .99 0   3.5  2.0  76 240 6.8 3.6 98 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c .096 .096 .93 23 .99 0   3.2  1.8  65 240 6.9 3.7 86 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c .10  .10  .82 23 .99 0   3.2  1.9  72 240 6.8 3.6 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c .091 .091 .92 23 .99 0   3.5  2.0  72 240 6.7 3.6 78 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c .076 .075 .87 23 .84 0   3.4  1.9  78 240 7.4 4.0 94 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c .077 .077 .80 23 .99 0   3.2  1.8  67 240 8.1 4.3 130 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c .10  .11  .71 23 .99 0   4.0  2.3  58 240 8.6 4.6 130 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c .11  .11  .59 23 .99 0   3.3  1.9  73 240 6.9 3.6 98 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c .074 .075 .85 23 .84 0   3.2  1.8  68 230 6.6 3.5 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c .077 .077 .97 23 .99 0   3.3  1.9  68 230 6.6 3.5 87 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c .11  .11  .69 23 .84 0   3.5  2.0  61 230 6.9 3.7 98 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c .076 .076 .78 23 .99 0   3.1  1.8  57 230 7.5 4.0 80 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c .078 .077 .75 23 .84 0   3.3  1.9  69 230 6.7 3.6 80 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c .10  .10  .85 23 .99 0   3.6  2.0  76 240 6.7 3.5 88 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c .095 .096 .77 23 .99 0   3.3  1.9  64 240 7.1 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c .088 .088 .87 23 .84 0   3.3  1.8  72 240 6.8 3.6 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c .11  .11  .75 23 .99 0   3.3  1.9  61 240 7.8 4.2 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c .075 .075 .86 23 .84 0   3.2  1.8  68 240 6.7 3.6 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c .077 .076 .87 23 .84 0   3.2  1.8  73 240 7.0 3.7 88 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c .077 .076 .80 23 .99 0   3.8  2.1  49 240 6.4 3.5 88 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c .11  .11  .68 23 .99 0   3.2  1.8  63 240 7.1 3.8 88 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c .073 .072 .88 23 .84 0   4.2  2.4  45 240 7.1 3.8 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c .11  .11  .71 23 .99 0   3.3  1.9  57 230 6.3 3.4 96 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c .081 .082 .90 23 .99 0   3.3  1.9  72 240 6.8 3.7 82 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c .097 .097 .80 23 .84 0   3.2  1.8  75 240 6.9 3.7 81 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c .11  .11  .88 23 .99 0   3.2  1.9  69 240 7.1 3.8 95 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c .078 .078 .73 23 .99 0   3.2  1.8  74 240 7.5 4.0 92 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c .074 .073 .88 23 .99 0   3.3  1.9  71 240 6.7 3.6 78 320
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c .099 .099 .94 23 .84 0   3.8  2.1  51 240 7.6 4.0 150 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c .076 .076 .86 23 .99 0   3.3  1.9  68 240 7.1 3.8 100 330
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c .076 .075 .93 23 .95 0   3.4  1.9  71 240 7.3 3.9 120 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c .11  .11  .69 23 .99 0   4.4  2.5  54 240 7.0 3.7 150 320
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c .076 .076 .82 23 .99 0   3.5  1.9  72 240 7.9 4.2 150 320
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c .082 .081 1.2  23 .99 0   6.9  3.6  130 290 7.8 4.2 120 340
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c .079 .078 .79 23 .84 0   3.0  1.7  72 240 6.6 3.5 80 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c .11  .11  .70 23 .84 0   3.4  1.9  74 240 8.2 4.3 150 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c .076 .076 .87 23 .99 0   2.9  1.7  61 230 6.8 3.6 85 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c .080 .079 .84 23 .84 0   3.3  1.9  62 240 7.4 3.9 160 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c .097 .099 .77 23 .84 0   3.2  1.8  64 250 8.8 4.8 170 330
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c .10  .10  .84 23 .99 0   3.3  1.9  61 250 7.4 4.0 96 310
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c .077 .076 .69 23 .99 0   3.2  1.8  68 250 7.6 4.0 91 330
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c .089 .089 .86 23 .84 0   3.4  1.9  71 250 7.0 3.7 82 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c .076 .077 .88 23 .99 0   3.4  1.9  58 240 7.2 3.9 130 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c .10  .10  .75 23 .99 0   3.4  1.9  66 240 7.3 3.9 120 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c .079 .079 .84 23 .84 0   3.3  1.9  72 240 6.6 3.5 82 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c .11  .11  .68 23 .84 0   3.2  1.8  62 230 6.8 3.6 80 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c .11  .11  .69 23 .99 0   3.2  1.8  70 240 7.7 4.0 150 320
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c .077 .076 .75 23 .99 0   3.3  1.9  72 230 6.8 3.6 86 320
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c .088 .087 .85 23 .99 0   3.3  1.9  63 250 7.0 3.7 78 320
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c .080 .080 .91 23 .98 0   3.2  1.8  65 230 7.6 4.1 89 330
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c .10  .10  .80 23 .84 0   3.4  1.9  72 240 6.9 3.7 81 320
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c .089 .090 .74 23 .99 0   3.4  1.9  70 240 7.3 3.9 87 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c 12     12     160    220 .99 0   4.4  2.4  96 250 7.9 4.3 94 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c .10  .10  .80 23 .99 0   3.5  2.0  75 240 8.4 4.4 120 350
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c .073 .074 .86 23 .84 0   3.4  1.9  72 240 8.1 4.3 91 350
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c .074 .074 1.0  23 .99 0   3.6  2.0  78 240 9.1 4.9 100 360
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c .080 .079 .81 23 .99 0   3.5  2.0  71 240 8.3 4.4 160 330
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c .079 .079 .96 23 .84 0   3.3  1.9  75 240 7.6 4.0 130 330
termination-crafted-lit/cstrncmp_false-no-overflow.c .080 .079 .93 23 .99 0   3.7  2.0  75 250 7.7 4.1 96 330
termination-crafted-lit/gcd1_false-no-overflow.c .074 .075 .83 23 .99 0   3.4  1.9  74 230 12   6.7 130 390
termination-crafted-lit/joey_false-no-overflow.c .098 .098 .76 23 .84 0   .50 .33 13 40 5.8 3.1 94 300
termination-crafted-lit/min_rf_false-no-overflow.c .078 .077 1.1  23 .99 0   3.3  1.8  72 240 8.0 4.3 78 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900     900     8900    240 .99 0   .51 .32 10   39 6.3 3.3 130 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 180     180     2500    15000 .99 0   .52 .34 11   40 5.8 3.1 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 180     180     2400    15000 .84 0   .48 .31 11   39 6.2 3.3 140 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 180     180     2300    15000 .99 0   .50 .32 12   40 6.1 3.2 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900     900     7400    2400 .99 0   .53 .35 11   39 5.8 3.1 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900     900     11000    240 .99 0   .48 .32 9.5 40 5.9 3.1 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 900     900     13000    580 .99 0   .53 .34 11   40 6.4 3.3 140 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 900     900     9400    7000 .84 0   .53 .34 13   40 6.8 3.6 120 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 900     900     8900    3100 .99 0   .51 .32 11   39 5.9 3.2 120 290
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 150     150     2100    15000 .99 0   .50 .33 11   40 6.8 3.6 130 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 820     810     9700    15000 .99 0   .52 .36 10   40 6.3 3.3 110 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 900     900     11000    6100 .99 0   .55 .36 12   40 6.0 3.2 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 900     900     14000    720 .99 0   .50 .33 11   40 6.3 3.3 130 310
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900     900     7900    5300 .99 0   .51 .34 8.9 43 6.3 3.3 120 300
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 900     900     10000    270 .99 0   .51 .35 11   40 5.8 3.1 110 300
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 900     900     11000    290 .84 0   .47 .30 7.4 39 5.8 3.1 110 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 900     900     13000    6300 .99 0   .51 .33 11   39 5.8 3.1 110 290
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900     900     11000    5900 .99 0   .55 .36 11   41 5.5 3.0 120 290
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 180     170     2200    15000 .99 0   .49 .32 11   39 6.9 3.6 130 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 180     180     1800    15000 .99 0   .56 .37 12   40 6.5 3.4 120 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 190     180     2400    15000 .99 0   .49 .32 11   43 5.9 3.1 110 290
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900     900     11000    230 .84 0   .52 .34 9.3 42 6.6 3.4 130 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 900     900     14000    640 .99 0   .49 .32 11   39 6.0 3.2 120 300
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 130     130     1600    15000 .99 0   .50 .33 12   40 6.1 3.2 120 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 900     900     6700    8400 .84 0   .58 .38 13   43 5.3 2.9 110 290
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 480     480     5200    15000 .99 0   .50 .31 11   40 6.3 3.3 130 310
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 180     180     2300    15000 .99 0   .52 .34 10   39 5.5 3.0 100 290
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 220     210     2500    15000 .99 0   .72 .45 10   40 6.4 3.4 120 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 200     200     2300    15000 .99 0   .51 .32 10   40 6.1 3.3 120 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 900     900     14000    1100 .99 0   .52 .33 12   40 6.2 3.2 110 300
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 170     160     2200    15000 .84 0   .50 .32 10   39 5.3 2.9 110 290
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 900     900     11000    3000 .99 0   .55 .36 11   42 5.8 3.1 120 300
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 92     86     1200    15000 .99 0   .51 .32 11   39 6.2 3.2 130 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900     900     13000    890 .99 0   .46 .30 7.8 39 6.1 3.2 130 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 900     900     12000    9100 .84 0   .51 .32 11   39 6.4 3.4 130 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 900     900     13000    8000 .99 0   .51 .32 11   40 6.0 3.2 120 300
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 900     900     9600    6700 .84 0   .55 .34 12   43 5.9 3.1 120 290
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 900     900     11000    14000 .99 0   .54 .35 10   41 6.4 3.4 140 310
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 900     900     13000    130 .99 0   .50 .33 11   40 5.6 3.0 110 300
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 790     780     9600    15000 .84 0   .50 .31 9.6 40 6.1 3.2 120 300
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 430     430     5200    15000 .99 0   .59 .40 9.0 41 6.3 3.3 120 300
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c .10  .10  .68 23 .99 0   .54 .35 13   41 6.3 3.3 120 300
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900     900     11000    91 .84 0   .53 .35 13   40 6.3 3.3 130 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 380     370     3700    15000 .99 0   .53 .33 9.5 41 5.9 3.2 120 300
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 390     390     3300    15000 .84 0   .51 .32 11   40 5.9 3.1 120 300
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 900     900     12000    3300 .99 0   .56 .35 12   42 6.2 3.3 130 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 290     280     4100    15000 .84 0   .51 .33 10   40 6.6 3.4 130 300
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 140     140     1700    15000 .99 0   .49 .31 10   39 5.8 3.0 110 300
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 900     900     13000    9600 .84 0   .48 .32 11   40 5.6 3.0 120 290
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 900     900     13000    5000 .84 0   .49 .33 3.5 39 5.8 3.1 120 300
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 190     180     2200    15000 .99 0   .53 .34 12   43 6.0 3.1 130 290
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 870     870     12000    15000 .99 0   .52 .35 12   40 6.9 3.7 140 310
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 46     43     630    15000 .99 0   .52 .36 13   41 5.6 3.0 110 290
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 260     250     3300    15000 .99 0   .54 .36 13   42 6.0 3.2 120 310
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 190     190     2300    15000 .99 0   .54 .34 13   40 5.3 2.9 100 290
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 900     900     11000    8200 .99 0   .52 .34 10   39 5.9 3.1 120 300
termination-crafted-lit/aviad_true-termination_true-no-overflow.c .070 .072 .84 23 .84 0   .49 .32 8.3 40 5.7 3.1 120 290
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 900     880     11000    14000 .99 0   .56 .36 13   40 6.0 3.2 120 300
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 900     900     11000    1300 .99 0   .55 .36 10   42 6.3 3.4 130 300
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 900     880     8800    2200 .84 0   .49 .31 11   39 5.6 3.0 110 300
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 900     900     12000    1300 .84 0   .53 .35 13   40 5.9 3.1 120 300
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 900     900     12000    1300 .99 0   .51 .32 11   41 5.5 3.0 120 290
termination-crafted-lit/genady_true-termination_true-no-overflow.c 78     75     940    15000 .99 0   .54 .36 13   39 6.1 3.2 130 300
termination-crafted-lit/strchr_true-no-overflow.c 900     880     8600    3400 .99 0   .50 .33 10   40 6.1 3.2 120 300
termination-numeric/Addition01_false-no-overflow.c .11  .11  .72 23 .84 0   3.3  1.8  77 250 7.4 3.9 83 320
termination-numeric/Avg_true_false-no-overflow.c .090 .089 1.1  23 .99 0   3.4  1.9  74 250 7.3 3.9 94 320
termination-numeric/Binomial_true-termination_false-no-overflow.c 11     11     160    200 .99 0   3.5  1.9  69 240 7.4 3.9 87 310
termination-numeric/Et1_true_false-no-overflow.c .077 .077 .93 23 .99 0   3.7  2.1  73 250 8.1 4.4 120 350
termination-numeric/Et2_true_false-no-overflow.c .092 .092 1.0  23 .99 0   3.6  2.0  79 250 7.8 4.1 85 330
termination-numeric/Et3_true_false-no-overflow.c .074 .073 1.1  23 .99 0   3.7  2.0  77 250 6.8 3.6 82 320
termination-numeric/Et4_true_false-no-overflow.c .11  .11  .77 23 .99 0   3.7  2.1  78 250 7.9 4.2 170 320
termination-numeric/MultCommutative_false-no-overflow.c .14  .14  1.1  23 .99 0   3.4  1.9  71 250 40   23   490 840
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 3.3   3.3   29    200 .99 0   3.7  2.1  75 250 97   79   1100 3900
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 900     900     6600    5600 .99 0   .50 .32 11   39 5.8 3.1 120 300
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900     900     11000    8500 .99 0   .49 .31 11   40 6.3 3.4 140 300
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 900     900     9900    9700 .99 0   .53 .33 9.7 43 6.0 3.2 120 300
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 570     560     7100    15000 .99 0   .51 .33 11   40 6.0 3.2 130 300
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900     900     7800    11000 .99 0   .54 .34 12   43 5.8 3.1 110 300
termination-numeric/Parts_true-termination_true-no-overflow.c 900     890     11000    12000 .99 0   .54 .36 11   39 5.7 3.0 100 300
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900     900     4600    6900 .99 0   .52 .32 12   39 5.7 3.1 110 300
termination-numeric/gcd01_true-termination_true-no-overflow.c 900     900     12000    960 .99 0   .52 .33 11   40 6.3 3.4 130 310
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 180     170     2400    15000 .99 0   .51 .34 11   40 6.1 3.2 120 300
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 900     900     10000    3400 .99 0   .55 .36 12   43 6.1 3.2 120 300
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900     900     12000    7800 .99 0   .54 .36 13   40 5.8 3.1 120 300
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900     900     10000    7600 .99 0   .71 .45 10   40 6.5 3.4 120 300
termination-numeric/twisted_true-termination_true-no-overflow.c .10  .10  .76 23 .99 0   .52 .34 12   39 5.9 3.2 120 290
recursive/Addition02WithOverflowBug_false-no-overflow.c .11  .11  .73 23 .84 0   3.3  1.8  71 250 7.6 4.0 83 330
recursive/Addition03_false-no-overflow.c .080 .080 .83 23 .84 0   3.5  1.9  78 260 7.7 4.1 110 330
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c .085 .085 .87 23 .99 0   .54 .33 12 39 9.2 4.8 70 310
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 900     900     8100    5600 .84 0   .55 .35 11   42 6.0 3.2 120 300
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 900     900     7000    5700 .99 0   .67 .43 12   40 5.8 3.1 110 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 900     900     6900    5700 .84 0   .51 .33 11   41 6.4 3.4 140 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 900     900     7100    5700 .99 0   .59 .38 12   42 6.9 3.6 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 570     570     3500    15000 .99 0   .54 .34 13   43 5.8 3.1 120 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 560     560     4000    15000 .84 0   .52 .32 10   40 5.7 3.0 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 570     570     4100    15000 .99 0   .51 .32 11   41 5.8 3.1 130 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 900     890     9100    920 .99 0   .49 .33 11   39 5.9 3.1 110 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c .11  .11  .65 23 .99 0   .47 .31 9.7 40 5.5 2.9 64 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c .11  .11  .64 23 .99 0   .52 .33 11   41 5.7 3.0 120 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 900     900     10000    9700 .84 0   .48 .30 11   39 5.8 3.1 130 290
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 300     290     4500    15000 .99 0   .61 .39 7.8 40 6.3 3.3 68 310
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 900     900     9600    3900 .99 0   .50 .34 11   41 6.3 3.3 120 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 900     900     9200    9700 .84 0   .50 .32 11   40 5.9 3.2 110 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 900     900     9700    9700 .84 0   .51 .32 11   40 5.8 3.1 110 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 900     900     10000    9900 .99 0   .51 .34 11   42 6.1 3.3 120 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 900     900     8800    10000 .84 0   .59 .38 12   42 5.8 3.1 110 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 900     900     7600    11000 .99 0   .52 .33 12   40 6.1 3.2 120 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 250     250     1700    15000 .99 0   .52 .33 13   42 6.0 3.2 120 290
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 900     900     10000    960 .99 0   .50 .34 10   39 6.0 3.2 130 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 900     900     10000    500 .99 0   .50 .33 11   40 6.1 3.2 130 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 610     610     4800    15000 .99 0   .52 .34 11   41 5.5 2.9 110 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 900     900     9400    3300 .99 0   .52 .35 13   39 6.2 3.3 120 290
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 900     900     13000    3300 .99 0   .48 .31 11   40 5.2 2.8 110 280
bitvector/jain_1_false-no-overflow.i .074 .076 .75 23 .99 0   3.1  1.8  64 240 7.2 3.8 93 320
bitvector/jain_2_false-no-overflow.i .11  .11  .84 23 .99 0   3.0  1.7  64 240 7.8 4.2 170 320
bitvector/jain_4_false-no-overflow.i .080 .081 .86 23 .99 0   3.2  1.8  70 240 7.2 3.9 130 320
bitvector/jain_5_false-no-overflow.i 110     110     1500    15000 .84 0   .48 .32 12 40 5.9 3.1 74 310
bitvector/jain_6_false-no-overflow.i .11  .11  .98 23 .84 0   3.1  1.8  76 240 7.3 3.9 110 320
bitvector/jain_7_false-no-overflow.i .10  .10  .86 23 .99 0   3.0  1.7  62 240 7.2 3.8 130 310
bitvector/modulus_false-no-overflow.i .10  .10  .82 23 .84 0   3.2  1.8  74 240 7.3 3.9 110 320
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 450     440     5000    15000 .99 0   .49 .33 13   40 6.0 3.2 130 300
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 380     380     5100    15000 .99 0   .51 .32 9.5 39 5.8 3.1 110 300
bitvector/byte_add_false-unreach-call_true-no-overflow.i 450     440     5300    15000 .84 0   .48 .32 11   40 6.1 3.2 130 300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i .089 .089 .83 23 .99 0   .52 .31 9.2 40 5.8 3.1 120 290
bitvector/gcd_2_true-unreach-call_true-no-overflow.i .086 .086 .67 23 .99 0   .50 .32 11   39 5.9 3.1 130 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i .071 .071 1.0  23 .99 0   .49 .32 11   39 6.1 3.2 110 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i .083 .082 .70 23 .99 0   .47 .31 7.8 40 6.6 3.5 120 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 900     870     14000    2600 .99 0   .51 .34 12   39 6.0 3.1 120 300
bitvector/jain_1_true-unreach-call_true-no-overflow.i 900     890     9900    790 .84 0   .51 .33 11   41 5.8 3.1 120 290
bitvector/jain_2_true-unreach-call_true-no-overflow.i 900     890     11000    780 .99 0   .54 .35 12   40 5.9 3.2 120 290
bitvector/jain_4_true-unreach-call_true-no-overflow.i 900     890     11000    780 .99 0   .51 .33 11   42 6.5 3.4 120 300
bitvector/jain_5_true-unreach-call_true-no-overflow.i 900     850     13000    12000 .99 0   .54 .36 13   43 6.2 3.3 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i 900     890     9500    760 .99 0   .51 .33 11   42 6.5 3.4 120 310
bitvector/jain_7_true-unreach-call_true-no-overflow.i 900     890     10000    760 .84 0   .55 .37 12   41 6.0 3.2 110 290
bitvector/modulus_true-unreach-call_true-no-overflow.i 900     900     12000    4800 .99 0   .51 .33 11   40 6.0 3.2 130 310
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 140     130     1800    15000 .99 0   .54 .36 13   40 6.4 3.4 120 300
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 140     130     1800    15000 .97 0   .53 .35 11   40 6.6 3.5 120 320
bitvector/parity_true-unreach-call_true-no-overflow.i 900     880     6900    700 .84 0   .60 .39 8.0 40 5.9 3.2 110 300
bitvector/sum02_false-unreach-call_true-no-overflow.i 900     880     9000    770 .99 0   .57 .38 13   41 5.8 3.1 120 300
bitvector/sum02_true-unreach-call_true-no-overflow.i 900     880     9100    750 .99 0   .55 .36 9.4 44 5.6 3.0 110 290
../../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 110000 110000 1200000 1400000 310 0   328 730 470 13000 45000 328 1300 740 19000 57000 328 86 56 1800 6600   328 980 520 19000 49000  
    correct results 149 25 25 280 3700 140 0   137 510 290 10000 36000 149 1100 580 16000 48000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 149 25 25 280 3700 140 0   118 510 290 10000 36000 137 1100 580 16000 48000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 11 27 27 360 820 11 0   6 220 180 3000 9100 10 220 150 2600 7900 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 11 27 27 360 820 11 0   0 220 180 3000 9100 0 220 150 2600 7900 0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (328 tasks, max score: 491) 149
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]