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 false(reach) 7.5 2.9 390 wit false(reach) 20   10   530 false(reach) 18 9.9 410
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 5.3 2.3 280 wit false(reach) 6.5 3.7 350 false(reach) 14 9.1 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 5.2 2.1 360 wit false(reach) 6.6 3.8 340 false(reach) 12 7.9 330
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 4.9 2.1 270 wit false(reach) 4.5 2.6 230 false(reach) 12 6.7 330
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) 13   4.9 600 wit false(reach) 65   41   1300 false(reach) 42 23   990
recursive/Fibonacci05_false-unreach-call_true-termination.c witness timeout 23   12   790 wit timeout 90   73   1500 timeout 90 61   3000
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 4.6 2.0 270 wit true 6.2 3.5 260 false(reach) 11 6.5 330
recursive/Ackermann01_true-unreach-call.c true 6.3 2.6 290 wit - -
recursive/Ackermann03_true-unreach-call.c true 62   47   2400 wit - -
recursive/Ackermann04_true-unreach-call.c true 21   11   780 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 5.3 2.2 320 wit - -
recursive/Addition03_true-unreach-call.c timeout 900   850   1800 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 7.1 3.5 300 wit - -
recursive/Fibonacci01_true-unreach-call.c true 12   5.4 500 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 8.2 2.3 430 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c timeout 900   840   1800 wit - -
recursive/McCarthy91_true-unreach-call.c true 5.1 2.2 270 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 900   890   910 wit - -
recursive/Primes_true-unreach-call.c timeout 900   890   860 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 5.7 2.4 280 wit - -
recursive/gcd02_true-unreach-call.c timeout 900   890   1300 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c exception 7.9 3.0 340 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 9.2 4.1 620 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 11   6.3 470 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 3.0 1.4 210 wit false(reach) 6.5 3.7 340 false(reach) 12 6.7 340
recursive-simple/afterrec_false-unreach-call.c false(reach) 3.0 1.4 190 wit false(reach) 6.4 3.6 340 false(reach) 13 7.1 340
recursive-simple/fibo_10_false-unreach-call.c witness timeout 9.6 3.4 500 wit timeout 91   73   2000 timeout 92 50   2500
recursive-simple/fibo_15_false-unreach-call.c witness invalid (exception) 71   32   1900 wit exception 33   17   810 timeout 91 53   3700
recursive-simple/fibo_20_false-unreach-call.c timeout 900   870   2800 wit - -
recursive-simple/fibo_25_false-unreach-call.c timeout 900   850   7800 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness timeout 9.9 3.6 490 wit timeout 91   70   1700 timeout 92 57   3700
recursive-simple/fibo_2calls_15_false-unreach-call.c witness invalid (exception) 71   34   1800 wit exception 28   15   770 timeout 92 52   2600
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 900   870   2800 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 900   740   8700 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 3.2 1.4 210 wit false(reach) 4.7 2.8 230 false(reach) 13 7.6 330
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 5.3 2.0 370 wit false(reach) 19   10   560 false(reach) 23 13   440
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 6.3 2.4 370 wit false(reach) 34   18   790 false(reach) 52 28   840
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) 6.6 2.5 380 wit false(reach) 52   30   1500 timeout 91 53   2600
recursive-simple/fibo_2calls_8_false-unreach-call.c witness timeout 8.3 2.9 420 wit timeout 91   73   2100 timeout 91 58   3100
recursive-simple/fibo_5_false-unreach-call.c false(reach) 6.1 2.4 370 wit false(reach) 28   15   740 false(reach) 42 23   1000
recursive-simple/fibo_7_false-unreach-call.c witness timeout 6.1 2.3 390 wit timeout (false(reach)) 91   62   2000 timeout 90 63   2800
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 5.8 2.3 370 wit false(reach) 6.6 3.7 350 false(reach) 12 6.8 350
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 4.2 1.8 270 wit false(reach) 6.8 3.8 350 false(reach) 14 7.5 350
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 4.1 1.8 270 wit false(reach) 6.5 3.7 340 false(reach) 13 7.1 340
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 5.2 2.2 270 wit false(reach) 8.2 4.6 380 true 13 7.1 340
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 5.6 2.2 280 wit false(reach) 9.1 5.1 410 true 14 12   360
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 6.6 2.5 370 wit false(reach) 9.6 5.3 440 true 14 8.2 360
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) 6.6 2.5 370 wit false(reach) 13   7.1 480 true 14 12   360
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 5.2 2.2 270 wit false(reach) 7.1 4.0 350 false(reach) 14 10   340
recursive-simple/id_o1000_false-unreach-call.c witness invalid (exception) 450   380   4200 wit exception 16   8.7 480 true 43 23   1500
recursive-simple/id_o100_false-unreach-call.c false(reach) 15   4.1 640 wit false(reach) 38   22   1200 true 22 12   570
recursive-simple/id_o10_false-unreach-call.c false(reach) 4.5 1.9 280 wit false(reach) 8.1 4.7 380 true 13 7.0 350
recursive-simple/id_o200_false-unreach-call.c witness timeout 23   7.3 960 wit timeout 91   69   1900 true 25 13   680
recursive-simple/id_o20_false-unreach-call.c false(reach) 6.9 2.6 390 wit false(reach) 11   5.8 430 true 13 9.4 370
recursive-simple/id_o3_false-unreach-call.c false(reach) 4.9 2.1 270 wit false(reach) 6.5 3.8 340 false(reach) 13 8.9 350
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 4.5 1.9 280 wit false(reach) 8.0 4.5 380 true 12 6.6 360
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 5.5 2.2 280 wit false(reach) 9.7 5.4 410 true 13 7.3 370
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 6.6 2.5 370 wit false(reach) 10   5.7 440 true 15 12   370
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 7.0 2.5 380 wit false(reach) 13   6.7 490 true 14 7.9 370
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 5.0 2.1 270 wit false(reach) 6.1 3.6 350 false(reach) 13 8.5 340
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 4.1 1.7 270 wit false(reach) 4.6 2.7 220 false(reach) 11 6.8 360
recursive-simple/sum_non_false-unreach-call.c false(reach) 4.8 2.0 260 wit false(reach) 4.5 2.6 220 false(reach) 11 6.5 330
recursive-simple/afterrec_2calls_true-unreach-call.c true 3.1 1.5 190 wit - -
recursive-simple/afterrec_true-unreach-call.c true 3.0 1.3 190 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 9.6 3.0 540 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 38   26   3600 wit - -
recursive-simple/fibo_20_true-unreach-call.c timeout 900   850   3700 wit - -
recursive-simple/fibo_25_true-unreach-call.c timeout 900   820   5100 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 12   3.5 670 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 52   38   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.2 1.5 180 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true 5.1 2.1 270 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true 4.7 1.9 270 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true 5.1 2.0 290 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 8.7 2.8 380 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 5.0 2.1 260 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 6.5 2.3 300 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 4.9 2.1 270 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 5.0 2.1 260 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 5.0 2.1 270 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true 4.9 2.1 260 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 4.6 2.0 260 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 4.6 1.9 260 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 4.8 2.0 270 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 4.2 1.7 260 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 4.2 1.7 270 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 5.4 2.2 270 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 5.4 2.3 270 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 4.8 2.0 260 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 5.4 2.2 280 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true 5.8 2.3 290 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true 6.6 2.4 320 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 7.2 2.5 350 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true 4.8 2.0 260 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true 4.3 1.8 270 wit - -
recursive-simple/sum_non_true-unreach-call.c true 5.2 2.3 270 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 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