Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 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/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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   3.2 330 wit false(reach) 24   12   750 false(reach) 19 11   410
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 10   3.1 330 wit false(reach) 7.5 4.4 370 false(reach) 14 7.6 350
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 9.3 2.9 330 wit true 5.0 2.9 220 false(reach) 12 7.4 320
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 8.9 2.8 330 wit false(reach) 6.7 3.8 350 false(reach) 12 7.2 330
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) 18   5.2 400 wit false(reach) 39   21   850 false(reach) 35 19   850
recursive/Fibonacci05_false-unreach-call_true-termination.c witness timeout 35   12   630 wit timeout 90   74   1600 timeout 92 58   4100
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 8.9 2.7 320 wit false(reach) 7.0 4.0 350 false(reach) 11 6.5 330
recursive/Ackermann01_true-unreach-call.c true 13   4.3 460 wit - -
recursive/Ackermann03_true-unreach-call.c true 28   11   540 wit - -
recursive/Ackermann04_true-unreach-call.c true 25   9.1 480 wit - -
recursive/Addition01_true-unreach-call_true-termination.c timeout 900   750   790 wit - -
recursive/Addition03_true-unreach-call.c true 630   510   1600 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c timeout 900   740   940 wit - -
recursive/Fibonacci01_true-unreach-call.c true 50   21   820 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 50   17   1100 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c true 38   14   860 wit - -
recursive/McCarthy91_true-unreach-call.c true 10   3.6 320 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 900   760   960 wit - -
recursive/Primes_true-unreach-call.c error 490   470   1000 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 12   4.2 360 wit - -
recursive/gcd02_true-unreach-call.c timeout 900   780   1600 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c error 210   150   5000 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 9.1 3.3 320 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c error 88   76   530 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 9.8 3.0 340 wit false(reach) 5.9 3.4 340 false(reach) 11 7.2 360
recursive-simple/afterrec_false-unreach-call.c false(reach) 8.8 2.6 330 wit false(reach) 5.3 3.0 340 false(reach) 12 7.1 330
recursive-simple/fibo_10_false-unreach-call.c witness timeout 50   18   990 wit timeout 91   70   2100 timeout 90 55   3300
recursive-simple/fibo_15_false-unreach-call.c witness invalid (exception) 240   170   5000 wit exception 53   35   1600 timeout 91 48   2800
recursive-simple/fibo_20_false-unreach-call.c timeout 900   780   6600 wit - -
recursive-simple/fibo_25_false-unreach-call.c timeout 900   780   6300 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness timeout 120   60   2600 wit timeout 91   69   2100 timeout 92 54   3600
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 900   690   5500 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 900   760   6400 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 900   750   6200 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 9.0 2.9 320 wit false(reach) 4.9 2.8 240 false(reach) 13 7.2 340
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 13   4.6 460 wit false(reach) 22   12   620 false(reach) 23 12   470
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 18   6.0 430 wit false(reach) 37   19   840 false(reach) 57 30   910
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) 25   8.5 680 wit false(reach) 54   32   1600 timeout 92 53   2500
recursive-simple/fibo_2calls_8_false-unreach-call.c witness timeout 63   21   1300 wit timeout 91   72   2400 timeout 90 58   3300
recursive-simple/fibo_5_false-unreach-call.c false(reach) 13   5.0 340 wit false(reach) 25   13   720 false(reach) 32 18   830
recursive-simple/fibo_7_false-unreach-call.c false(reach) 22   7.0 450 wit false(reach) 89   63   2100 timeout 92 62   3600
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 9.7 3.0 340 wit false(reach) 7.0 3.9 370 false(reach) 12 6.8 340
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 11   4.0 360 wit false(reach) 8.2 4.6 380 false(reach) 14 7.6 360
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 9.5 3.5 320 wit false(reach) 6.3 3.6 350 false(reach) 12 7.2 340
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 16   6.1 360 wit false(reach) 8.8 4.8 390 true 13 7.8 350
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 20   7.2 480 wit false(reach) 10   5.5 410 true 13 7.8 360
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 26   12   600 wit false(reach) 11   6.1 450 true 14 7.7 370
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) 30   14   610 wit false(reach) 14   7.5 490 true 16 9.0 380
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 12   5.1 350 wit false(reach) 6.7 3.7 370 false(reach) 14 7.5 350
recursive-simple/id_o1000_false-unreach-call.c timeout 900   740   1700 wit - -
recursive-simple/id_o100_false-unreach-call.c timeout 900   730   950 wit - -
recursive-simple/id_o10_false-unreach-call.c false(reach) 15   4.7 350 wit false(reach) 9.8 5.4 410 true 13 7.4 370
recursive-simple/id_o200_false-unreach-call.c timeout 900   730   950 wit - -
recursive-simple/id_o20_false-unreach-call.c false(reach) 27   11   690 wit false(reach) 14   7.6 470 true 15 8.3 390
recursive-simple/id_o3_false-unreach-call.c false(reach) 9.3 3.2 330 wit false(reach) 6.3 3.5 370 false(reach) 15 8.2 380
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 14   5.1 470 wit false(reach) 7.7 4.3 400 true 14 8.2 350
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 22   8.9 400 wit false(reach) 10   5.7 420 true 14 8.0 360
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 23   9.6 470 wit false(reach) 11   6.2 450 true 15 8.8 370
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 28   14   560 wit false(reach) 12   6.3 480 true 14 8.1 370
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 9.7 3.7 340 wit false(reach) 6.3 3.5 350 false(reach) 12 7.6 330
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 8.1 2.9 320 wit false(reach) 5.5 3.2 350 false(reach) 11 7.1 320
recursive-simple/sum_non_false-unreach-call.c false(reach) 8.7 2.7 320 wit false(reach) 6.5 3.7 340 false(reach) 12 7.3 340
recursive-simple/afterrec_2calls_true-unreach-call.c true 8.6 2.7 330 wit - -
recursive-simple/afterrec_true-unreach-call.c true 10   4.1 350 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 58   22   1300 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 270   200   5200 wit - -
recursive-simple/fibo_20_true-unreach-call.c timeout 900   770   6400 wit - -
recursive-simple/fibo_25_true-unreach-call.c timeout 900   780   6800 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 130   72   2100 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 900   720   5800 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 900   760   6400 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 900   770   6500 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 11   3.8 340 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true 16   5.9 410 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true 22   7.7 450 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true 29   10   670 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 70   25   1200 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 17   5.2 480 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 27   8.2 690 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 24   7.4 330 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 13   5.4 390 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 15   5.5 460 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true 12   4.0 330 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 10   4.3 320 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 11   3.5 330 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 14   4.5 470 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 16   5.2 460 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 22   7.8 620 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 25   11   650 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 34   16   620 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 12   3.8 400 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 19   6.3 500 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true 24   9.0 580 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true 26   12   660 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 36   17   750 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true 10   3.5 340 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c timeout 900   750   1400 wit - -
recursive-simple/sum_non_true-unreach-call.c timeout 900   770   830 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 21000 17000 130000 98 910   610   27000   98 1100   670   35000  
    correct results 71 2400 1300 42000 32 490   290   17000   30 680   400   18000  
        correct true 39 1900 1100 29000 1 0   0   0   10 0   0   0  
        correct false 32 490 180 13000 31 490   290   17000   20 680   400   18000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 110
Run set sv-comp16.Recursive