Tool BLAST 2.7.3
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]]
Run set sv-comp16.Recursive
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
recursive/Ackermann02_false-unreach-call_false-termination.c exception (gremlins) 2.8   3.6   40 wit - -
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 1.4   1.8   25 wit false(reach) 7.5 4.2 360 false(reach) 13 7.6 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) .36  .40  24 wit true 5.8 3.2 250 false(reach) 12 6.5 340
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) .078 .083 20 wit false(reach) 6.5 3.7 340 false(reach) 12 6.8 340
recursive/Fibonacci04_false-unreach-call_true-termination.c exception (gremlins) 4.2   5.3   40 wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c exception (gremlins) 4.4   5.5   40 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) .082 .092 17 wit false(reach) 6.9 3.8 360 false(reach) 11 7.9 330
recursive/Ackermann01_true-unreach-call.c exception (gremlins) 37     48     58 wit - -
recursive/Ackermann03_true-unreach-call.c exception (gremlins) 6.2   7.9   38 wit - -
recursive/Ackermann04_true-unreach-call.c exception (gremlins) 5.8   7.5   38 wit - -
recursive/Addition01_true-unreach-call_true-termination.c exception (gremlins) 11     14     39 wit - -
recursive/Addition03_true-unreach-call.c exception (gremlins) 2.8   3.5   42 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c false(reach) .090 .094 21 wit - -
recursive/Fibonacci01_true-unreach-call.c exception (gremlins) 6.4   8.5   40 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c exception (gremlins) 34     40     40 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c exception (gremlins) 3.8   4.9   40 wit - -
recursive/McCarthy91_true-unreach-call.c false(reach) 6.1   8.0   40 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c exception (gremlins) 140     170     54 wit - -
recursive/Primes_true-unreach-call.c exception (gremlins) 110     120     570 wit - -
recursive/gcd01_true-unreach-call_true-termination.c false(reach) 6.8   8.9   43 wit - -
recursive/gcd02_true-unreach-call.c exception (gremlins) 22     28     41 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c exception (gremlins) 130     140     74 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c false(reach) 1.2   1.6   29 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c exception (gremlins) 3.9   5.2   37 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) .079 .083 20 wit false(reach) 6.5 3.6 360 false(reach) 11 6.9 330
recursive-simple/afterrec_false-unreach-call.c false(reach) .094 .098 16 wit false(reach) 6.0 3.6 350 false(reach) 12 6.7 340
recursive-simple/fibo_10_false-unreach-call.c exception (gremlins) 48     54     43 wit - -
recursive-simple/fibo_15_false-unreach-call.c exception (gremlins) 33     39     41 wit - -
recursive-simple/fibo_20_false-unreach-call.c exception (gremlins) 30     38     41 wit - -
recursive-simple/fibo_25_false-unreach-call.c exception (gremlins) 38     49     41 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c exception (gremlins) 35     40     46 wit - -
recursive-simple/fibo_2calls_15_false-unreach-call.c exception (gremlins) 85     94     42 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c exception (gremlins) 120     140     49 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c exception (gremlins) 110     130     50 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) .14  .14  19 wit false(reach) 4.8 2.9 230 false(reach) 12 6.7 350
recursive-simple/fibo_2calls_4_false-unreach-call.c true 9.7   13     34 wit - -
recursive-simple/fibo_2calls_5_false-unreach-call.c true 4.9   6.5   27 wit - -
recursive-simple/fibo_2calls_6_false-unreach-call.c true 6.3   8.4   31 wit - -
recursive-simple/fibo_2calls_8_false-unreach-call.c exception (gremlins) 34     40     40 wit - -
recursive-simple/fibo_5_false-unreach-call.c exception (gremlins) 8.1   10     39 wit - -
recursive-simple/fibo_7_false-unreach-call.c exception (gremlins) 19     23     39 wit - -
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) .60  .77  24 wit false(reach) 8.6 4.8 390 false(reach) 13 7.4 340
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) .14  .14  20 wit false(reach) 7.4 4.1 380 false(reach) 13 7.1 350
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) .44  .54  24 wit false(reach) 7.9 4.5 370 false(reach) 12 6.3 340
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) .063 .070 20 wit false(reach) 8.3 4.6 380 false(reach) 56 30   740
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) .11  .12  19 wit false(reach) 8.3 4.7 390 false(reach) 71 39   1000
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) .090 .094 19 wit false(reach) 8.5 4.9 390 false(reach) 89 49   1400
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) .063 .068 21 wit false(reach) 8.8 4.9 410 true 76 44   1300
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) .13  .13  19 wit false(reach) 8.1 4.4 370 false(reach) 34 18   560
recursive-simple/id_o1000_false-unreach-call.c witness timeout 1.1   1.5   27 wit timeout 91   70   3100 true 85 48   1300
recursive-simple/id_o100_false-unreach-call.c false(reach) 1.3   1.7   27 wit false(reach) 83   58   2700 timeout 92 48   1000
recursive-simple/id_o10_false-unreach-call.c false(reach) 1.6   2.2   27 wit false(reach) 22   11   590 false(reach) 66 36   730
recursive-simple/id_o200_false-unreach-call.c witness timeout 1.5   2.0   28 wit timeout 91   71   3300 timeout 91 53   1500
recursive-simple/id_o20_false-unreach-call.c false(reach) 1.4   1.9   27 wit false(reach) 31   16   810 false(reach) 89 50   1300
recursive-simple/id_o3_false-unreach-call.c false(reach) .74  .91  27 wit false(reach) 8.4 4.7 380 false(reach) 16 8.3 360
recursive-simple/sum_10x0_false-unreach-call.c false(reach) .14  .15  20 wit false(reach) 8.6 4.8 390 false(reach) 57 30   680
recursive-simple/sum_15x0_false-unreach-call.c false(reach) .078 .083 18 wit false(reach) 8.7 5.1 400 false(reach) 70 37   1000
recursive-simple/sum_20x0_false-unreach-call.c false(reach) .12  .13  21 wit false(reach) 9.2 5.1 400 false(reach) 85 47   1200
recursive-simple/sum_25x0_false-unreach-call.c false(reach) .11  .12  19 wit false(reach) 9.4 5.2 410 true 85 48   1300
recursive-simple/sum_2x3_false-unreach-call.c false(reach) .13  .13  20 wit false(reach) 6.7 3.7 350 false(reach) 11 7.7 340
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) .058 .062 19 wit false(reach) 6.3 3.6 360 false(reach) 12 6.5 330
recursive-simple/sum_non_false-unreach-call.c false(reach) .081 .090 16 wit false(reach) 6.2 3.5 340 false(reach) 12 7.2 340
recursive-simple/afterrec_2calls_true-unreach-call.c true .030 .035 13 wit - -
recursive-simple/afterrec_true-unreach-call.c true .015 .019 12 wit - -
recursive-simple/fibo_10_true-unreach-call.c exception (gremlins) 43     50     45 wit - -
recursive-simple/fibo_15_true-unreach-call.c exception (gremlins) 36     42     38 wit - -
recursive-simple/fibo_20_true-unreach-call.c exception (gremlins) 31     39     39 wit - -
recursive-simple/fibo_25_true-unreach-call.c exception (gremlins) 37     47     39 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c exception (gremlins) 35     41     45 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c exception (gremlins) 87     96     45 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c exception (gremlins) 120     130     47 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c exception (gremlins) 120     140     54 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true .023 .025 16 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c exception (gremlins) 8.4   10     36 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c exception (gremlins) 13     16     39 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c exception (gremlins) 27     32     41 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c exception (gremlins) 33     39     39 wit - -
recursive-simple/fibo_5_true-unreach-call.c exception (gremlins) 8.3   10     39 wit - -
recursive-simple/fibo_7_true-unreach-call.c exception (gremlins) 19     23     39 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true .47  .61  27 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true .48  .59  23 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true .62  .79  25 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .027 .032 14 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true .35  .42  24 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true .16  .19  23 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true .25  .31  27 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c false(reach) .13  .13  19 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c false(reach) .12  .12  18 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c false(reach) .081 .083 20 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c false(reach) .078 .084 20 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c false(reach) .089 .092 17 wit - -
recursive-simple/sum_10x0_true-unreach-call.c false(reach) .088 .093 19 wit - -
recursive-simple/sum_15x0_true-unreach-call.c false(reach) .14  .15  19 wit - -
recursive-simple/sum_20x0_true-unreach-call.c false(reach) .13  .14  19 wit - -
recursive-simple/sum_25x0_true-unreach-call.c false(reach) .13  .13  20 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .026 .030 13 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c exception (gremlins) 10     13     41 wit - -
recursive-simple/sum_non_true-unreach-call.c exception (gremlins) 12     14     44 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 98 1800   2100   3600 98 490   320   19000   98 1200   680   20000  
    correct results 37 12   15   760 26 310   180   12000   25 1000   580   17000  
        correct true 11 2.4 3.0 220 1 0   0   0   2 0   0   0  
        correct false 26 9.6 12   550 25 310   180   12000   23 1000   580   17000  
    incorrect results 16 36   47   400 0 0   0   0   0 0   0   0  
        incorrect true 3 21   28   92 0 0   0   0   0 0   0   0  
        incorrect false 13 15   20   310 0 0   0   0   0 0   0   0  
score (98 tasks, max score: 151) -256
Run set sv-comp16.Recursive