Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .47  .46  1.3  23 .84 0   false(unreach-call) 6.6  3.6  84 290 false(unreach-call) 10   5.5 150 350 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .091 .090 .93 23 .84 0   false(unreach-call) 5.1  2.8  75 290 false(unreach-call) 7.6 4.1 92 320 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .073 .072 .88 23 .84 0   true 3.7  2.0  74 280 false(unreach-call) 9.0 4.8 100 320 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .11  .11  .73 23 .84 0   false(unreach-call) 4.8  2.6  75 280 false(unreach-call) 7.0 3.7 140 310 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .12  .12  1.2  23 .84 0   false(unreach-call) 64    43    600 1500 timeout 96   65   1300 5200 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 2.3   2.2   6.4  73 .84 0   timeout 97    70    1300 4200 timeout 97   74   1300 5100 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .074 .074 .83 23 .84 0   false(unreach-call) 4.5  2.4  68 290 false(unreach-call) 7.2 3.8 110 310 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 260     260     3000    15000 .84 0   - - error (invalid witness file) .52 .34 8.9 41 error (invalid witness file) 6.4 3.4 130 310
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 290     290     3500    15000 .84 0   - - error (invalid witness file) .52 .32 12   39 error (invalid witness file) 5.9 3.1 120 290
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 380     380     3900    15000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 5.9 3.1 120 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 470     470     3400    15000 .84 0   - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.5 3.4 130 310
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 240     230     2200    15000 .84 0   - - error (invalid witness file) .56 .37 13   44 error (invalid witness file) 5.7 3.0 110 290
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 800     790     9500    15000 .84 0   - - error (invalid witness file) .75 .48 9.1 43 error (invalid witness file) 7.1 3.7 120 330
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     11000    3200 .84 0   - - error (invalid witness file) .49 .34 6.1 39 error (invalid witness file) 6.4 3.4 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     860     11000    11000 .84 0   - - error (invalid witness file) .53 .35 11   39 error (invalid witness file) 5.8 3.1 110 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    5800 .84 0   - - error (invalid witness file) .53 .34 4.1 41 error (invalid witness file) 5.4 2.9 89 290
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    7000 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.3 3.3 120 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8100    9800 .84 0   - - error (invalid witness file) .47 .30 6.2 39 error (invalid witness file) 6.0 3.1 100 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 310     310     3400    15000 .84 0   - - error (invalid witness file) .49 .32 7.2 40 error (invalid witness file) 5.7 3.0 100 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    160 .84 0   - - error (invalid witness file) .52 .33 7.6 40 error (invalid witness file) 6.4 3.3 120 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    850 .84 0   - - error (invalid witness file) .53 .36 4.1 41 error (invalid witness file) 6.4 3.4 130 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 380     380     3200    15000 .84 0   - - error (invalid witness file) .52 .34 4.5 40 error (invalid witness file) 6.4 3.4 120 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 440     440     5400    15000 .84 0   - - error (invalid witness file) .50 .31 7.6 39 error (invalid witness file) 5.7 3.1 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 460     450     5100    15000 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.1 3.3 120 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .074 .073 .74 23 .84 0   false(unreach-call) 3.7  2.1  67 280 true 6.7 3.6 130 300 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  .57 23 .84 0   false(unreach-call) 3.7  2.1  59 270 true 5.9 3.2 86 310 - -
recursive-simple/fibo_10_false-unreach-call.c false(unreach-call) 1 wit inspect .54  .50  1.5  23 .84 0   false(unreach-call) 10    5.4  120 450 true 7.6 4.1 130 320 - -
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .96  .92  15    33 .88 0   false(unreach-call) 61    46    870 2000 true 6.8 3.7 110 320 - -
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 0 wit inspect 63     56     120    260 .84 0   timeout 97    82    950 1500 true 7.3 3.9 130 320 - -
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 0 wit inspect 210     210     2900    3000 .84 0   timeout 97    66    1200 6100 true 6.6 3.5 81 310 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .13  .13  1.4  23 .84 0   false(unreach-call) 9.2  4.9  140 460 true 7.6 4.0 110 320 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .65  .62  7.5  25 .84 0   false(unreach-call) 39    28    410 1900 true 8.7 4.6 95 310 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 0 wit inspect 7.8   7.5   99    170 .84 0   timeout 97    85    1500 1700 true 7.1 3.8 120 310 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 0 wit inspect 130     130     1600    2000 .84 0   timeout 97    56    1300 4700 true 8.2 4.3 100 310 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 .081 .74 23 .84 0   false(unreach-call) 4.5  2.5  56 280 true 7.1 3.8 110 320 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .099 .83 23 .84 0   false(unreach-call) 4.6  2.5  76 280 true 6.7 3.6 77 310 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .076 .075 .95 23 .84 0   false(unreach-call) 4.6  2.5  56 290 true 7.0 3.7 96 310 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .095 .094 .80 23 .84 0   false(unreach-call) 6.4  3.5  72 280 true 7.1 3.8 120 320 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c false(unreach-call) 1 wit inspect .12  .12  .76 23 .84 0   false(unreach-call) 6.6  3.6  110 300 true 9.2 4.9 97 320 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .077 .82 23 .84 0   false(unreach-call) 4.8  2.7  98 280 true 6.7 3.7 120 310 - -
recursive-simple/fibo_7_false-unreach-call.c false(unreach-call) 1 wit inspect .091 .090 .97 23 .84 0   false(unreach-call) 5.5  3.0  120 290 true 7.3 3.8 150 320 - -
recursive-simple/id2_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .081 .081 .87 23 .84 0   false(unreach-call) 5.1  2.8  90 290 false(unreach-call) 8.2 4.4 160 340 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  .65 23 .84 0   false(unreach-call) 5.1  2.8  61 280 true 9.2 4.9 100 320 - -
recursive-simple/id_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .86 23 .84 0   false(unreach-call) 4.4  2.4  36 280 false(unreach-call) 9.8 5.3 180 350 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .087 .087 .97 23 .84 0   false(unreach-call) 4.3  2.3  56 290 true 9.6 5.1 110 320 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .093 .092 .99 23 .84 0   false(unreach-call) 4.6  2.5  72 290 true 6.8 3.7 110 320 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  1.0  23 .84 0   false(unreach-call) 5.3  2.9  82 280 true 6.5 3.5 120 310 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  1.3  23 .84 0   false(unreach-call) 5.3  2.9  110 280 true 6.7 3.5 98 310 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .077 .81 23 .84 0   false(unreach-call) 4.1  2.2  47 290 true 6.7 3.6 76 320 - -
recursive-simple/id_o1000_false-unreach-call.c timeout 0 wit inspect 900     900     13000    6200 .84 0   error (invalid witness file) .49 .32 11 40 error (invalid witness file) 7.5 3.9 82 300 - -
recursive-simple/id_o100_false-unreach-call.c false(unreach-call) 0 wit inspect 8.8   8.7   130    250 .84 0   timeout 97    75    1100 4100 timeout 96   71   1100 5400 - -
recursive-simple/id_o10_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  1.4  23 .84 0   false(unreach-call) 7.9  4.2  84 330 timeout 97   62   1300 6500 - -
recursive-simple/id_o200_false-unreach-call.c false(unreach-call) 0 wit inspect 67     66     940    1000 .84 0   timeout 96    76    2200 4100 timeout 97   70   1100 6000 - -
recursive-simple/id_o20_false-unreach-call.c false(unreach-call) 1 wit inspect .26  .25  2.5  28 .84 0   false(unreach-call) 15    7.8  170 550 timeout 97   64   1100 5800 - -
recursive-simple/id_o3_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .89 23 .84 0   false(unreach-call) 4.4  2.4  59 280 false(unreach-call) 9.9 5.3 150 340 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  .82 23 .84 0   false(unreach-call) 4.4  2.4  69 290 true 6.6 3.5 130 310 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36  .35  .94 23 .84 0   false(unreach-call) 5.3  2.9  76 290 true 7.2 3.8 120 320 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .11  1.4  23 .84 0   false(unreach-call) 6.0  3.3  79 290 true 6.9 3.7 140 320 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .48  .45  1.2  23 .99 0   false(unreach-call) 6.0  3.3  57 280 true 7.0 3.7 81 310 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .10  .82 23 .84 0   false(unreach-call) 5.0  2.8  53 270 true 6.9 3.7 140 310 - -
recursive-simple/sum_non_eq_false-unreach-call.c false(unreach-call) 1 wit inspect .073 .073 .89 23 .84 0   false(unreach-call) 3.8  2.1  87 270 false(unreach-call) 7.1 3.8 130 310 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .077 .077 .79 23 .84 0   false(unreach-call) 3.7  2.1  81 270 false(unreach-call) 6.9 3.7 81 320 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c out of memory 0 wit inspect 880     800     11000    15000 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.0 3.2 120 310
recursive-simple/afterrec_true-unreach-call_true-termination.c out of memory 0 wit inspect 880     800     11000    15000 .84 0   - - error (invalid witness file) .53 .33 4.3 39 error (invalid witness file) 5.8 3.1 110 290
recursive-simple/fibo_10_true-unreach-call.c timeout 0 wit inspect 900     860     12000    11000 .84 0   - - error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.3 3.3 120 310
recursive-simple/fibo_15_true-unreach-call.c timeout 0 wit inspect 900     860     12000    9800 .84 0   - - error (invalid witness file) .62 .39 7.5 40 error (invalid witness file) 5.5 2.9 110 290
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900     870     11000    8400 .84 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.5 3.0 110 280
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900     870     11000    8500 .84 0   - - error (invalid witness file) .57 .37 9.9 43 error (invalid witness file) 5.7 3.1 110 290
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 wit inspect 900     860     12000    11000 .84 0   - - error (invalid witness file) .52 .34 13   39 error (invalid witness file) 5.7 3.0 100 290
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 wit inspect 900     860     12000    9500 .84 0   - - error (invalid witness file) .53 .33 8.0 41 error (invalid witness file) 6.9 3.6 130 320
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900     870     11000    8200 .84 0   - - error (invalid witness file) .50 .32 4.8 41 error (invalid witness file) 6.5 3.4 120 310
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900     870     11000    7900 .84 0   - - error (invalid witness file) .50 .31 8.8 40 error (invalid witness file) 5.6 3.0 120 290
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     12000    11000 .84 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.4 2.9 110 290
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     14000    11000 .84 0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.8 3.1 120 290
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     13000    12000 .84 0   - - error (invalid witness file) .55 .35 6.9 39 error (invalid witness file) 6.3 3.3 130 300
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     13000    11000 .84 0   - - error (invalid witness file) .50 .33 9.4 39 error (invalid witness file) 6.4 3.4 120 290
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     14000    11000 .84 0   - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.2 3.2 120 300
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     12000    12000 .84 0   - - error (invalid witness file) .50 .33 7.9 40 error (invalid witness file) 5.9 3.2 120 300
recursive-simple/fibo_7_true-unreach-call.c timeout 0 wit inspect 900     850     12000    12000 .84 0   - - error (invalid witness file) .61 .40 7.9 40 error (invalid witness file) 5.9 3.2 100 300
recursive-simple/id2_b2_o3_true-unreach-call.c out of memory 0 wit inspect 570     560     6900    15000 .84 0   - - error (invalid witness file) .51 .35 5.2 41 error (invalid witness file) 5.7 3.0 110 300
recursive-simple/id2_b3_o5_true-unreach-call.c timeout 0 wit inspect 900     900     11000    12000 .84 0   - - error (invalid witness file) .50 .32 8.9 39 error (invalid witness file) 6.0 3.2 120 300
recursive-simple/id2_b5_o10_true-unreach-call.c timeout 0 wit inspect 900     900     11000    14000 .84 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.8 3.1 110 300
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     11000    13000 .84 0   - - error (invalid witness file) .49 .33 8.1 40 error (invalid witness file) 6.1 3.2 120 290
recursive-simple/id_b2_o3_true-unreach-call.c out of memory 0 wit inspect 540     540     6600    15000 .84 0   - - error (invalid witness file) .55 .34 12   42 error (invalid witness file) 6.1 3.2 110 310
recursive-simple/id_b3_o5_true-unreach-call.c out of memory 0 wit inspect 820     810     9900    15000 .84 0   - - error (invalid witness file) .54 .36 5.6 41 error (invalid witness file) 6.0 3.2 110 290
recursive-simple/id_b5_o10_true-unreach-call.c out of memory 0 wit inspect 630     630     7700    15000 .84 0   - - error (invalid witness file) .53 .33 11   39 error (invalid witness file) 5.6 3.0 110 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     13000    13000 .84 0   - - error (invalid witness file) .48 .32 3.9 40 error (invalid witness file) 5.2 2.8 100 290
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     12000    12000 .84 0   - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.2 3.2 120 310
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     12000    12000 .84 0   - - error (invalid witness file) .63 .39 10   43 error (invalid witness file) 5.8 3.1 100 300
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     14000    11000 .84 0   - - error (invalid witness file) .57 .37 8.0 39 error (invalid witness file) 5.9 3.1 120 300
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     14000    13000 .84 0   - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.4 3.4 110 300
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     12000    14000 .84 0   - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.2 3.3 110 290
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     11000    13000 .84 0   - - error (invalid witness file) .58 .39 9.8 43 error (invalid witness file) 5.5 2.9 110 280
recursive-simple/sum_20x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900     860     14000    12000 .84 0   - - error (invalid witness file) .62 .39 10   43 error (invalid witness file) 5.9 3.1 120 300
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900     870     12000    11000 .84 0   - - error (invalid witness file) .54 .35 12   43 error (invalid witness file) 6.3 3.3 120 300
recursive-simple/sum_2x3_true-unreach-call_true-termination.c timeout 0 wit inspect 900     850     11000    13000 .84 0   - - error (invalid witness file) .51 .33 7.6 41 error (invalid witness file) 5.8 3.1 130 300
recursive-simple/sum_non_eq_true-unreach-call.c timeout 0 wit inspect 900     900     11000    1100 .84 0   - - error (invalid witness file) .50 .33 11   41 error (invalid witness file) 6.4 3.4 130 310
recursive-simple/sum_non_true-unreach-call_true-termination.c out of memory 0 wit inspect 580     570     7700    15000 .84 0   - - error (invalid witness file) .58 .38 4.7 44 error (invalid witness file) 5.9 3.2 110 300
../../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 98 37 43000   41000   550000 620000 82   0   98 1000 730 14000 42000 98 870 560 12000 46000 98 28 18 480 2200   98 320 170 6100 16000  
    correct results 37 37 6.6 6.5 57 870 31   0   37 350 220 4600 16000 34 550 330 7700 28000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 37 37 6.6 6.5 57 870 31   0   36 350 220 4600 16000 10 550 330 7700 28000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 7 0 490   470   5800 6700 5.9 0   0 680 510 9600 26000 4 320 230 4000 18000 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 7 0 490   470   5800 6700 5.9 0   0 680 510 9600 26000 0 320 230 4000 18000 0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 37
Run set sv-comp17.ReachSafety-Recursive