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 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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 .15  .15  1.8  23 .84 0   false(unreach-call) 5.6  3.0  110   300 false(unreach-call) 9.4 5.1 180 350 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .11  .11  1.1  23 .84 0   false(unreach-call) 4.5  2.5  88   290 false(unreach-call) 7.2 3.9 150 310 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .081 .082 .87 23 .84 0   true 3.3  1.9  47   270 false(unreach-call) 7.0 3.8 140 310 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .077 .076 .85 23 .84 0   false(unreach-call) 4.2  2.3  99   270 false(unreach-call) 7.8 4.2 150 320 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .15  .15  1.4  23 .84 0   false(unreach-call) 56    37    800   1500 timeout 96   69   1100 5300 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect .79  .77  8.9  95 .84 0   timeout 97    70    2200   4300 timeout 98   74   1700 5400 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .082 .081 .86 23 .84 0   false(unreach-call) 3.9  2.2  55   280 false(unreach-call) 7.8 4.1 140 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8300    3900 .84 0   - - error (invalid witness file) .51 .33 9.6 40 error (invalid witness file) 6.0 3.2 110 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8800    3600 .84 0   - - error (invalid witness file) .52 .35 9.4 39 error (invalid witness file) 6.0 3.2 110 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8400    3900 .84 0   - - error (invalid witness file) .48 .32 12   39 error (invalid witness file) 5.4 2.9 87 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 870     860     6100    15000 .84 0   - - error (invalid witness file) .50 .33 4.0 40 error (invalid witness file) 5.9 3.2 110 290
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 380     380     3600    15000 .84 0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 5.9 3.1 110 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 490     490     6800    15000 .84 0   - - error (invalid witness file) .50 .31 8.8 39 error (invalid witness file) 5.9 3.1 120 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     8800    2300 .84 0   - - error (invalid witness file) .52 .32 9.8 40 error (invalid witness file) 6.2 3.3 120 290
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .33  .32  3.7  26 .84 0   - - error (recursion) 3.6  2.0  65   260 true 32   18   320 1300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    3200 .84 0   - - error (invalid witness file) .71 .46 9.9 39 error (invalid witness file) 5.9 3.2 120 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     8500    5000 .84 0   - - error (invalid witness file) .54 .35 5.5 42 error (invalid witness file) 5.1 2.8 85 290
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7000    2500 .99 0   - - error (invalid witness file) .64 .40 8.3 41 error (invalid witness file) 5.5 2.9 110 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 330     320     3200    15000 .84 0   - - error (invalid witness file) .53 .35 12   40 error (invalid witness file) 6.3 3.3 120 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    160 .84 0   - - error (invalid witness file) .54 .35 8.5 44 error (invalid witness file) 6.6 3.5 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) .58 .37 15   44 error (invalid witness file) 5.9 3.1 110 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 360     360     3000    15000 .84 0   - - error (invalid witness file) .51 .33 8.0 40 error (invalid witness file) 5.4 3.0 100 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.2   1.2   15    79 .84 0   - - error (recursion) 3.4  2.0  45   260 true 8.4 4.5 140 340
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.5   1.4   21    81 .90 0   - - error (recursion) 3.6  2.0  71   260 timeout 960   950   14000 2600
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .074 .073 .88 23 .84 0   false(unreach-call) 3.8  2.1  81   280 true 7.3 3.9 130 320 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .074 .074 .80 23 .84 0   false(unreach-call) 3.6  2.0  76   270 true 7.0 3.7 140 310 - -
recursive-simple/fibo_10_false-unreach-call.c false(unreach-call) 1 wit inspect .64  .63  7.4  30 .84 0   false(unreach-call) 8.3  4.4  100   450 true 7.0 3.7 130 320 - -
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 190     190     2200    150 .84 0   false(unreach-call) 40    28    620   2100 true 6.7 3.6 130 310 - -
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 900     900     11000    380 .84 0   error (invalid witness file) .52 .34 5.8 40 error (invalid witness file) 5.4 2.9 120 290 - -
recursive-simple/fibo_25_false-unreach-call.c timeout 0 wit inspect 900     900     10000    380 .84 0   error (invalid witness file) .51 .33 7.6 42 error (invalid witness file) 6.0 3.2 110 310 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .45  .44  5.2  25 .84 0   false(unreach-call) 9.6  5.1  170   460 true 7.2 3.8 120 310 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 97     97     1100    100 .84 0   false(unreach-call) 38    27    410   1900 true 7.1 3.8 140 310 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 900     900     11000    530 .84 0   error (invalid witness file) .51 .32 8.3 39 error (invalid witness file) 6.7 3.5 120 300 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 900     900     10000    560 .84 0   error (invalid witness file) .58 .37 15   44 error (invalid witness file) 6.1 3.2 110 300 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .077 .71 23 .84 0   false(unreach-call) 3.6  2.1  77   280 true 7.1 3.8 140 310 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .077 .077 .83 23 .84 0   false(unreach-call) 4.6  2.5  52   290 true 6.9 3.7 130 310 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .085 .084 .90 23 .84 0   false(unreach-call) 5.0  2.7  97   290 true 7.8 4.2 140 330 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .094 .093 1.1  23 .84 0   false(unreach-call) 5.4  2.9  97   290 true 8.0 4.3 160 330 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c false(unreach-call) 1 wit inspect .15  .14  1.5  23 .84 0   false(unreach-call) 7.3  3.9  140   310 true 7.3 3.9 140 320 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .096 .094 .91 23 .84 0   false(unreach-call) 5.0  2.8  91   280 true 7.3 3.9 140 320 - -
recursive-simple/fibo_7_false-unreach-call.c false(unreach-call) 1 wit inspect .16  .15  1.4  23 .84 0   false(unreach-call) 5.5  3.0  100   290 true 6.7 3.6 120 320 - -
recursive-simple/id2_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .75 23 .84 0   false(unreach-call) 5.0  2.7  81   290 false(unreach-call) 8.2 4.4 130 350 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  .76 23 .84 0   false(unreach-call) 5.2  2.8  69   290 true 7.3 3.9 150 320 - -
recursive-simple/id_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect .082 .081 .87 23 .84 0   false(unreach-call) 4.6  2.5  93   280 false(unreach-call) 9.7 5.2 160 350 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .11  1.2  23 .84 0   false(unreach-call) 5.4  3.0  50   290 true 6.6 3.5 150 300 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  .13  1.2  23 .84 0   false(unreach-call) 4.6  2.5  65   280 true 6.7 3.6 130 300 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16  .16  1.4  24 .84 0   false(unreach-call) 5.1  2.8  100   280 true 7.5 4.0 130 320 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .19  .18  1.9  26 .84 0   false(unreach-call) 6.1  3.4  81   290 true 6.9 3.7 140 320 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .12  .87 23 .84 0   false(unreach-call) 4.2  2.3  67   290 true 7.6 4.0 150 330 - -
recursive-simple/id_o1000_false-unreach-call.c timeout 0 wit inspect 900     900     13000    13000 .84 0   error (invalid witness file) .55 .36 15   44 error (invalid witness file) 5.9 3.2 120 310 - -
recursive-simple/id_o100_false-unreach-call.c false(unreach-call) 0 wit inspect 12     12     140    530 .84 0   timeout 96    76    2200   4100 timeout 97   68   1200 4700 - -
recursive-simple/id_o10_false-unreach-call.c false(unreach-call) 1 wit inspect .15  .15  1.8  25 .84 0   false(unreach-call) 6.6  3.6  90   310 timeout 96   61   660 6200 - -
recursive-simple/id_o200_false-unreach-call.c false(unreach-call) 0 wit inspect 86     86     1200    2400 .84 0   timeout 96    76    2100   4100 timeout 96   68   1100 5600 - -
recursive-simple/id_o20_false-unreach-call.c false(unreach-call) 1 wit inspect 1.3   1.3   2.6  41 .84 0   false(unreach-call) 15    7.8  280   540 timeout 97   64   830 6100 - -
recursive-simple/id_o3_false-unreach-call.c false(unreach-call) 1 wit inspect .086 .085 .88 23 .84 0   false(unreach-call) 4.6  2.6  98   280 false(unreach-call) 9.2 5.0 170 350 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  .099 1.0  23 .84 0   false(unreach-call) 4.7  2.6  100   290 true 7.8 4.1 120 310 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .11  1.2  23 .84 0   false(unreach-call) 4.6  2.5  71   290 true 7.5 3.9 130 330 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .13  1.4  24 .84 0   false(unreach-call) 4.9  2.7  100   280 true 7.5 4.0 92 310 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20  .20  2.0  27 .84 0   false(unreach-call) 5.2  2.9  91   300 true 6.8 3.6 120 310 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 .081 .84 23 .84 0   false(unreach-call) 3.9  2.2  65   280 true 6.5 3.6 130 310 - -
recursive-simple/sum_non_eq_false-unreach-call.c false(unreach-call) 1 wit inspect .073 .072 .97 23 .84 0   false(unreach-call) 3.7  2.1  69   270 false(unreach-call) 11   5.5 110 340 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .072 .072 .90 23 .84 0   false(unreach-call) 3.6  2.0  48   280 false(unreach-call) 7.4 3.9 160 320 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .072 .071 .84 23 .84 0   - - true 3.2  1.8  42   260 true 7.3 3.9 85 330
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .085 .084 .76 23 .84 0   - - true 3.2  1.8  55   260 true 8.0 4.2 150 330
recursive-simple/fibo_10_true-unreach-call.c true 2 wit inspect .59  .58  6.7  31 .84 0   - - error (recursion) 3.5  2.0  65   260 true 40   23   390 2900
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 220     220     3100    190 .84 0   - - error (recursion) 5.0  2.7  94   280 true 610   560   12000 6300
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900     900     10000    380 .84 0   - - error (invalid witness file) .48 .33 6.6 40 error (invalid witness file) 5.8 3.1 120 310
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900     900     2000    210 .84 0   - - error (invalid witness file) .51 .33 9.2 40 error (invalid witness file) 6.6 3.5 150 310
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .38  .37  4.5  25 .84 0   - - error (recursion) 3.9  2.2  56   260 true 82   50   770 4100
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 130     130     1600    150 .84 0   - - error (recursion) 4.5  2.5  56   270 timeout 960   900   14000 5500
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900     900     11000    520 .84 0   - - error (invalid witness file) .52 .34 8.8 40 error (invalid witness file) 6.0 3.2 120 300
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900     900     13000    580 .84 0   - - error (invalid witness file) .47 .30 6.9 39 error (invalid witness file) 6.5 3.4 140 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .098 .098 .74 23 .84 0   - - true 3.4  1.9  54   260 true 11   6.3 200 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .30  .30  .84 23 .84 0   - - error (recursion) 3.8  2.1  80   260 true 21   12   400 540
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  .77 23 .84 0   - - error (recursion) 3.6  2.0  70   260 true 24   13   300 650
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .12  .12  .87 23 .84 0   - - error (recursion) 3.5  2.0  72   260 true 32   19   280 730
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .16  .16  1.3  23 .84 0   - - error (recursion) 3.4  1.9  27   260 true 51   30   470 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .099 .097 1.2  23 .84 0   - - error (recursion) 3.5  1.9  40   270 true 16   9.1 210 550
recursive-simple/fibo_7_true-unreach-call.c true 2 wit inspect .17  .17  1.7  23 .84 0   - - error (recursion) 4.3  2.4  41   260 true 21   12   270 650
recursive-simple/id2_b2_o3_true-unreach-call.c out of memory 0 wit inspect 440     430     5300    15000 .84 0   - - error (invalid witness file) .53 .35 8.6 40 error (invalid witness file) 6.3 3.3 110 300
recursive-simple/id2_b3_o5_true-unreach-call.c out of memory 0 wit inspect 510     510     6400    15000 .84 0   - - error (invalid witness file) .53 .34 9.2 43 error (invalid witness file) 5.7 3.0 120 300
recursive-simple/id2_b5_o10_true-unreach-call.c out of memory 0 wit inspect 460     460     6200    15000 .84 0   - - error (invalid witness file) .47 .31 6.3 39 error (invalid witness file) 6.0 3.2 110 310
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .090 .089 .97 23 .84 0   - - error (recursion) 3.1  1.8  50   260 true 13   7.5 200 460
recursive-simple/id_b2_o3_true-unreach-call.c out of memory 0 wit inspect 430     420     5100    15000 .84 0   - - error (invalid witness file) .63 .39 8.0 40 error (invalid witness file) 5.8 3.1 110 300
recursive-simple/id_b3_o5_true-unreach-call.c out of memory 0 wit inspect 510     500     6900    15000 .84 0   - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 5.9 3.1 120 300
recursive-simple/id_b5_o10_true-unreach-call.c out of memory 0 wit inspect 460     460     5800    15000 .99 0   - - error (invalid witness file) .52 .35 8.8 39 error (invalid witness file) 6.2 3.4 130 310
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .38  .36  .72 23 .84 0   - - error (recursion) 3.2  1.8  42   250 true 17   9.5 230 540
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .11  .11  1.3  23 .84 0   - - error (recursion) 3.4  1.9  62   250 true 23   13   350 640
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .17  .17  1.4  24 .84 0   - - error (recursion) 3.6  2.0  65   270 true 32   18   460 710
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .67  .62  1.3  27 .84 0   - - error (recursion) 3.5  2.0  70   250 true 37   22   360 810
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .084 .082 .79 23 .84 0   - - error (recursion) 3.5  1.9  61   260 true 12   6.4 190 360
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .11  .11  1.0  23 .84 0   - - error (recursion) 3.4  1.9  49   260 true 19   11   240 540
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .12  .11  1.3  23 .84 0   - - error (recursion) 3.4  1.9  58   260 true 25   15   370 700
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .16  .15  1.6  24 .84 0   - - error (recursion) 3.4  1.9  57   260 true 38   22   370 630
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .18  .18  2.2  27 .84 0   - - error (recursion) 3.4  1.9  41   260 true 41   25   410 860
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .10  .10  .80 23 .84 0   - - error (recursion) 3.3  1.9  63   260 true 11   6.3 190 410
recursive-simple/sum_non_eq_true-unreach-call.c timeout 0 wit inspect 900     900     13000    2200 .84 0   - - error (invalid witness file) .51 .33 9.3 40 error (invalid witness file) 6.2 3.3 120 300
recursive-simple/sum_non_true-unreach-call_true-termination.c out of memory 0 wit inspect 350     340     4100    15000 .84 0   - - error (invalid witness file) .49 .32 7.8 40 error (invalid witness file) 6.4 3.4 130 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 89 23000 23000 260000 230000 83   0   98 610 410 11000 29000   98 870 560 12000 46000   98 110   63   1800 8000   98 3300 2800 50000 43000  
    correct results 62 87 520 520 6500 1900 52   0   37 310 190 4900 16000   34 550 330 7300 29000   3 88   50   1400 6500   25 1200 920 19000 27000  
        correct true 25 50 220 220 3100 830 21   0   1 0 0 0 0   24 0 0 0 0   3 88   50   1400 6500   25 1200 920 19000 27000  
        correct false 37 37 290 290 3400 1100 31   0   36 310 190 4900 16000   10 550 330 7300 29000   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 5 2 240 230 3000 3200 4.3 0   0 290 220 6500 13000   0 290 210 4000 16000   0 8.1 4.5 130 530   0 1900 1800 28000 8100  
        correct-unconfirmed true 2 2 140 140 1700 230 1.7 0   0 0 0 0 0   0 0 0 0 0   0 8.1 4.5 130 530   0 1900 1800 28000 8100  
        correct-unconfirmed false 3 0 100 99 1300 3000 2.5 0   0 290 220 6500 13000   0 290 210 4000 16000   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) 89
Run set sv-comp17.ReachSafety-Recursive