Tool Ceagle AbsRef 1.0.0
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-04 05:59:47 CET [[ 2016-01-15 08:28:20 CET ]] [[ 2016-01-15 21:58:46 CET ]]
Run set sv-comp16.Recursive
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle-absref.2016-01-04_0559.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 unknown 3.5   3.5   12   wit - -
recursive/Addition02_false-unreach-call_false-termination.c unknown .50  .52  5.8 wit - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c true .28  .31  5.9 wit - -
recursive/EvenOdd03_false-unreach-call_false-termination.c witness unconfirmed .15  .18  5.7 wit true 5.3 2.9 250 true 11 7.6 320
recursive/Fibonacci04_false-unreach-call_true-termination.c unknown 1.9   1.9   9.4 wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c unknown 1.7   1.7   9.2 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c witness unconfirmed .22  .24  5.4 wit true 4.8 2.8 240 true 10 6.7 320
recursive/Ackermann01_true-unreach-call.c unknown 3.6   3.7   12   wit - -
recursive/Ackermann03_true-unreach-call.c unknown 3.7   3.7   12   wit - -
recursive/Ackermann04_true-unreach-call.c unknown 3.7   3.7   12   wit - -
recursive/Addition01_true-unreach-call_true-termination.c unknown .59  .63  5.8 wit - -
recursive/Addition03_true-unreach-call.c unknown .63  .66  6.0 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c unknown .26  .29  5.9 wit - -
recursive/Fibonacci01_true-unreach-call.c unknown 1.9   1.9   9.6 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c unknown .27  .30  5.7 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c unknown 1.8   1.8   9.4 wit - -
recursive/McCarthy91_true-unreach-call.c unknown .31  .33  5.6 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c unknown 18     18     38   wit - -
recursive/Primes_true-unreach-call.c unknown 3.1   3.1   12   wit - -
recursive/gcd01_true-unreach-call_true-termination.c unknown .75  .78  6.4 wit - -
recursive/gcd02_true-unreach-call.c unknown .96  .98  8.2 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c unknown 1.0   1.1   8.5 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c unknown .14  .17  5.9 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c unknown .21  .24  5.9 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c witness unconfirmed .067 .096 5.7 wit true 5.1 2.9 250 true 10 6.7 320
recursive-simple/afterrec_false-unreach-call.c witness unconfirmed .10  .13  6.0 wit true 4.8 2.8 240 true 11 7.2 310
recursive-simple/fibo_10_false-unreach-call.c unknown .25  .27  6.0 wit - -
recursive-simple/fibo_15_false-unreach-call.c unknown .24  .27  5.8 wit - -
recursive-simple/fibo_20_false-unreach-call.c unknown .34  .37  5.7 wit - -
recursive-simple/fibo_25_false-unreach-call.c unknown .26  .29  5.9 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c unknown .45  .48  5.7 wit - -
recursive-simple/fibo_2calls_15_false-unreach-call.c unknown .36  .39  5.6 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c unknown .27  .30  5.9 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c unknown .38  .40  5.9 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c true .31  .33  6.0 wit - -
recursive-simple/fibo_2calls_4_false-unreach-call.c true .40  .43  5.6 wit - -
recursive-simple/fibo_2calls_5_false-unreach-call.c true .31  .34  5.9 wit - -
recursive-simple/fibo_2calls_6_false-unreach-call.c unknown .28  .31  5.9 wit - -
recursive-simple/fibo_2calls_8_false-unreach-call.c unknown .35  .37  5.7 wit - -
recursive-simple/fibo_5_false-unreach-call.c true .48  .50  5.6 wit - -
recursive-simple/fibo_7_false-unreach-call.c unknown .34  .37  5.7 wit - -
recursive-simple/id2_b3_o2_false-unreach-call.c unknown .13  .15  5.6 wit - -
recursive-simple/id2_i5_o5_false-unreach-call.c unknown .15  .18  5.8 wit - -
recursive-simple/id_b3_o2_false-unreach-call.c unknown .19  .22  5.7 wit - -
recursive-simple/id_i10_o10_false-unreach-call.c unknown .14  .18  5.9 wit - -
recursive-simple/id_i15_o15_false-unreach-call.c unknown .072 .098 5.8 wit - -
recursive-simple/id_i20_o20_false-unreach-call.c unknown .10  .13  5.6 wit - -
recursive-simple/id_i25_o25_false-unreach-call.c unknown .11  .15  5.9 wit - -
recursive-simple/id_i5_o5_false-unreach-call.c unknown .14  .18  6.0 wit - -
recursive-simple/id_o1000_false-unreach-call.c unknown .11  .14  6.0 wit - -
recursive-simple/id_o100_false-unreach-call.c unknown .12  .14  6.0 wit - -
recursive-simple/id_o10_false-unreach-call.c unknown .12  .14  5.9 wit - -
recursive-simple/id_o200_false-unreach-call.c unknown .12  .15  5.6 wit - -
recursive-simple/id_o20_false-unreach-call.c unknown .16  .19  5.9 wit - -
recursive-simple/id_o3_false-unreach-call.c unknown .13  .15  5.9 wit - -
recursive-simple/sum_10x0_false-unreach-call.c unknown .097 .12  5.8 wit - -
recursive-simple/sum_15x0_false-unreach-call.c unknown .11  .14  5.9 wit - -
recursive-simple/sum_20x0_false-unreach-call.c unknown .16  .19  5.7 wit - -
recursive-simple/sum_25x0_false-unreach-call.c unknown .11  .14  5.8 wit - -
recursive-simple/sum_2x3_false-unreach-call.c witness unconfirmed .087 .12  5.7 wit true 4.8 2.8 240 true 12 7.4 340
recursive-simple/sum_non_eq_false-unreach-call.c witness unconfirmed .15  .18  5.9 wit true 4.7 2.9 240 true 10 6.2 320
recursive-simple/sum_non_false-unreach-call.c witness unconfirmed .11  .14  5.5 wit true 4.6 2.8 230 true 11 6.5 320
recursive-simple/afterrec_2calls_true-unreach-call.c true .12  .15  5.5 wit - -
recursive-simple/afterrec_true-unreach-call.c true .12  .14  5.6 wit - -
recursive-simple/fibo_10_true-unreach-call.c unknown .37  .39  5.9 wit - -
recursive-simple/fibo_15_true-unreach-call.c unknown .42  .45  6.0 wit - -
recursive-simple/fibo_20_true-unreach-call.c unknown .33  .37  5.9 wit - -
recursive-simple/fibo_25_true-unreach-call.c unknown .33  .36  5.7 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c unknown .31  .33  5.7 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown .31  .34  5.8 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown .40  .44  5.9 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown .36  .39  5.8 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c false(reach) .23  .26  5.6 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c false(reach) .47  .49  5.7 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c false(reach) .34  .37  5.6 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c unknown .32  .35  6.0 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c unknown .24  .27  5.7 wit - -
recursive-simple/fibo_5_true-unreach-call.c false(reach) .43  .45  5.7 wit - -
recursive-simple/fibo_7_true-unreach-call.c unknown .46  .50  5.9 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c unknown .22  .25  5.7 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c unknown .14  .16  5.9 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c unknown .21  .24  6.0 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c unknown .14  .18  5.6 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c unknown .15  .17  5.7 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c unknown .17  .19  5.6 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c unknown .13  .16  5.9 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c unknown .12  .14  5.9 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c unknown .13  .16  6.0 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c unknown .089 .12  5.5 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c unknown .12  .14  5.9 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c unknown .13  .16  5.8 wit - -
recursive-simple/sum_10x0_true-unreach-call.c unknown .14  .18  5.7 wit - -
recursive-simple/sum_15x0_true-unreach-call.c unknown .078 .10  5.7 wit - -
recursive-simple/sum_20x0_true-unreach-call.c unknown .10  .13  5.9 wit - -
recursive-simple/sum_25x0_true-unreach-call.c unknown .15  .19  5.7 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .16  .19  6.0 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c unknown .13  .16  5.9 wit - -
recursive-simple/sum_non_true-unreach-call.c unknown .097 .12  6.0 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 65    68    650 98 34   20   1700   98 75   48   2200  
    correct results 3 .40 .48 17 0 0   0   0   0 0   0   0  
        correct true 3 .40 .48 17 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 9 3.2  3.5  52 0 0   0   0   0 0   0   0  
        incorrect true 5 1.8  1.9  29 0 0   0   0   0 0   0   0  
        incorrect false 4 1.5  1.6  23 0 0   0   0   0 0   0   0  
score (98 tasks, max score: 151) -218
Run set sv-comp16.Recursive