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 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.Recursive
Options -sv-comp16-bam -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-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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) 7.5 2.9 380 wit false(reach) 20   11   540 false(reach) 19 10   400
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 4.7 2.0 250 wit false(reach) 5.7 3.2 350 false(reach) 13 7.6 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 3.4 1.6 220 wit false(reach) 6.3 3.5 360 false(reach) 12 10   320
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 3.8 1.7 250 wit false(reach) 4.5 2.6 230 false(reach) 13 9.5 340
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) 12   4.9 570 wit false(reach) 63   39   1300 false(reach) 42 24   980
recursive/Fibonacci05_false-unreach-call_true-termination.c witness timeout 25   13   790 wit timeout 90   73   1600 timeout 92 60   4000
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 4.5 1.9 250 wit true 6.0 3.4 260 false(reach) 11 6.5 350
recursive/Ackermann01_true-unreach-call.c true 6.1 2.5 270 wit - -
recursive/Ackermann03_true-unreach-call.c true 61   46   1300 wit - -
recursive/Ackermann04_true-unreach-call.c true 23   12   760 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 5.0 2.1 290 wit - -
recursive/Addition03_true-unreach-call.c timeout 900   850   1100 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 6.8 3.4 270 wit - -
recursive/Fibonacci01_true-unreach-call.c true 10   4.4 490 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 8.2 2.3 400 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c timeout 900   850   3700 wit - -
recursive/McCarthy91_true-unreach-call.c true 4.0 1.7 250 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 900   890   960 wit - -
recursive/Primes_true-unreach-call.c timeout 900   890   860 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 5.1 2.2 260 wit - -
recursive/gcd02_true-unreach-call.c timeout 900   890   1300 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c true 56   32   1300 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 9.9 4.4 600 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 13   6.9 450 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 3.9 1.8 230 wit false(reach) 5.8 3.3 340 false(reach) 11 6.6 350
recursive-simple/afterrec_false-unreach-call.c false(reach) 3.7 1.7 230 wit false(reach) 6.3 3.7 340 false(reach) 13 7.9 320
recursive-simple/fibo_10_false-unreach-call.c witness timeout 8.0 2.9 510 wit timeout 90   74   2000 timeout 92 53   3700
recursive-simple/fibo_15_false-unreach-call.c witness invalid (exception) 74   28   2600 wit exception 30   16   810 timeout 92 50   2900
recursive-simple/fibo_20_false-unreach-call.c timeout 900   870   3300 wit - -
recursive-simple/fibo_25_false-unreach-call.c timeout 900   830   8000 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness timeout 8.6 3.0 500 wit timeout 90   72   2200 timeout 91 54   3400
recursive-simple/fibo_2calls_15_false-unreach-call.c witness invalid (exception) 65   28   1900 wit exception 24   13   740 timeout 92 49   3200
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 900   860   3400 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 900   770   8600 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 4.6 2.0 260 wit false(reach) 5.1 3.0 220 false(reach) 13 7.2 340
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 4.2 1.8 250 wit false(reach) 17   9.1 540 false(reach) 21 12   460
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 4.5 1.8 270 wit false(reach) 31   16   850 false(reach) 61 33   1100
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) 5.8 2.3 280 wit false(reach) 55   31   1400 false(reach) 75 42   2100
recursive-simple/fibo_2calls_8_false-unreach-call.c witness timeout 7.9 2.8 400 wit timeout 91   71   2100 timeout 91 57   3000
recursive-simple/fibo_5_false-unreach-call.c false(reach) 5.0 2.1 260 wit false(reach) 31   16   740 false(reach) 44 27   1200
recursive-simple/fibo_7_false-unreach-call.c false(reach) 5.9 2.2 280 wit false(reach) 85   59   2000 timeout 92 59   2900
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 4.2 1.8 250 wit false(reach) 7.1 4.0 360 false(reach) 11 6.6 320
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 3.9 1.7 250 wit false(reach) 6.9 3.9 360 false(reach) 13 7.4 330
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 3.9 1.7 250 wit false(reach) 6.7 3.8 350 false(reach) 13 9.7 330
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 4.2 1.8 260 wit false(reach) 7.9 4.4 380 true 13 9.9 340
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 4.3 1.8 260 wit false(reach) 7.6 4.3 400 true 14 7.8 350
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 5.4 2.2 260 wit false(reach) 10   5.7 440 true 13 7.8 370
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) 5.5 2.2 270 wit false(reach) 11   6.1 480 true 15 8.6 390
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 4.6 2.0 250 wit false(reach) 7.0 4.0 360 false(reach) 13 7.6 340
recursive-simple/id_o1000_false-unreach-call.c witness invalid (exception) 440   370   4200 wit exception 15   8.2 480 true 44 26   1600
recursive-simple/id_o100_false-unreach-call.c false(reach) 13   3.7 620 wit false(reach) 38   22   1200 true 22 12   570
recursive-simple/id_o10_false-unreach-call.c false(reach) 4.2 1.8 260 wit false(reach) 7.0 3.9 370 true 13 7.7 360
recursive-simple/id_o200_false-unreach-call.c witness timeout 21   6.6 950 wit timeout 92   74   1600 true 27 14   680
recursive-simple/id_o20_false-unreach-call.c false(reach) 6.1 2.4 280 wit false(reach) 9.2 5.1 440 true 15 8.9 370
recursive-simple/id_o3_false-unreach-call.c false(reach) 4.5 2.0 250 wit false(reach) 6.4 3.7 340 false(reach) 14 7.9 350
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 4.1 1.7 250 wit false(reach) 8.4 4.7 380 true 13 7.5 350
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 4.5 1.8 260 wit false(reach) 9.3 5.2 410 true 14 8.2 370
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 5.4 2.2 260 wit false(reach) 10   5.7 430 true 17 9.3 390
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 5.6 2.3 270 wit false(reach) 12   6.3 470 true 15 11   380
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 4.4 2.0 250 wit false(reach) 5.9 3.4 350 false(reach) 14 7.3 350
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 3.6 1.6 240 wit false(reach) 4.1 2.4 220 false(reach) 12 7.4 330
recursive-simple/sum_non_false-unreach-call.c false(reach) 4.1 1.8 240 wit false(reach) 4.2 2.5 230 false(reach) 11 6.7 330
recursive-simple/afterrec_2calls_true-unreach-call.c true 3.2 1.5 220 wit - -
recursive-simple/afterrec_true-unreach-call.c true 3.1 1.5 230 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 8.5 2.6 510 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 35   25   3600 wit - -
recursive-simple/fibo_20_true-unreach-call.c timeout 900   850   3600 wit - -
recursive-simple/fibo_25_true-unreach-call.c timeout 900   810   5100 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 12   3.4 670 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 51   37   3600 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 900   840   3700 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 900   810   5100 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 3.7 1.6 240 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true 4.7 2.0 250 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true 5.1 2.1 260 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true 4.9 1.9 270 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 7.3 2.3 370 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 4.0 1.7 240 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 5.9 2.2 280 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 4.6 1.9 250 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 4.6 1.9 240 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 4.1 1.7 240 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true 3.8 1.6 240 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 3.7 1.5 240 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 4.4 1.9 240 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 4.5 1.9 240 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 4.4 1.9 250 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 4.6 2.0 240 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 4.2 1.8 250 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 5.3 2.2 250 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 4.4 1.9 240 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 4.9 2.0 260 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true 4.8 1.9 280 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true 5.5 1.9 300 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 5.7 2.0 310 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true 4.4 1.9 240 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true 4.6 2.0 240 wit - -
recursive-simple/sum_non_true-unreach-call.c true 4.8 2.1 260 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 13000 12000 92000 98 1000   710   29000   98 1300   780   41000  
    correct results 77 610 310 31000 33 520   300   17000   32 700   420   18000  
        correct true 44 440 240 22000 1 0   0   0   11 0   0   0  
        correct false 33 170 69 9200 32 520   300   17000   21 700   420   18000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 121
Run set sv-comp16.Recursive