Tool SMACK+Corral 1.7.2
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-14 07:19:02 CET [[ 2017-01-15 04:32:52 CET ]] [[ 2017-01-15 05:00:11 CET ]] [[ 2017-01-15 04:38:10 CET ]] [[ 2017-01-15 05:08:13 CET ]]
Run set sv-comp17.Overflows-BitVectors
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness 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 1 1.5  1.5  20   73 .86 0      4.1  2.3  88   250 7.0 3.7 100 320
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 1 1.5  1.5  19   77 .89 0      4.1  2.3  92   250 7.3 3.9 150 320
signedintegeroverflow-regression/Division_false-no-overflow.c.i 1 1.6  1.6  20   80 .88 0      4.0  2.2  77   250 7.4 3.9 120 310
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 1 1.5  1.5  18   74 .86 0      4.0  2.2  82   250 7.1 3.8 120 330
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 1 1.5  1.5  17   77 .86 0      3.9  2.2  64   240 8.5 4.4 140 330
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 1 1.5  1.5  20   80 .88 0      3.9  2.2  70   240 7.2 3.9 110 320
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 1 1.5  1.5  19   75 .86 0      3.9  2.2  77   240 7.0 3.7 120 310
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 1 1.5  1.5  17   70 .88 0      3.9  2.2  80   240 6.7 3.7 140 300
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 1 1.5  1.5  18   71 .86 0      4.0  2.2  86   240 6.8 3.7 130 310
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 1 1.5  1.5  19   70 .88 0      4.0  2.2  86   240 6.8 3.7 110 300
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i 2 1.2  1.2  14   68 .85 0      4.1  2.2  80   260 6.5 3.5 110 310
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i 2 1.2  1.2  15   67 .88 0      4.2  2.3  74   270 7.5 4.0 130 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i 2 1.2  1.2  13   68 .86 0      4.2  2.3  92   260 6.7 3.5 77 300
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i 2 1.2  1.2  15   69 .86 0      4.2  2.3  96   260 7.2 3.8 73 320
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i 2 1.2  1.2  14   69 .87 0      4.3  2.4  84   280 6.6 3.5 74 310
termination-crafted/2Nested_false-no-overflow.c 1 1.7  1.8  19   85 .87 0      3.2  1.8  74   240 7.1 3.8 120 320
termination-crafted/4NestedWith3Variables_false-no-overflow.c 1 1.9  1.9  22   84 .91 0      3.3  1.9  68   240 9.2 4.9 100 320
termination-crafted/Ackermann_false-no-overflow.c 1 1.6  1.6  20   80 .89 0      3.3  1.8  68   240 7.3 3.9 120 320
termination-crafted/Bangalore_false-no-overflow.c 0 880    930    10000   1300 .86 0      .49 .32 5.9 40 5.7 3.0 98 300
termination-crafted/Bangalore_v3_false-no-overflow.c 1 1.7  1.8  22   76 .86 0      3.2  1.8  60   240 7.2 3.9 120 320
termination-crafted/Benghazi_nondet_false-no-overflow.c 1 1.8  1.8  20   86 .88 0      3.0  1.7  65   230 7.3 3.9 140 320
termination-crafted/Binary_Search_false-no-overflow.c 1 1.6  1.6  19   78 .88 0      3.1  1.8  64   240 7.3 3.9 120 320
termination-crafted/Cairo_nondet_false-no-overflow.c 1 1.7  1.6  24   75 .86 0      3.2  1.8  71   240 7.7 4.1 150 320
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 1 1.7  1.8  20   82 .88 0      3.1  1.8  57   240 6.9 3.7 110 310
termination-crafted/Copenhagen_disj_false-no-overflow.c 1 1.7  1.8  22   83 .87 0      3.3  1.9  66   240 7.4 4.0 110 330
termination-crafted/Gothenburg_false-no-overflow.c 1 1.8  1.8  21   88 .90 0      3.3  1.9  68   240 7.7 4.1 150 320
termination-crafted/Gothenburg_v2_false-no-overflow.c 1 1.8  1.8  20   78 .91 0      3.4  1.9  78   240 7.7 4.1 150 310
termination-crafted/Hanoi_2vars_false-no-overflow.c 1 1.7  1.8  23   82 .86 0      3.3  1.8  77   240 7.5 4.0 130 320
termination-crafted/Hanoi_3vars_false-no-overflow.c 1 1.8  1.8  19   80 .88 0      3.0  1.7  66   230 7.3 3.8 120 320
termination-crafted/Hanoi_plus_false-no-overflow.c 1 1.8  1.8  23   88 .88 0      3.3  1.9  74   240 6.6 3.5 120 310
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 1 1.7  1.7  22   73 .86 0      3.2  1.8  72   240 7.3 3.9 130 320
termination-crafted/Mysore_false-no-overflow.c 1 1.7  1.8  21   81 .88 0      3.4  1.9  75   240 7.0 3.8 120 320
termination-crafted/NestedRecursion_1a_false-no-overflow.c 1 1.6  1.6  19   72 .89 0      3.3  1.9  70   240 7.6 4.0 150 320
termination-crafted/NestedRecursion_2a_false-no-overflow.c 1 1.5  1.5  22   71 .86 0      3.1  1.7  49   250 6.9 3.7 120 320
termination-crafted/NonTermination1_false-no-overflow.c 1 2.9  2.9  31   79 .86 0      3.2  1.8  74   240 8.3 4.4 110 310
termination-crafted/NonTermination2_false-no-overflow.c 1 1.6  1.6  20   76 .86 0      3.4  1.9  70   240 7.2 3.8 100 320
termination-crafted/NonTermination4_false-no-overflow.c 1 110    110    830   400 .86 0      3.6  2.0  80   250 8.9 4.8 170 350
termination-crafted/NonTerminationSimple2_false-no-overflow.c 0 880    930    9600   1900 .86 0      .49 .32 6.7 41 5.8 3.1 110 300
termination-crafted/NonTerminationSimple3_false-no-overflow.c 1 1.7  1.6  23   73 .86 0      3.1  1.8  70   240 6.9 3.7 150 320
termination-crafted/NonTerminationSimple4_false-no-overflow.c 0 880    930    9700   810 .86 0      .53 .34 12   41 5.9 3.1 98 300
termination-crafted/NonTerminationSimple5_false-no-overflow.c 1 1.7  1.8  20   81 .88 0      3.2  1.8  64   230 7.1 3.7 110 320
termination-crafted/NonTerminationSimple6_false-no-overflow.c 0 880    930    9800   1800 .86 0      .53 .35 4.7 43 5.7 3.0 110 290
termination-crafted/NonTerminationSimple8_false-no-overflow.c 1 1.8  1.8  23   83 .90 0      3.3  1.9  65   230 7.2 3.9 120 320
termination-crafted/NonTerminationSimple9_false-no-overflow.c 1 1.7  1.6  21   76 .86 0      3.2  1.8  65   240 6.8 3.6 110 320
termination-crafted/Pure2Phase_false-no-overflow.c 1 1.8  1.8  22   83 .88 0      3.3  1.8  75   240 7.4 4.0 120 320
termination-crafted/Pure3Phase_false-no-overflow.c 1 1.8  1.8  22   80 .89 0      3.0  1.7  65   230 7.7 4.1 160 320
termination-crafted/RecursiveMultiplication_false-no-overflow.c 1 1.6  1.6  19   84 .89 0      3.2  1.8  73   250 7.5 4.0 120 320
termination-crafted/RecursiveNonterminating_false-no-overflow.c 1 1.5  1.5  19   75 .89 0      3.1  1.8  71   240 7.5 4.0 150 310
termination-crafted/Rotation180_false-no-overflow.c 1 1.7  1.6  22   74 .86 0      3.3  1.9  74   240 6.7 3.6 120 300
termination-crafted/Singapore_false-no-overflow.c 1 1.7  1.8  22   81 .89 0      3.2  1.8  71   240 7.3 3.9 130 320
termination-crafted/Singapore_plus_false-no-overflow.c 1 13    13    140   110 .89 0      3.2  1.8  67   230 6.8 3.6 110 310
termination-crafted/Singapore_v1_false-no-overflow.c 0 880    930    12000   450 .89 0      .50 .33 11   41 7.0 3.7 86 300
termination-crafted/Singapore_v2_false-no-overflow.c 1 14    13    170   110 .89 0      3.1  1.8  63   240 6.9 3.7 110 310
termination-crafted/Stockholm_false-no-overflow.c 1 1.7  1.8  25   84 .88 0      3.3  1.9  61   230 7.2 3.8 110 310
termination-crafted/Thun_false-no-overflow.c 1 1.8  1.8  21   80 .88 0      3.1  1.8  61   230 7.2 3.8 77 310
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 1 1.7  1.8  22   84 .88 0      3.3  1.9  70   230 9.0 4.8 170 330
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 1 1.9  1.9  28   88 1.0  0      3.5  2.0  74   240 7.8 4.1 120 320
termination-crafted/aaron2_false-no-overflow.c 1 1.8  1.8  22   81 .89 0      3.6  2.0  55   240 7.2 3.9 120 310
termination-crafted/aaron3_false-no-overflow.c 1 1.8  1.8  21   82 .88 0      3.3  1.9  64   240 7.6 4.0 150 320
termination-crafted/4BitCounterPointer_true-no-overflow.c 2 1.3  1.3  16   75 .86 0      4.6  2.6  100   280 7.0 3.7 93 310
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c 0 880    930    7900   1100 .90 0      .57 .36 10   43 6.0 3.2 96 300
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c 2 880    880    9500   660 .88 0      3.7  2.1  78   290 7.5 4.0 120 320
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c 0 880    930    7700   1200 .89 0      .54 .35 9.4 40 6.0 3.2 110 300
termination-crafted/Bangalore_true-no-overflow.c 2 880    880    11000   870 .86 0      4.0  2.2  84   280 8.3 4.5 140 330
termination-crafted/Bangalore_v2_true-no-overflow.c 2 880    880    10000   510 .86 0      3.9  2.2  83   270 8.6 4.7 120 330
termination-crafted/Bangalore_v4_true-no-overflow.c 2 1.4  1.3  16   77 .86 0      3.6  2.1  87   280 8.7 4.6 140 350
termination-crafted/Benghazi_true-no-overflow.c 2 880    880    9100   920 .88 0      4.1  2.3  79   280 96   60   1100 1600
termination-crafted/Cairo_step2_true-no-overflow.c 2 880    880    11000   620 .86 0      4.7  2.6  58   280 960   810   13000 4500
termination-crafted/Cairo_true-no-overflow.c 2 880    880    11000   820 .86 0      3.8  2.2  75   280 7.8 4.2 140 330
termination-crafted/Copenhagen_true-no-overflow.c 2 880    880    10000   690 .86 0      4.0  2.3  41   280 8.3 4.5 130 330
termination-crafted/Division_true-no-overflow.c 2 880    880    10000   2800 .87 0      4.2  2.4  72   280 7.4 4.0 110 320
termination-crafted/LexIndexValue-Array_true-no-overflow.c 0 880    930    8500   980 .89 0      .47 .31 4.4 39 5.5 2.9 67 300
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 0 880    930    11000   1300 .88 0      .54 .34 12   41 5.2 2.8 54 290
termination-crafted/Madrid_true-no-overflow.c 2 1.3  1.3  16   76 .84 0      3.8  2.1  77   280 7.3 3.9 130 320
termination-crafted/McCarthy91_Iteration_true-no-overflow.c 2 880    880    9500   350 .88 0      3.9  2.2  78   280 960   850   14000 4600
termination-crafted/McCarthy91_Recursion_true-no-overflow.c 2 880    880    8800   210 .86 0      3.5  2.0  73   260 9.1 5.0 120 330
termination-crafted/MenloPark_true-no-overflow.c 2 880    880    9400   890 .88 0      3.6  2.1  64   270 17   9.5 200 490
termination-crafted/MutualRecursion_1a_true-no-overflow.c 2 880    880    8700   250 .89 0      3.6  2.0  78   250 12   6.7 140 390
termination-crafted/MutualRecursion_1b_true-no-overflow.c 0 880    930    9000   220 .89 0      .49 .33 5.4 40 6.1 3.2 99 300
termination-crafted/NestedRecursion_1b_true-no-overflow.c 2 880    880    7400   510 .89 0      3.7  2.1  71   250 17   9.3 180 550
termination-crafted/NestedRecursion_1c_true-no-overflow.c 2 880    880    8000   520 .89 0      3.5  2.0  76   240 13   7.2 160 420
termination-crafted/NestedRecursion_1d_true-no-overflow.c 2 880    880    7300   340 .89 0      3.9  2.2  77   270 17   9.1 210 540
termination-crafted/NestedRecursion_2b_true-no-overflow.c 1 880    880    8000   280 .88 0      3.5  1.9  64   250 960   800   10000 3800
termination-crafted/NestedRecursion_2c_true-no-overflow.c 1 880    880    6300   530 .88 0      3.3  1.9  73   240 960   800   17000 3900
termination-crafted/NonTermination3_true-no-overflow.c 2 1.3  1.3  18   75 .86 0      4.3  2.4  86   280 6.4 3.5 75 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c 0 880    930    9700   4400 .86 0      .54 .35 13   43 5.6 3.0 53 300
termination-crafted/Nyala-2lex_true-no-overflow.c 2 880    880    11000   360 .88 0      4.3  2.4  87   280 7.2 3.9 62 320
termination-crafted/Parallel_true-no-overflow.c 2 880    880    9400   630 .88 0      4.4  2.4  84   270 8.3 4.4 110 330
termination-crafted/Piecewise_true-no-overflow.c 2 880    880    10000   380 .88 0      4.7  2.6  89   280 7.9 4.2 140 330
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c 2 880    880    11000   1000 .86 0      3.8  2.1  61   270 8.0 4.3 120 320
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c 2 880    880    11000   420 .89 0      4.9  2.7  97   280 8.4 4.5 100 320
termination-crafted/Waldkirch_true-no-overflow.c 2 880    880    9700   850 .86 0      3.8  2.1  79   270 7.3 3.9 140 320
termination-crafted/WhileFalse_true-no-overflow.c 2 1.2  1.2  13   68 .84 0      3.5  2.0  84   270 7.1 3.8 120 320
termination-crafted/WhileTrue_true-no-overflow.c 2 1.3  1.3  15   76 .84 0      3.4  1.9  74   270 6.9 3.7 78 310
termination-crafted/easy1_true-no-overflow.c 2 22    22    330   150 .86 0      4.3  2.4  79   300 7.5 4.0 150 320
termination-crafted/easy2_true-no-overflow.c 2 880    880    11000   800 .88 0      4.1  2.3  63   270 960   820   12000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 1 1.8  1.8  21   80 .90 0      3.2  1.9  66   240 7.4 4.0 110 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 1 2.0  1.9  23   88 .95 0      3.3  1.8  65   240 7.4 3.9 140 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 1 1.8  1.8  22   79 .89 0      3.2  1.8  62   240 7.8 4.2 150 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 1 1.8  1.8  22   80 .89 0      3.3  1.9  70   240 7.5 4.0 140 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 1 1.9  1.9  25   81 .91 0      3.4  1.9  74   240 7.7 4.1 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 1 1.8  1.8  23   84 .90 0      3.5  1.9  71   240 7.6 4.0 78 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 0 1.8  1.8  22   76 .89 0      93    81    1200   3700 6.5 3.5 75 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 1 1.8  1.8  19   86 .88 0      3.4  1.9  72   240 7.8 4.1 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c 0 88    88    1000   120 .89 0      .49 .31 6.8 39 5.7 3.1 100 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 1 1.7  1.6  21   73 .87 0      3.2  1.8  64   240 7.1 3.8 110 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 1 1.7  1.8  19   81 .89 0      3.5  2.0  51   240 7.9 4.2 150 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 1 1.8  1.8  22   85 .89 0      3.4  1.9  66   240 7.7 4.1 110 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 1 1.7  1.7  25   84 .88 0      3.5  2.0  69   240 7.6 4.1 150 320
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 1 1.8  1.8  23   86 .89 0      3.2  1.8  63   240 7.3 4.0 130 310
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 1 1.8  1.8  26   89 .91 0      3.3  1.9  67   240 8.2 4.4 110 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 1 2.4  2.4  27   94 .90 0      3.2  1.8  65   240 7.3 3.9 110 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 1 1.8  1.8  21   91 .92 0      3.5  2.0  72   230 7.3 3.9 120 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 1 1.8  1.8  24   87 .89 0      3.4  2.0  53   240 7.7 4.1 140 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 1 1.8  1.8  24   83 .89 0      3.3  1.9  77   240 7.2 3.9 120 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 1 1.9  1.9  24   88 .94 .0082 3.6  2.0  74   240 7.0 3.8 120 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 1 1.8  1.8  23   84 .91 0      3.5  1.9  73   240 7.1 3.9 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 1 1.7  1.8  20   79 .88 0      3.1  1.8  63   240 7.0 3.8 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 1 1.7  1.7  25   79 .88 0      3.2  1.8  64   240 7.9 4.2 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 1 1.7  1.8  23   83 .88 0      3.2  1.8  71   230 7.4 4.0 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 1 1.7  1.6  19   73 .86 0      3.2  1.8  63   240 7.2 3.8 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 1 1.7  1.6  23   78 .86 0      3.3  1.9  64   240 7.0 3.7 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 1 1.7  1.8  22   81 .88 0      3.3  1.8  74   240 6.8 3.6 96 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 1 1.7  1.8  19   80 .88 0      3.2  1.8  68   230 7.9 4.2 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 1 1.8  1.9  22   83 .88 0      3.3  1.9  71   240 7.2 3.9 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 1 1.7  1.8  22   86 .88 0      3.2  1.8  66   230 6.7 3.6 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 1 1.7  1.8  22   81 .86 0      3.3  1.8  68   250 6.8 3.7 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 1 1.8  1.8  22   83 .91 0      3.4  1.9  80   230 7.9 4.2 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 1 1.7  1.8  22   75 .88 0      3.0  1.7  61   240 7.4 3.9 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 1 1.7  1.8  23   82 .88 0      3.1  1.8  53   240 7.0 3.7 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 1 1.8  1.8  19   80 .89 0      3.3  1.8  66   240 8.3 4.5 130 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 1 1.7  1.8  21   76 .88 0      3.3  1.8  74   230 8.8 4.6 140 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 1 1.8  1.8  21   82 .91 0      3.3  1.9  59   240 7.7 4.1 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 1 1.7  1.8  20   81 .88 0      3.2  1.9  72   230 7.1 3.8 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 1 1.7  1.8  22   78 .88 0      3.2  1.8  70   230 7.3 3.9 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 1 1.9  1.9  23   76 .88 0      3.4  1.9  76   230 6.5 3.5 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 1 1.7  1.6  20   88 .86 0      3.2  1.8  64   240 6.8 3.6 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 1 1.7  1.6  19   75 .86 .0082 3.2  1.8  74   230 7.2 3.8 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 1 1.7  1.8  22   80 .88 0      3.1  1.8  65   230 6.7 3.6 100 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 1 1.7  1.8  20   83 .89 0      3.2  1.8  71   240 7.1 3.8 100 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 1 1.7  1.8  23   84 .89 0      3.1  1.8  59   240 6.4 3.5 120 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 1 1.7  1.8  22   82 .88 0      3.0  1.7  59   230 6.4 3.5 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 1 1.7  1.6  22   82 .86 0      3.3  1.9  65   240 7.1 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 1 1.7  1.8  23   83 .88 0      3.1  1.8  67   240 7.2 3.8 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 1 1.7  1.8  25   82 .88 0      3.1  1.8  66   240 7.5 4.0 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 1 1.8  1.8  22   78 .89 0      3.4  2.0  68   240 8.2 4.4 160 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 1 1.7  1.8  23   80 .88 0      3.4  1.9  66   230 7.4 3.9 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 1 1.8  1.8  22   83 .89 0      3.3  1.9  66   240 7.1 3.8 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 1 1.7  1.8  22   80 .88 0      3.1  1.7  70   240 7.0 3.7 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 1 1.8  1.8  26   81 .89 0      3.3  1.9  66   230 7.5 3.9 130 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 1 1.7  1.7  22   80 .86 0      3.5  2.0  80   240 7.1 3.7 120 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 1 1.8  1.8  24   80 .89 0      3.3  1.9  67   230 8.6 4.5 130 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 1 1.8  1.8  20   89 .89 0      3.2  1.8  67   240 7.6 4.0 120 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 1 1.8  1.8  22   86 .88 0      3.0  1.7  61   240 7.9 4.2 140 330
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 1 1.7  1.8  22   79 .88 0      3.2  1.8  70   230 8.1 4.3 130 330
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 1 1.8  1.8  19   87 .88 0      3.2  1.8  71   240 6.8 3.7 130 310
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 1 1.8  1.8  23   89 .89 0      3.3  1.8  72   240 6.9 3.7 110 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 1 1.7  1.8  23   78 .88 0      3.3  1.8  72   240 6.9 3.7 110 320
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 1 1.7  1.8  23   83 .88 0      93    79    1400   3700 9.1 4.8 100 310
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 1 1.8  1.8  21   77 .93 0      7.1  3.8  130   290 6.9 3.7 100 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 1 1.8  1.8  21   79 .89 0      3.1  1.8  67   240 7.5 4.0 140 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 1 1.7  1.8  22   78 .89 0      3.4  1.9  67   250 7.9 4.2 150 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 1 1.7  1.8  22   81 .89 0      3.0  1.7  60   240 7.7 4.1 150 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 1 1.8  1.8  21   79 .89 0      3.2  1.8  50   240 7.4 3.9 120 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 1 1.6  1.6  22   79 .88 0      3.4  1.9  67   250 8.8 4.8 160 350
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 1 1.6  1.6  18   80 .88 0      3.1  1.7  62   250 7.1 3.9 120 310
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 1 1.6  1.6  21   91 .89 0      3.2  1.8  64   250 7.2 3.8 110 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 1 1.6  1.6  21   78 .89 0      3.2  1.8  66   250 7.9 4.1 110 330
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 1 1.7  1.8  21   86 .88 0      3.2  1.8  69   230 6.8 3.7 100 310
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 1 1.7  1.8  21   81 .88 0      3.4  1.9  72   240 7.7 4.1 120 330
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 1 1.7  1.8  21   80 .88 0      3.1  1.8  53   230 7.0 3.7 150 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 1 1.7  1.6  20   82 .86 0      3.2  1.8  61   230 7.2 3.8 140 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 1 1.7  1.8  19   80 .87 0      3.3  1.8  65   240 7.0 3.8 140 310
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 1 1.7  1.8  20   79 .88 0      3.3  1.9  65   240 6.9 3.7 130 320
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 1 1.8  1.8  23   78 .89 0      3.4  2.0  53   240 7.0 3.8 140 310
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 1 1.9  1.9  20   82 .90 0      3.4  1.9  72   250 7.2 3.8 110 320
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 1 1.7  1.8  23   82 .88 0      3.3  1.9  77   240 6.9 3.7 140 310
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 1 1.8  1.8  24   87 .89 0      3.3  1.9  74   240 6.9 3.7 110 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c -32 880    880    11000   230 .88 0      4.0  2.2  81   280 40   24   390 770
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 1 1.7  1.8  19   82 .88 0      3.3  1.9  74   240 6.5 3.5 100 310
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 1 1.8  1.8  21   84 .88 0      3.4  1.9  71   250 7.6 4.0 140 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 1 1.8  1.8  25   84 .88 0      3.4  1.9  69   230 7.8 4.1 140 320
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 1 1.8  1.8  22   85 .91 0      3.3  1.9  72   240 7.4 3.9 150 320
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 1 1.7  1.8  24   86 .88 0      3.1  1.8  74   230 7.7 4.1 130 320
termination-crafted-lit/cstrncmp_false-no-overflow.c 1 1.8  1.8  24   78 .91 0      3.8  2.2  53   250 6.9 3.7 94 310
termination-crafted-lit/gcd1_false-no-overflow.c 1 1.7  1.8  21   79 .89 0      3.7  2.1  64   240 7.2 3.8 140 310
termination-crafted-lit/joey_false-no-overflow.c 1 1.6  1.6  21   75 .88 0      3.4  1.9  51   260 7.3 3.9 100 320
termination-crafted-lit/min_rf_false-no-overflow.c 0 .41 .45 5.1 35 .90 0      .50 .32 12   40 5.8 3.1 66 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 0 880    930    12000   160 .89 0      .50 .32 9.6 39 6.2 3.2 100 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 2 880    880    12000   400 .88 0      4.3  2.4  84   280 7.5 4.1 65 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2 22    22    260   150 .88 0      4.1  2.3  85   280 7.0 3.8 91 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 2 880    880    9500   820 .88 0      3.7  2.1  69   280 960   820   12000 4700
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 1 880    880    8500   420 .91 0      900    880    18000   4800 960   780   12000 3900
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 2 880    880    11000   180 .89 .0041 4.1  2.3  87   280 440   340   8400 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 2 26    26    330   110 .91 0      900    880    14000   4000 46   27   420 2100
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 2 880    880    9900   490 .88 0      4.3  2.4  92   280 8.3 4.5 140 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 2 880    880    10000   490 .88 0      4.3  2.4  82   280 9.1 4.9 130 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 2 880    880    11000   370 .88 0      4.2  2.3  81   280 8.9 4.8 150 330
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 2 880    880    10000   520 .88 0      900    870    12000   4800 7.8 4.1 130 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 2 880    880    9300   990 .88 0      900    860    15000   4900 7.9 4.3 120 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 2 880    880    11000   780 .90 0      4.0  2.2  88   280 11   5.7 170 360
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 1 880    880    10000   540 .90 0      900    840    11000   6100 960   840   10000 4600
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 2 880    880    11000   170 .88 0      4.0  2.2  76   280 13   7.4 250 470
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 2 880    880    10000   180 .88 0      4.0  2.2  84   280 13   7.0 190 460
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 2 880    880    8300   470 .88 0      4.3  2.4  80   280 11   5.6 180 360
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 1 880    880    10000   610 .89 0      900    850    13000   5800 960   820   11000 4600
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 2 880    880    11000   880 .88 0      3.9  2.2  75   300 23   13   320 590
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2 22    22    290   150 .88 0      4.0  2.3  83   280 7.2 3.9 74 320
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 2 880    880    9900   810 .88 0      3.8  2.1  76   280 960   820   13000 4800
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 2 880    880    12000   170 .89 0      4.1  2.3  79   280 450   350   4500 7000
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 2 25    24    360   110 .91 0      900    880    19000   3500 46   27   410 2300
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 2 1.3  1.3  16   82 .87 0      3.9  2.2  72   270 6.2 3.3 110 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 2 880    880    9300   880 .86 0      3.7  2.1  69   270 6.9 3.7 110 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 2 880    880    9700   990 .86 0      4.1  2.3  84   280 7.8 4.2 120 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 2 880    880    12000   460 .88 0      4.4  2.5  98   280 7.5 3.9 70 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 2 880    880    13000   450 .89 0      4.7  2.6  97   280 7.8 4.2 110 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 2 880    880    8200   430 .89 0      5.3  2.9  110   280 7.9 4.3 120 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 2 880    880    9800   670 .88 0      3.8  2.1  73   280 8.7 4.7 110 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 2 880    880    11000   900 .88 0      4.3  2.4  83   280 8.1 4.4 130 330
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 2 880    880    11000   680 .87 0      3.7  2.1  81   270 7.8 4.3 130 330
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 0 880    930    8900   670 .86 0      .50 .33 9.4 40 5.5 2.9 45 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 1 880    880    12000   240 .91 0      900    870    14000   5000 960   850   17000 4700
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 2 880    880    11000   330 .88 0      4.7  2.6  94   280 7.2 3.9 100 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 2 880    880    10000   1000 .88 0      3.9  2.2  78   270 21   12   340 580
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 2 880    880    11000   740 .86 0      3.9  2.2  73   280 7.3 3.9 91 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 2 880    880    13000   1300 .88 0      3.8  2.2  72   280 8.8 4.8 99 330
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 2 880    880    11000   430 .86 0      4.0  2.3  89   270 8.3 4.4 150 340
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 1 880    880    11000   400 .90 0      900    840    12000   6800 960   800   17000 4700
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 2 880    880    10000   430 .88 0      4.3  2.4  90   280 7.3 3.9 130 320
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 2 880    880    11000   320 .88 0      4.2  2.4  61   280 7.4 4.0 87 330
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 2 880    880    9600   250 .91 0      4.1  2.3  90   280 960   820   17000 2700
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 2 880    880    13000   170 .89 0      3.4  1.9  75   250 11   6.3 190 420
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 1 880    880    10000   250 .88 0      3.5  2.0  80   240 960   800   12000 4000
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 2 880    880    9700   280 .89 0      4.2  2.3  87   280 8.4 4.5 120 330
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 2 880    880    9300   710 .88 0      4.6  2.6  100   280 7.3 4.0 95 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2 16    16    190   110 .86 0      3.9  2.2  76   270 7.2 3.8 110 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 2 880    880    9800   850 .86 0      3.8  2.1  88   280 7.2 3.9 140 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 2 880    880    9800   900 .88 0      4.2  2.4  90   270 7.7 4.2 110 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 2 880    880    11000   400 .88 0      4.3  2.4  86   300 7.6 4.0 100 320
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 2 880    880    12000   1000 .86 0      4.1  2.3  89   280 8.2 4.3 96 340
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 2 880    880    9300   980 .88 0      330    320    4700   7000 8.7 4.6 140 320
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 2 880    880    11000   380 .88 0      360    340    7400   7000 8.3 4.4 120 320
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 2 880    880    11000   370 .90 0      5.5  3.0  120   290 8.0 4.3 65 320
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 2 1.4  1.5  17   80 .88 0      4.6  2.6  92   280 7.4 4.0 130 320
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 2 880    880    12000   740 .88 0      4.4  2.5  88   280 960   800   12000 4700
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 2 1.4  1.5  19   85 .90 0      5.8  3.2  100   310 7.9 4.2 92 330
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 2 1.4  1.5  17   82 .90 0      5.8  3.3  70   310 8.0 4.3 120 320
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 2 1.4  1.3  15   75 .88 0      4.1  2.3  83   290 7.4 4.0 79 320
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 2 1.4  1.5  17   75 .90 0      6.7  3.7  130   310 8.0 4.3 110 320
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 2 1.4  1.5  16   84 .90 0      5.2  2.9  100   320 7.9 4.3 89 330
termination-crafted-lit/genady_true-termination_true-no-overflow.c 0 880    930    8000   1200 .86 0      .53 .36 10   42 5.8 3.1 110 290
termination-crafted-lit/strchr_true-no-overflow.c 2 1.4  1.5  17   83 .88 0      5.2  2.9  110   300 7.9 4.2 140 320
termination-numeric/Addition01_false-no-overflow.c 1 1.6  1.6  19   84 .89 0      3.1  1.8  73   250 7.8 4.1 140 310
termination-numeric/Avg_true_false-no-overflow.c 1 1.6  1.6  19   73 .90 0      3.4  1.9  67   250 7.4 4.0 150 310
termination-numeric/Binomial_true-termination_false-no-overflow.c 0 880    930    9600   130 .93 0      .47 .31 5.0 39 5.7 3.0 81 290
termination-numeric/Et1_true_false-no-overflow.c 1 1.7  1.7  20   78 .89 0      3.8  2.1  81   250 8.0 4.2 150 320
termination-numeric/Et2_true_false-no-overflow.c 1 1.7  1.7  23   81 .89 0      3.7  2.1  52   250 7.7 4.1 160 320
termination-numeric/Et3_true_false-no-overflow.c 1 1.7  1.7  19   85 .88 0      3.5  2.0  68   250 7.4 3.9 120 320
termination-numeric/Et4_true_false-no-overflow.c 1 1.7  1.7  20   77 .89 0      3.6  2.0  50   260 7.2 3.8 120 310
termination-numeric/MultCommutative_false-no-overflow.c 0 1.6  1.6  21   87 .89 0      3.2  1.8  69   250 11   5.7 130 360
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 0 880    930    11000   83 .88 0      .46 .29 4.9 39 5.9 3.1 130 290
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 1 880    880    7900   280 .91 0      3.3  1.9  64   250 660   530   7900 7000
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 1 880    880    10000   210 .89 0      3.3  1.9  72   240 960   800   9200 4500
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 1 880    880    9400   240 .89 0      3.4  1.9  73   250 960   890   16000 5700
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 2 880    880    11000   250 .88 0      3.4  1.9  75   240 8.7 4.6 130 330
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 0 880    930    11000   91 .88 0      .52 .34 8.9 40 5.7 3.0 84 290
termination-numeric/Parts_true-termination_true-no-overflow.c 1 880    880    9500   380 .91 0      2.7  1.6  56   220 960   800   12000 4800
termination-numeric/TwoWay_true-termination_true-no-overflow.c 0 740    740    8300   100 .89 0      .50 .32 12   39 5.2 2.8 52 300
termination-numeric/gcd01_true-termination_true-no-overflow.c 2 880    880    10000   94 .89 0      3.4  1.9  70   250 8.0 4.3 93 320
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 2 21    21    230   120 .86 .0041 4.1  2.3  79   280 59   35   790 830
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 0 2.0  1.9  27   76 .89 0      .54 .34 13   42 5.6 3.0 100 300
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 1 880    880    9100   340 .89 0      2.8  1.6  67   190 960   810   15000 5100
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 1 880    880    9600   320 .89 0      2.7  1.5  56   220 960   810   14000 4900
termination-numeric/twisted_true-termination_true-no-overflow.c 2 880    880    11000   200 .89 0      6.3  3.4  110   300 960   800   17000 2900
../../sv-benchmarks/c/ verifier status score witness inspect witness 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 274 311 89000   89000   1000000 78000 240    .025  274 670   440   13000 42000   274 1200 620   20000 50000   274 9200 8700 150000 86000   274 23000 19000 320000 150000  
    correct results 236 329 60000   60000   700000 55000 210    .025  132 570   350   11000 38000   143 1100 560   18000 46000   79 4700 4400 79000 55000   83 9500 7800 140000 82000  
        correct true 93 186 59000   59000   690000 43000 82    .0082 10 0   0   0 0   4 0 0   0 0   70 4700 4400 79000 55000   83 9500 7800 140000 82000  
        correct false 143 143 380   380   4200 12000 130    .016  122 570   350   11000 38000   139 1100 560   18000 46000   9 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 16 14 12000   12000   130000 5200 14    0      0 96   83   1300 3900   2 17 9.3 210 680   0 4500 4300 70000 31000   0 13000 11000 180000 66000  
        correct-unconfirmed true 14 14 12000   12000   130000 5000 13    0      0 0   0   0 0   2 0 0   0 0   0 4500 4300 70000 31000   0 13000 11000 180000 66000  
        correct-unconfirmed false 2 0 3.4 3.4 43 160 1.8  0      0 96   83   1300 3900   0 17 9.3 210 680   0 0 0 0 0   0 0 0 0 0  
    incorrect results 1 -32 880   880   11000 230 .88 0      1 4.0 2.2 81 280   1 40 24   390 770   0 0 0 0 0   0 0 0 0 0  
        incorrect true 1 -32 880   880   11000 230 .88 0      1 4.0 2.2 81 280   0 40 24   390 770   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (274 tasks, max score: 393) 311
Run set sv-comp17.Overflows-BitVectors