Tool impara 0.45
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-23-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-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]
Run set sv-comp16.Recursive
Options --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.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 timeout 900     900     330 wit - -
recursive/Addition02_false-unreach-call_false-termination.c timeout 900     900     66 wit - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) .086 .094 23 wit false(reach) 7.1 4.1 350 false(reach) 12 7.2 340
recursive/EvenOdd03_false-unreach-call_false-termination.c timeout 900     900     250 wit - -
recursive/Fibonacci04_false-unreach-call_true-termination.c timeout 900     900     89 wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c timeout 900     900     89 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c timeout 900     900     290 wit - -
recursive/Ackermann01_true-unreach-call.c timeout 900     900     71 wit - -
recursive/Ackermann03_true-unreach-call.c timeout 900     900     73 wit - -
recursive/Ackermann04_true-unreach-call.c timeout 900     900     71 wit - -
recursive/Addition01_true-unreach-call_true-termination.c timeout 900     900     130 wit - -
recursive/Addition03_true-unreach-call.c timeout 900     900     57 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c timeout 900     900     260 wit - -
recursive/Fibonacci01_true-unreach-call.c false(reach) 7.3   7.3   30 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c false(reach) .16  .17  26 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c false(reach) 7.1   7.1   30 wit - -
recursive/McCarthy91_true-unreach-call.c timeout 900     900     290 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 900     900     99 wit - -
recursive/Primes_true-unreach-call.c timeout 900     900     86 wit - -
recursive/gcd01_true-unreach-call_true-termination.c timeout 900     900     62 wit - -
recursive/gcd02_true-unreach-call.c timeout 900     900     74 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c timeout 900     900     110 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true .49  .49  23 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 5.3   5.3   24 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) .11  .11  23 wit false(reach) 6.8 3.8 350 false(reach) 10 7.6 320
recursive-simple/afterrec_false-unreach-call.c false(reach) .15  .15  23 wit false(reach) 6.1 3.6 350 false(reach) 12 6.6 330
recursive-simple/fibo_10_false-unreach-call.c true .13  .14  23 wit - -
recursive-simple/fibo_15_false-unreach-call.c true .17  .18  23 wit - -
recursive-simple/fibo_20_false-unreach-call.c true .24  .24  23 wit - -
recursive-simple/fibo_25_false-unreach-call.c true .27  .27  23 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c true .14  .15  23 wit - -
recursive-simple/fibo_2calls_15_false-unreach-call.c true .20  .21  23 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c true .28  .29  23 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c true .38  .38  23 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) .13  .14  23 wit false(reach) 4.9 2.9 230 false(reach) 12 7.5 330
recursive-simple/fibo_2calls_4_false-unreach-call.c true .15  .16  23 wit - -
recursive-simple/fibo_2calls_5_false-unreach-call.c true .13  .14  23 wit - -
recursive-simple/fibo_2calls_6_false-unreach-call.c true .16  .17  23 wit - -
recursive-simple/fibo_2calls_8_false-unreach-call.c true .093 .098 23 wit - -
recursive-simple/fibo_5_false-unreach-call.c true .082 .090 23 wit - -
recursive-simple/fibo_7_false-unreach-call.c true .16  .17  23 wit - -
recursive-simple/id2_b3_o2_false-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) .089 .094 23 wit false(reach) 7.4 4.2 360 false(reach) 14 8.6 340
recursive-simple/id_b3_o2_false-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) .098 .10  23 wit false(reach) 7.2 4.2 360 false(reach) 23 14   480
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) .18  .18  23 wit false(reach) 7.0 3.9 360 false(reach) 31 20   490
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) .14  .14  24 wit false(reach) 7.0 3.9 380 false(reach) 34 22   660
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) .15  .16  24 wit false(reach) 7.8 4.4 390 false(reach) 40 27   970
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) .15  .15  23 wit false(reach) 6.6 3.8 350 false(reach) 15 8.6 370
recursive-simple/id_o1000_false-unreach-call.c timeout 900     900     420 wit - -
recursive-simple/id_o100_false-unreach-call.c timeout 900     900     420 wit - -
recursive-simple/id_o10_false-unreach-call.c timeout 900     900     400 wit - -
recursive-simple/id_o200_false-unreach-call.c timeout 900     900     420 wit - -
recursive-simple/id_o20_false-unreach-call.c timeout 900     900     420 wit - -
recursive-simple/id_o3_false-unreach-call.c timeout 900     900     420 wit - -
recursive-simple/sum_10x0_false-unreach-call.c false(reach) .12  .12  24 wit false(reach) 6.9 3.9 360 false(reach) 22 14   480
recursive-simple/sum_15x0_false-unreach-call.c false(reach) .13  .14  24 wit false(reach) 7.4 4.3 370 false(reach) 28 18   530
recursive-simple/sum_20x0_false-unreach-call.c false(reach) .15  .16  26 wit false(reach) 7.8 4.4 380 false(reach) 33 21   670
recursive-simple/sum_25x0_false-unreach-call.c false(reach) .17  .17  24 wit false(reach) 8.3 4.6 400 false(reach) 40 26   890
recursive-simple/sum_2x3_false-unreach-call.c false(reach) .11  .11  23 wit false(reach) 6.0 3.4 350 false(reach) 12 7.3 330
recursive-simple/sum_non_eq_false-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/sum_non_false-unreach-call.c timeout 900     900     690 wit - -
recursive-simple/afterrec_2calls_true-unreach-call.c true .10  .11  23 wit - -
recursive-simple/afterrec_true-unreach-call.c true .13  .13  23 wit - -
recursive-simple/fibo_10_true-unreach-call.c false(reach) .18  .18  24 wit - -
recursive-simple/fibo_15_true-unreach-call.c false(reach) .22  .22  24 wit - -
recursive-simple/fibo_20_true-unreach-call.c false(reach) .29  .29  26 wit - -
recursive-simple/fibo_25_true-unreach-call.c false(reach) .40  .40  25 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c false(reach) .15  .15  24 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c false(reach) .15  .16  24 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c false(reach) .32  .33  26 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c false(reach) .44  .44  25 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true .10  .10  23 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c false(reach) .14  .15  23 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c false(reach) .12  .13  23 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c false(reach) .16  .16  24 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c false(reach) .14  .14  23 wit - -
recursive-simple/fibo_5_true-unreach-call.c false(reach) .12  .12  25 wit - -
recursive-simple/fibo_7_true-unreach-call.c false(reach) .15  .15  24 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c timeout 900     900     480 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .11  .11  23 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c timeout 900     900     480 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c timeout 900     900     480 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true .14  .14  23 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true .16  .17  23 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true .17  .17  23 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true .13  .14  23 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true .11  .11  23 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true .11  .11  23 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true .15  .16  23 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true .14  .15  23 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true .15  .15  23 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .10  .10  23 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c timeout 900     900     470 wit - -
recursive-simple/sum_non_true-unreach-call.c timeout 900     900     690 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 32000   32000   13000 98 100   59   5400   98 340   220   7500  
    correct results 31 9.6 9.7 720 15 100   59   5400   15 340   220   7500  
        correct true 16 7.6 7.7 370 0 0   0   0   0 0   0   0  
        correct false 15 1.9 2.0 350 15 100   59   5400   15 340   220   7500  
    incorrect results 31 20   20   750 0 0   0   0   0 0   0   0  
        incorrect true 14 2.6 2.7 320 0 0   0   0   0 0   0   0  
        incorrect false 17 18   18   430 0 0   0   0   0 0   0   0  
score (98 tasks, max score: 151) -673
Run set sv-comp16.Recursive