Tool CPAchecker 1.4-svcomp16c
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-22-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-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.Recursive
Options -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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 7.5 2.9 390 20   10   530 18 9.9 410
recursive/Addition02_false-unreach-call_false-termination.c 5.3 2.3 280 6.5 3.7 350 14 9.1 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c 5.2 2.1 360 6.6 3.8 340 12 7.9 330
recursive/EvenOdd03_false-unreach-call_false-termination.c 4.9 2.1 270 4.5 2.6 230 12 6.7 330
recursive/Fibonacci04_false-unreach-call_true-termination.c 13   4.9 600 65   41   1300 42 23   990
recursive/Fibonacci05_false-unreach-call_true-termination.c 23   12   790 90   73   1500 90 61   3000
recursive/McCarthy91_false-unreach-call_false-termination.c 4.6 2.0 270 6.2 3.5 260 11 6.5 330
recursive/Ackermann01_true-unreach-call.c 6.3 2.6 290
recursive/Ackermann03_true-unreach-call.c 62   47   2400
recursive/Ackermann04_true-unreach-call.c 21   11   780
recursive/Addition01_true-unreach-call_true-termination.c 5.3 2.2 320
recursive/Addition03_true-unreach-call.c 900   850   1800
recursive/EvenOdd01_true-unreach-call_true-termination.c 7.1 3.5 300
recursive/Fibonacci01_true-unreach-call.c 12   5.4 500
recursive/Fibonacci02_true-unreach-call_true-termination.c 8.2 2.3 430
recursive/Fibonacci03_true-unreach-call_true-termination.c 900   840   1800
recursive/McCarthy91_true-unreach-call.c 5.1 2.2 270
recursive/MultCommutative_true-unreach-call_true-termination.c 900   890   910
recursive/Primes_true-unreach-call.c 900   890   860
recursive/gcd01_true-unreach-call_true-termination.c 5.7 2.4 280
recursive/gcd02_true-unreach-call.c 900   890   1300
recursive/recHanoi01_true-unreach-call_true-termination.c 7.9 3.0 340
recursive/recHanoi02_true-unreach-call_true-termination.c 9.2 4.1 620
recursive/recHanoi03_true-unreach-call_true-termination.c 11   6.3 470
recursive-simple/afterrec_2calls_false-unreach-call.c 3.0 1.4 210 6.5 3.7 340 12 6.7 340
recursive-simple/afterrec_false-unreach-call.c 3.0 1.4 190 6.4 3.6 340 13 7.1 340
recursive-simple/fibo_10_false-unreach-call.c 9.6 3.4 500 91   73   2000 92 50   2500
recursive-simple/fibo_15_false-unreach-call.c 71   32   1900 33   17   810 91 53   3700
recursive-simple/fibo_20_false-unreach-call.c 900   870   2800
recursive-simple/fibo_25_false-unreach-call.c 900   850   7800
recursive-simple/fibo_2calls_10_false-unreach-call.c 9.9 3.6 490 91   70   1700 92 57   3700
recursive-simple/fibo_2calls_15_false-unreach-call.c 71   34   1800 28   15   770 92 52   2600
recursive-simple/fibo_2calls_20_false-unreach-call.c 900   870   2800
recursive-simple/fibo_2calls_25_false-unreach-call.c 900   740   8700
recursive-simple/fibo_2calls_2_false-unreach-call.c 3.2 1.4 210 4.7 2.8 230 13 7.6 330
recursive-simple/fibo_2calls_4_false-unreach-call.c 5.3 2.0 370 19   10   560 23 13   440
recursive-simple/fibo_2calls_5_false-unreach-call.c 6.3 2.4 370 34   18   790 52 28   840
recursive-simple/fibo_2calls_6_false-unreach-call.c 6.6 2.5 380 52   30   1500 91 53   2600
recursive-simple/fibo_2calls_8_false-unreach-call.c 8.3 2.9 420 91   73   2100 91 58   3100
recursive-simple/fibo_5_false-unreach-call.c 6.1 2.4 370 28   15   740 42 23   1000
recursive-simple/fibo_7_false-unreach-call.c 6.1 2.3 390 91   62   2000 90 63   2800
recursive-simple/id2_b3_o2_false-unreach-call.c 5.8 2.3 370 6.6 3.7 350 12 6.8 350
recursive-simple/id2_i5_o5_false-unreach-call.c 4.2 1.8 270 6.8 3.8 350 14 7.5 350
recursive-simple/id_b3_o2_false-unreach-call.c 4.1 1.8 270 6.5 3.7 340 13 7.1 340
recursive-simple/id_i10_o10_false-unreach-call.c 5.2 2.2 270 8.2 4.6 380 13 7.1 340
recursive-simple/id_i15_o15_false-unreach-call.c 5.6 2.2 280 9.1 5.1 410 14 12   360
recursive-simple/id_i20_o20_false-unreach-call.c 6.6 2.5 370 9.6 5.3 440 14 8.2 360
recursive-simple/id_i25_o25_false-unreach-call.c 6.6 2.5 370 13   7.1 480 14 12   360
recursive-simple/id_i5_o5_false-unreach-call.c 5.2 2.2 270 7.1 4.0 350 14 10   340
recursive-simple/id_o1000_false-unreach-call.c 450   380   4200 16   8.7 480 43 23   1500
recursive-simple/id_o100_false-unreach-call.c 15   4.1 640 38   22   1200 22 12   570
recursive-simple/id_o10_false-unreach-call.c 4.5 1.9 280 8.1 4.7 380 13 7.0 350
recursive-simple/id_o200_false-unreach-call.c 23   7.3 960 91   69   1900 25 13   680
recursive-simple/id_o20_false-unreach-call.c 6.9 2.6 390 11   5.8 430 13 9.4 370
recursive-simple/id_o3_false-unreach-call.c 4.9 2.1 270 6.5 3.8 340 13 8.9 350
recursive-simple/sum_10x0_false-unreach-call.c 4.5 1.9 280 8.0 4.5 380 12 6.6 360
recursive-simple/sum_15x0_false-unreach-call.c 5.5 2.2 280 9.7 5.4 410 13 7.3 370
recursive-simple/sum_20x0_false-unreach-call.c 6.6 2.5 370 10   5.7 440 15 12   370
recursive-simple/sum_25x0_false-unreach-call.c 7.0 2.5 380 13   6.7 490 14 7.9 370
recursive-simple/sum_2x3_false-unreach-call.c 5.0 2.1 270 6.1 3.6 350 13 8.5 340
recursive-simple/sum_non_eq_false-unreach-call.c 4.1 1.7 270 4.6 2.7 220 11 6.8 360
recursive-simple/sum_non_false-unreach-call.c 4.8 2.0 260 4.5 2.6 220 11 6.5 330
recursive-simple/afterrec_2calls_true-unreach-call.c 3.1 1.5 190
recursive-simple/afterrec_true-unreach-call.c 3.0 1.3 190
recursive-simple/fibo_10_true-unreach-call.c 9.6 3.0 540
recursive-simple/fibo_15_true-unreach-call.c 38   26   3600
recursive-simple/fibo_20_true-unreach-call.c 900   850   3700
recursive-simple/fibo_25_true-unreach-call.c 900   820   5100
recursive-simple/fibo_2calls_10_true-unreach-call.c 12   3.5 670
recursive-simple/fibo_2calls_15_true-unreach-call.c 52   38   3600
recursive-simple/fibo_2calls_20_true-unreach-call.c 900   840   3700
recursive-simple/fibo_2calls_25_true-unreach-call.c 900   810   5100
recursive-simple/fibo_2calls_2_true-unreach-call.c 3.2 1.5 180
recursive-simple/fibo_2calls_4_true-unreach-call.c 5.1 2.1 270
recursive-simple/fibo_2calls_5_true-unreach-call.c 4.7 1.9 270
recursive-simple/fibo_2calls_6_true-unreach-call.c 5.1 2.0 290
recursive-simple/fibo_2calls_8_true-unreach-call.c 8.7 2.8 380
recursive-simple/fibo_5_true-unreach-call.c 5.0 2.1 260
recursive-simple/fibo_7_true-unreach-call.c 6.5 2.3 300
recursive-simple/id2_b2_o3_true-unreach-call.c 4.9 2.1 270
recursive-simple/id2_b3_o5_true-unreach-call.c 5.0 2.1 260
recursive-simple/id2_b5_o10_true-unreach-call.c 5.0 2.1 270
recursive-simple/id2_i5_o5_true-unreach-call.c 4.9 2.1 260
recursive-simple/id_b2_o3_true-unreach-call.c 4.6 2.0 260
recursive-simple/id_b3_o5_true-unreach-call.c 4.6 1.9 260
recursive-simple/id_b5_o10_true-unreach-call.c 4.8 2.0 270
recursive-simple/id_i10_o10_true-unreach-call.c 4.2 1.7 260
recursive-simple/id_i15_o15_true-unreach-call.c 4.2 1.7 270
recursive-simple/id_i20_o20_true-unreach-call.c 5.4 2.2 270
recursive-simple/id_i25_o25_true-unreach-call.c 5.4 2.3 270
recursive-simple/id_i5_o5_true-unreach-call.c 4.8 2.0 260
recursive-simple/sum_10x0_true-unreach-call.c 5.4 2.2 280
recursive-simple/sum_15x0_true-unreach-call.c 5.8 2.3 290
recursive-simple/sum_20x0_true-unreach-call.c 6.6 2.4 320
recursive-simple/sum_25x0_true-unreach-call.c 7.2 2.5 350
recursive-simple/sum_2x3_true-unreach-call.c 4.8 2.0 260
recursive-simple/sum_non_eq_true-unreach-call.c 4.3 1.8 270
recursive-simple/sum_non_true-unreach-call.c 5.2 2.3 270
../../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 13000 12000 91000 98 1100   710   29000   98 1300   800   39000  
    correct results 75 590 290 33000 32 450   250   15000   31 610   370   16000  
        correct true 43 410 220 23000 1 0   0   0   11 0   0   0  
        correct false 32 190 73 10000 31 450   250   15000   20 610   370   16000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 118
Run set sv-comp16.Recursive