Tool ULTIMATE Kojak fd30d3d8
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-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 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/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.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 38   930   500 wit - -
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 9.7 3.0 330 wit false(reach) 6.9 4.1 350 false(reach) 13   7.8 330
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 9.6 3.0 330 wit true 4.6 2.6 220 false(reach) 12   6.7 340
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 9.0 2.8 330 wit false(reach) 6.6 3.7 350 false(reach) 11   6.5 340
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) 15   4.3 490 wit false(reach) 55   32   980 false(reach) 30   17   850
recursive/Fibonacci05_false-unreach-call_true-termination.c timeout 39   930   640 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 9.1 2.7 330 wit false(reach) 6.9 3.9 350 false(reach) 12   6.7 350
recursive/Ackermann01_true-unreach-call.c timeout 50   930   670 wit - -
recursive/Ackermann03_true-unreach-call.c timeout 38   930   570 wit - -
recursive/Ackermann04_true-unreach-call.c timeout 38   930   540 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 11   3.6 340 wit - -
recursive/Addition03_true-unreach-call.c timeout 38   930   640 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c timeout 58   930   1000 wit - -
recursive/Fibonacci01_true-unreach-call.c timeout 29   930   600 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c timeout 37   930   590 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c timeout 39   930   720 wit - -
recursive/McCarthy91_true-unreach-call.c true 11   3.2 330 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 37   930   580 wit - -
recursive/Primes_true-unreach-call.c timeout 42   930   830 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 12   3.2 350 wit - -
recursive/gcd02_true-unreach-call.c timeout 44   930   900 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c timeout 42   930   710 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 10   3.0 350 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 14   4.6 460 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 10   3.2 330 wit false(reach) 6.4 3.6 360 false(reach) 11   6.2 350
recursive-simple/afterrec_false-unreach-call.c false(reach) 8.6 2.7 320 wit false(reach) 6.5 3.7 350 false(reach) 12   7.1 340
recursive-simple/fibo_10_false-unreach-call.c timeout 40   930   670 wit - -
recursive-simple/fibo_15_false-unreach-call.c timeout 41   930   640 wit - -
recursive-simple/fibo_20_false-unreach-call.c timeout 39   930   690 wit - -
recursive-simple/fibo_25_false-unreach-call.c timeout 39   930   660 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c timeout 46   930   680 wit - -
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 49   930   860 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 47   930   660 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 44   930   830 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 8.9 2.9 320 wit false(reach) 4.9 2.8 230 false(reach) 12   6.6 340
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 12   3.8 340 wit false(reach) 24   12   610 false(reach) 19   10   460
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 17   5.1 470 wit false(reach) 34   18   820 false(reach) 45   24   880
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) 25   7.6 640 wit false(reach) 54   30   1600 timeout 90   52   2800
recursive-simple/fibo_2calls_8_false-unreach-call.c timeout 40   930   730 wit - -
recursive-simple/fibo_5_false-unreach-call.c false(reach) 14   4.3 470 wit false(reach) 29   15   680 false(reach) 35   19   880
recursive-simple/fibo_7_false-unreach-call.c false(reach) 30   7.5 490 wit false(reach) 77   55   2100 timeout 92   61   3600
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 10   3.2 320 wit false(reach) 8.3 4.7 380 false(reach) 12   7.1 340
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 13   3.9 470 wit false(reach) 8.2 4.8 370 false(reach) 13   8.3 350
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 11   3.1 360 wit false(reach) 7.5 4.3 360 false(reach) 13   7.1 350
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 32   15   810 wit false(reach) 8.9 5.1 390 true 13   7.6 360
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 57   32   910 wit false(reach) 9.8 5.6 420 true 12   7.0 350
recursive-simple/id_i20_o20_false-unreach-call.c timeout 100   930   920 wit - -
recursive-simple/id_i25_o25_false-unreach-call.c timeout 100   930   2800 wit - -
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 14   4.2 450 wit false(reach) 6.8 3.8 370 false(reach) 11   6.4 330
recursive-simple/id_o1000_false-unreach-call.c timeout 56   930   1200 wit - -
recursive-simple/id_o100_false-unreach-call.c timeout 55   930   910 wit - -
recursive-simple/id_o10_false-unreach-call.c false(reach) 15   4.7 360 wit false(reach) 9.4 5.2 410 true 12   6.8 350
recursive-simple/id_o200_false-unreach-call.c timeout 54   930   820 wit - -
recursive-simple/id_o20_false-unreach-call.c false(reach) 28   9.6 600 wit false(reach) 14   7.5 470 true 13   7.5 370
recursive-simple/id_o3_false-unreach-call.c false(reach) 10   3.2 330 wit false(reach) 7.2 4.1 360 false(reach) 11   6.5 340
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 16   4.5 470 wit false(reach) 9.2 5.1 390 true 12   6.8 360
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 21   6.0 490 wit false(reach) 10   5.6 420 true 14   7.6 370
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 26   7.9 640 wit false(reach) 12   6.4 440 true 13   7.1 380
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 31   10   560 wit false(reach) 11   5.9 480 true 13   7.1 360
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 9.6 3.0 320 wit false(reach) 6.6 3.9 360 false(reach) 11   6.1 330
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 8.5 2.7 330 wit false(reach) 6.1 3.7 360 false(reach) 9.8 5.6 320
recursive-simple/sum_non_false-unreach-call.c false(reach) 9.4 2.8 330 wit false(reach) 6.3 3.6 350 false(reach) 12   7.1 350
recursive-simple/afterrec_2calls_true-unreach-call.c true 7.8 2.6 320 wit - -
recursive-simple/afterrec_true-unreach-call.c true 7.8 2.5 320 wit - -
recursive-simple/fibo_10_true-unreach-call.c timeout 36   930   650 wit - -
recursive-simple/fibo_15_true-unreach-call.c timeout 45   930   650 wit - -
recursive-simple/fibo_20_true-unreach-call.c timeout 42   930   720 wit - -
recursive-simple/fibo_25_true-unreach-call.c timeout 41   930   650 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 47   930   860 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 49   930   940 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 45   930   1100 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 48   930   760 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c timeout 33   930   510 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c timeout 34   930   640 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c timeout 43   930   730 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c timeout 50   930   1100 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c timeout 38   930   650 wit - -
recursive-simple/fibo_5_true-unreach-call.c timeout 37   930   690 wit - -
recursive-simple/fibo_7_true-unreach-call.c timeout 48   930   710 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 9.4 2.8 330 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 9.1 2.9 320 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 8.9 2.8 330 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c timeout 46   930   690 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 9.6 2.9 330 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 10   3.3 320 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 9.1 2.9 320 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 21   7.6 470 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 30   12   600 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 41   18   980 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 51   25   1200 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 17   5.1 360 wit - -
recursive-simple/sum_10x0_true-unreach-call.c timeout 38   930   660 wit - -
recursive-simple/sum_15x0_true-unreach-call.c timeout 44   930   700 wit - -
recursive-simple/sum_20x0_true-unreach-call.c timeout 54   930   810 wit - -
recursive-simple/sum_25x0_true-unreach-call.c timeout 59   930   810 wit - -
recursive-simple/sum_2x3_true-unreach-call.c timeout 30   930   640 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true 11   3.0 340 wit - -
recursive-simple/sum_non_true-unreach-call.c true 11   3.3 310 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 3000 46000 60000 98 460   270   15000   98 590   340   18000  
    correct results 49 800 280 22000 29 460   270   15000   27 590   340   18000  
        correct true 20 310 110 8600 1 0   0   0   8 0   0   0  
        correct false 29 490 170 13000 28 460   270   15000   19 590   340   18000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 69
Run set sv-comp16.Recursive