Tool CPAchecker 1.4-svn 18373
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 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.Recursive
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -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-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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 error (recursion) 3.5 1.7 210 wit - -
recursive/Addition02_false-unreach-call_false-termination.c error (recursion) 3.6 1.7 200 wit - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 4.4 2.0 240 wit false(reach) 6.6 3.7 350 false(reach) 10   5.4 330
recursive/EvenOdd03_false-unreach-call_false-termination.c error (recursion) 3.6 1.6 210 wit - -
recursive/Fibonacci04_false-unreach-call_true-termination.c error (recursion) 3.6 1.6 210 wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c error (recursion) 3.5 1.6 210 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c error (recursion) 3.5 1.6 200 wit - -
recursive/Ackermann01_true-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive/Ackermann03_true-unreach-call.c error (recursion) 3.1 1.4 210 wit - -
recursive/Ackermann04_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive/Addition01_true-unreach-call_true-termination.c error (recursion) 3.7 1.7 210 wit - -
recursive/Addition03_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c error (recursion) 3.6 1.6 210 wit - -
recursive/Fibonacci01_true-unreach-call.c error (recursion) 3.5 1.5 210 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c error (recursion) 3.5 1.6 210 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c error (recursion) 3.6 1.7 210 wit - -
recursive/McCarthy91_true-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c error (recursion) 3.5 1.7 210 wit - -
recursive/Primes_true-unreach-call.c error (recursion) 3.8 1.7 210 wit - -
recursive/gcd01_true-unreach-call_true-termination.c error (recursion) 3.6 1.7 210 wit - -
recursive/gcd02_true-unreach-call.c error (recursion) 3.8 1.7 220 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c error (recursion) 3.6 1.7 210 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c error (recursion) 3.5 1.6 210 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c error (recursion) 3.5 1.6 220 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 3.9 1.8 230 wit false(reach) 5.8 3.3 360 false(reach) 9.3 5.2 320
recursive-simple/afterrec_false-unreach-call.c false(reach) 3.7 1.7 230 wit false(reach) 6.2 3.6 340 false(reach) 13   7.3 340
recursive-simple/fibo_10_false-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/fibo_15_false-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/fibo_20_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/fibo_25_false-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_2calls_15_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/fibo_2calls_20_false-unreach-call.c error (recursion) 3.0 1.4 200 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c error (recursion) 3.6 1.6 220 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 4.2 1.9 230 wit false(reach) 4.7 2.7 230 false(reach) 13   7.2 350
recursive-simple/fibo_2calls_4_false-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/fibo_2calls_5_false-unreach-call.c error (recursion) 3.4 1.6 200 wit - -
recursive-simple/fibo_2calls_6_false-unreach-call.c error (recursion) 3.5 1.5 210 wit - -
recursive-simple/fibo_2calls_8_false-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive-simple/fibo_5_false-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_7_false-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/id2_b3_o2_false-unreach-call.c error (recursion) 3.5 1.5 210 wit - -
recursive-simple/id2_i5_o5_false-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/id_b3_o2_false-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive-simple/id_i10_o10_false-unreach-call.c error (recursion) 3.4 1.6 200 wit - -
recursive-simple/id_i15_o15_false-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/id_i20_o20_false-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/id_i25_o25_false-unreach-call.c error (recursion) 3.2 1.5 210 wit - -
recursive-simple/id_i5_o5_false-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/id_o1000_false-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/id_o100_false-unreach-call.c error (recursion) 3.4 1.6 200 wit - -
recursive-simple/id_o10_false-unreach-call.c error (recursion) 2.8 1.3 200 wit - -
recursive-simple/id_o200_false-unreach-call.c error (recursion) 3.6 1.6 200 wit - -
recursive-simple/id_o20_false-unreach-call.c error (recursion) 3.4 1.6 200 wit - -
recursive-simple/id_o3_false-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/sum_10x0_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/sum_15x0_false-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/sum_20x0_false-unreach-call.c error (recursion) 3.3 1.6 210 wit - -
recursive-simple/sum_25x0_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/sum_2x3_false-unreach-call.c error (recursion) 2.9 1.4 200 wit - -
recursive-simple/sum_non_eq_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/sum_non_false-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/afterrec_2calls_true-unreach-call.c true 3.7 1.7 210 wit - -
recursive-simple/afterrec_true-unreach-call.c true 3.5 1.7 200 wit - -
recursive-simple/fibo_10_true-unreach-call.c error (recursion) 3.0 1.3 210 wit - -
recursive-simple/fibo_15_true-unreach-call.c error (recursion) 3.5 1.7 210 wit - -
recursive-simple/fibo_20_true-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/fibo_25_true-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c error (recursion) 3.5 1.6 220 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c error (recursion) 3.7 1.7 210 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 3.7 1.6 210 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c error (recursion) 3.6 1.7 200 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_5_true-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/fibo_7_true-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c error (recursion) 3.5 1.7 210 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c error (recursion) 3.5 1.6 200 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c error (recursion) 3.3 1.6 210 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c error (recursion) 3.6 1.6 210 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c error (recursion) 3.4 1.6 210 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c error (recursion) 2.9 1.4 200 wit - -
recursive-simple/sum_10x0_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/sum_15x0_true-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/sum_20x0_true-unreach-call.c error (recursion) 3.5 1.6 210 wit - -
recursive-simple/sum_25x0_true-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/sum_2x3_true-unreach-call.c error (recursion) 3.0 1.4 210 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c error (recursion) 2.9 1.4 210 wit - -
recursive-simple/sum_non_true-unreach-call.c error (recursion) 3.4 1.6 210 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 340 160   20000 98 23   13   1300   98 45   25   1300  
    correct results 7 27 12   1500 4 23   13   1300   4 45   25   1300  
        correct true 3 11 5.0 620 0 0   0   0   0 0   0   0  
        correct false 4 16 7.4 930 4 23   13   1300   4 45   25   1300  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 10
Run set sv-comp16.Recursive