Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.Recursive
Options -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 true .95 1.1  38   wit - -
recursive/Addition02_false-unreach-call_false-termination.c true 1.6  2.0  38   wit - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c true .60 .70 39   wit - -
recursive/EvenOdd03_false-unreach-call_false-termination.c witness timeout 18    20    86   wit timeout 90   76   2700 true 12   7.7 330
recursive/Fibonacci04_false-unreach-call_true-termination.c true .81 .95 38   wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c true .58 .69 38   wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c true 3.9  4.6  38   wit - -
recursive/Ackermann01_true-unreach-call.c true .54 .62 38   wit - -
recursive/Ackermann03_true-unreach-call.c true 3.0  3.6  39   wit - -
recursive/Ackermann04_true-unreach-call.c true 590    620    39   wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 3.5  4.1  38   wit - -
recursive/Addition03_true-unreach-call.c true 190    200    39   wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 41    45    94   wit - -
recursive/Fibonacci01_true-unreach-call.c true 270    280    38   wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true .56 .65 38   wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c true .56 .67 38   wit - -
recursive/McCarthy91_true-unreach-call.c true 4.0  4.8  38   wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c true .68 .79 38   wit - -
recursive/Primes_true-unreach-call.c true .70 .81 36   wit - -
recursive/gcd01_true-unreach-call_true-termination.c error (134) 14    16    38   wit - -
recursive/gcd02_true-unreach-call.c true .67 .77 39   wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c true .56 .66 38   wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true .56 .65 38   wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 3.5  4.1  39   wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) .73 .83 57   wit false(reach) 6.2 3.5 370 true 9.8 5.6 310
recursive-simple/afterrec_false-unreach-call.c false(reach) .51 .60 38   wit false(reach) 5.7 3.3 350 true 12   6.8 350
recursive-simple/fibo_10_false-unreach-call.c false(reach) .54 .64 38   wit false(reach) 12   6.4 520 true 10   6.7 320
recursive-simple/fibo_15_false-unreach-call.c false(reach) .59 .69 38   wit false(reach) 75   50   2700 true 10   5.9 330
recursive-simple/fibo_20_false-unreach-call.c witness timeout .59 .72 38   wit timeout 90   71   2000 true 11   6.8 320
recursive-simple/fibo_25_false-unreach-call.c witness timeout .55 .64 38   wit timeout 90   61   5100 true 11   7.1 350
recursive-simple/fibo_2calls_10_false-unreach-call.c false(reach) .78 .87 83   wit false(reach) 13   6.9 510 true 10   6.1 340
recursive-simple/fibo_2calls_15_false-unreach-call.c false(reach) .79 .89 83   wit false(reach) 78   49   2000 true 10   5.8 320
recursive-simple/fibo_2calls_20_false-unreach-call.c witness timeout .81 .89 83   wit timeout 91   51   1900 true 12   7.0 350
recursive-simple/fibo_2calls_25_false-unreach-call.c witness timeout .66 .76 83   wit timeout 92   51   5400 true 13   7.5 370
recursive-simple/fibo_2calls_2_false-unreach-call.c true .62 .72 38   wit - -
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) .77 .87 83   wit false(reach) 6.8 3.8 360 true 10   8.1 330
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) .76 .86 83   wit false(reach) 7.8 4.3 380 true 10   6.4 320
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) .70 .79 83   wit false(reach) 8.1 4.5 400 true 9.9 6.4 320
recursive-simple/fibo_2calls_8_false-unreach-call.c false(reach) .73 .84 83   wit false(reach) 9.9 5.5 440 true 10   6.7 340
recursive-simple/fibo_5_false-unreach-call.c false(reach) .55 .64 38   wit false(reach) 6.7 3.8 360 true 11   6.7 350
recursive-simple/fibo_7_false-unreach-call.c false(reach) .60 .70 36   wit false(reach) 8.7 4.9 400 true 11   6.5 320
recursive-simple/id2_b3_o2_false-unreach-call.c unknown .70 .80 82   wit - -
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) .70 .79 62   wit false(reach) 6.6 3.8 350 true 10   5.8 340
recursive-simple/id_b3_o2_false-unreach-call.c true 3.3  3.9  38   wit - -
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) .61 .70 38   wit false(reach) 7.0 3.9 370 true 9.8 6.8 310
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) .57 .67 38   wit false(reach) 7.1 4.1 360 true 9.2 5.4 320
recursive-simple/id_i20_o20_false-unreach-call.c true .61 .70 38   wit - -
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) .49 .57 38   wit false(reach) 6.6 3.7 390 true 11   7.5 310
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) .55 .64 38   wit false(reach) 6.8 3.8 350 true 10   6.7 320
recursive-simple/id_o1000_false-unreach-call.c true 3.9  4.6  38   wit - -
recursive-simple/id_o100_false-unreach-call.c true 4.3  5.1  38   wit - -
recursive-simple/id_o10_false-unreach-call.c true 3.0  3.6  38   wit - -
recursive-simple/id_o200_false-unreach-call.c true .56 .65 38   wit - -
recursive-simple/id_o20_false-unreach-call.c error (134) 2.1  2.4  38   wit - -
recursive-simple/id_o3_false-unreach-call.c true .55 .65 38   wit - -
recursive-simple/sum_10x0_false-unreach-call.c false(reach) .54 .61 38   wit false(reach) 6.7 3.9 350 true 9.8 6.2 330
recursive-simple/sum_15x0_false-unreach-call.c false(reach) .52 .62 38   wit false(reach) 7.4 4.2 380 true 12   7.9 350
recursive-simple/sum_20x0_false-unreach-call.c false(reach) .58 .67 38   wit false(reach) 6.8 3.9 370 true 11   7.5 320
recursive-simple/sum_25x0_false-unreach-call.c false(reach) .53 .63 38   wit false(reach) 8.2 4.5 380 true 10   6.8 340
recursive-simple/sum_2x3_false-unreach-call.c false(reach) .49 .56 38   wit false(reach) 6.4 3.6 360 true 9.7 5.6 330
recursive-simple/sum_non_eq_false-unreach-call.c timeout 900    910    1200   wit - -
recursive-simple/sum_non_false-unreach-call.c true 1.2  1.4  38   wit - -
recursive-simple/afterrec_2calls_true-unreach-call.c true .63 .72 57   wit - -
recursive-simple/afterrec_true-unreach-call.c true .54 .63 38   wit - -
recursive-simple/fibo_10_true-unreach-call.c true 2.9  3.4  38   wit - -
recursive-simple/fibo_15_true-unreach-call.c true .62 .72 38   wit - -
recursive-simple/fibo_20_true-unreach-call.c true .68 .80 38   wit - -
recursive-simple/fibo_25_true-unreach-call.c true 23    25    41   wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c error (139) .92 1.1  83   wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c unknown .71 .79 83   wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown .78 .87 83   wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c true .81 .90 83   wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 1.2  1.3  83   wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c unknown .68 .76 83   wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c unknown .73 .83 83   wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true .73 .81 83   wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true .68 .77 83   wit - -
recursive-simple/fibo_5_true-unreach-call.c true .87 1.0  38   wit - -
recursive-simple/fibo_7_true-unreach-call.c true .53 .63 38   wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c error (134) 1.6  1.9  82   wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c unknown .68 .76 82   wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 3.5  4.1  82   wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .69 .80 63   wit - -
recursive-simple/id_b2_o3_true-unreach-call.c false(valid-free) 560    580    38   wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 350    360    39   wit - -
recursive-simple/id_b5_o10_true-unreach-call.c timeout 900    910    1200   wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 1.4  1.6  38   wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true .60 .70 38   wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 2.4  2.8  38   wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 1.1  1.4  38   wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true .66 .79 38   wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 1.5  1.7  38   wit - -
recursive-simple/sum_15x0_true-unreach-call.c true .62 .72 38   wit - -
recursive-simple/sum_20x0_true-unreach-call.c true .58 .68 38   wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 1.1  1.3  38   wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .53 .64 38   wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true .65 .75 38   wit - -
recursive-simple/sum_non_true-unreach-call.c true .22 .32 7.4 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 4000 4100 7200 98 760   500   30000   98 290   180   9000  
    correct results 65 1500 1600 3100 22 310   190   12000   22 230   140   7200  
        correct true 43 1500 1600 1900 0 0   0   0   22 0   0   0  
        correct false 22 14 16 1200 22 310   190   12000   0 230   140   7200  
    incorrect results 16 590 620 610 0 0   0   0   0 0   0   0  
        incorrect true 15 27 31 570 0 0   0   0   0 0   0   0  
        incorrect false 1 560 580 38 0 0   0   0   0 0   0   0  
score (98 tasks, max score: 151) -388
Run set sv-comp16.Recursive