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