Tool PAC-MAN
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:33:23 CET [[ 2016-01-15 09:22:08 CET ]] [[ 2016-01-15 22:28:32 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/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/pacman.2016-01-13_0733.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 false(reach) 11   11   360 wit false(reach) 11   5.8 460 true 11   6.4 320
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 1.8 1.9 360 wit false(reach) 7.8 4.3 370 true 11   6.9 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 8.1 4.7 370 true 9.5 5.6 330
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 1.8 1.9 320 wit false(reach) 6.9 3.9 360 true 11   7.0 330
recursive/Fibonacci04_false-unreach-call_true-termination.c witness timeout 2.1 2.1 320 wit timeout 91   69   2400 true 11   7.2 320
recursive/Fibonacci05_false-unreach-call_true-termination.c witness timeout 40   40   330 wit timeout 90   75   2700 true 12   7.0 340
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 1.5 1.6 110 wit false(reach) 6.3 3.6 360 true 10   6.0 330
recursive/Ackermann01_true-unreach-call.c true 660   900   160 wit - -
recursive/Ackermann03_true-unreach-call.c true 670   900   160 wit - -
recursive/Ackermann04_true-unreach-call.c true 650   900   160 wit - -
recursive/Addition01_true-unreach-call_true-termination.c unknown 890   900   370 wit - -
recursive/Addition03_true-unreach-call.c true 880   900   310 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c unknown 880   900   330 wit - -
recursive/Fibonacci01_true-unreach-call.c true 660   900   170 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 670   900   200 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c true 670   900   170 wit - -
recursive/McCarthy91_true-unreach-call.c true 650   900   180 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c true 660   900   210 wit - -
recursive/Primes_true-unreach-call.c true 880   900   450 wit - -
recursive/gcd01_true-unreach-call_true-termination.c unknown 900   900   6300 wit - -
recursive/gcd02_true-unreach-call.c unknown 890   900   620 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c true 680   900   180 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 660   900   160 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 660   900   160 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c witness unconfirmed 1.4 1.5 110 wit true 4.2 2.6 240 unknown 11   6.4 330
recursive-simple/afterrec_false-unreach-call.c witness unconfirmed 1.5 1.6 110 wit true 4.5 2.8 230 unknown 9.6 6.0 330
recursive-simple/fibo_10_false-unreach-call.c witness timeout 1.6 1.6 110 wit timeout 92   68   2900 true 12   6.7 330
recursive-simple/fibo_15_false-unreach-call.c witness invalid (exception) 5.5 5.6 110 wit exception 14   7.7 510 error 13   8.2 340
recursive-simple/fibo_20_false-unreach-call.c witness invalid (exception) 440   440   110 wit exception 22   11   760 error 16   9.2 440
recursive-simple/fibo_25_false-unreach-call.c timeout (false(reach)) 900   900   880 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness timeout 1.7 1.7 110 wit timeout 91   75   3300 true 12   6.9 340
recursive-simple/fibo_2calls_15_false-unreach-call.c witness invalid (exception) 5.2 5.3 110 wit exception 16   8.5 570 error 13   7.6 330
recursive-simple/fibo_2calls_20_false-unreach-call.c witness invalid (exception) 390   390   110 wit exception 21   11   770 error 16   9.5 450
recursive-simple/fibo_2calls_25_false-unreach-call.c witness unconfirmed 900   900   880 wit true 4.9 2.9 240 unknown 9.1 5.1 320
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 1.5 1.6 110 wit false(reach) 5.2 3.0 240 true 12   8.4 330
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 1.5 1.6 110 wit false(reach) 26   13   800 true 11   6.9 340
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 50   30   1600 true 12   7.0 340
recursive-simple/fibo_2calls_6_false-unreach-call.c witness timeout 1.4 1.4 110 wit timeout 90   57   1700 true 11   7.9 320
recursive-simple/fibo_2calls_8_false-unreach-call.c witness timeout 1.6 1.7 110 wit timeout 90   73   3000 true 12   7.3 330
recursive-simple/fibo_5_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 46   27   1500 true 11   6.5 330
recursive-simple/fibo_7_false-unreach-call.c witness timeout 1.3 1.3 110 wit timeout 91   76   2700 true 11   6.2 330
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 2.1 2.2 240 wit false(reach) 7.6 4.2 380 true 11   6.2 330
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 8.5 4.7 420 true 11   7.0 340
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 2.2 2.2 240 wit false(reach) 8.3 4.6 390 true 10   6.1 350
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 1.5 1.6 110 wit false(reach) 31   16   900 true 9.7 6.0 320
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 50   29   1600 true 11   6.4 320
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 1.3 1.4 110 wit false(reach) 61   42   2500 true 10   6.4 310
recursive-simple/id_i25_o25_false-unreach-call.c witness timeout 1.6 1.7 110 wit timeout 91   67   4000 true 11   7.1 320
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 9.0 5.0 420 true 11   6.3 330
recursive-simple/id_o1000_false-unreach-call.c unknown 880   900   250 wit - -
recursive-simple/id_o100_false-unreach-call.c unknown 870   900   250 wit - -
recursive-simple/id_o10_false-unreach-call.c false(reach) 1.8 1.8 240 wit false(reach) 23   12   760 true 11   6.9 310
recursive-simple/id_o200_false-unreach-call.c unknown 880   900   5400 wit - -
recursive-simple/id_o20_false-unreach-call.c unknown 880   900   7800 wit - -
recursive-simple/id_o3_false-unreach-call.c false(reach) 1.9 2.0 240 wit false(reach) 8.8 4.9 410 true 9.8 5.7 310
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 1.5 1.6 110 wit false(reach) 27   14   910 true 11   7.1 320
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 1.6 1.6 110 wit false(reach) 47   27   1600 true 11   6.1 330
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 1.6 1.7 110 wit false(reach) 77   56   3800 true 12   6.7 340
recursive-simple/sum_25x0_false-unreach-call.c witness timeout 1.5 1.6 110 wit timeout 91   70   2200 true 11   6.5 320
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 1.3 1.4 110 wit false(reach) 6.7 3.7 340 true 10   6.7 330
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 1.9 1.9 270 wit false(reach) 6.4 3.6 350 true 13   7.7 350
recursive-simple/sum_non_false-unreach-call.c false(reach) 1.9 1.9 270 wit false(reach) 14   7.2 570 true 11   7.2 330
recursive-simple/afterrec_2calls_true-unreach-call.c true 690   900   210 wit - -
recursive-simple/afterrec_true-unreach-call.c true 670   900   200 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 670   900   200 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 670   900   200 wit - -
recursive-simple/fibo_20_true-unreach-call.c true 700   900   170 wit - -
recursive-simple/fibo_25_true-unreach-call.c unknown 860   900   150 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 650   900   200 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c true 710   900   170 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown 860   900   150 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 670   900   200 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true 670   900   210 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true 670   900   210 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 670   900   210 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 690   900   210 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 870   900   250 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c unknown 890   900   7300 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 880   900   250 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c unknown 880   900   250 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c unknown 880   900   250 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c unknown 880   900   250 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 690   900   210 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 690   900   210 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true 670   900   200 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 680   900   210 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true 670   900   210 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c unknown 890   900   11000 wit - -
recursive-simple/sum_non_true-unreach-call.c unknown 880   900   280 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 45000 54000 57000 98 1500   1000   50000   98 450   270   13000  
    correct results 65 29000 37000 13000 24 550   330   21000   24 260   160   7900  
        correct true 41 28000 37000 8500 0 0   0   0   24 0   0   0  
        correct false 24 49 51 4100 24 550   330   21000   0 260   160   7900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 106
Run set sv-comp16.Recursive