Tool CPAchecker 1.6.1-svn 23987
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic]
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 26 280 .0041 0      .50 .33 9.3 39 5.8 3.1 93 290
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 3.0 1.3 29 280 .0041 0      .52 .33 13   42 7.1 3.7 140 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 26 270 .0041 0      .50 .33 5.9 39 7.1 3.7 130 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 3.0 1.3 26 280 .0041 0      .50 .33 8.9 41 6.0 3.2 110 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 22 270 .0041 .020  .52 .35 11   39 5.9 3.1 100 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 26 270 .0041 0      .50 .33 8.1 40 5.5 3.0 100 290
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 26 280 .0041 0      .65 .42 9.2 44 6.5 3.4 120 290
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 2.9 1.2 26 280 .0041 .0082 .62 .39 9.8 40 5.8 3.1 86 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 2.8 1.2 23 270 .0041 .0041 .50 .33 12   42 5.5 3.0 110 290
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 2.9 1.2 27 280 .0041 0      .68 .45 7.2 40 6.0 3.2 110 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.3 26 280 .0041 0      .60 .38 11   44 6.6 3.5 91 290
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 24 270 .0041 0      .63 .41 8.3 40 6.7 3.5 85 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 25 270 .0041 .025  .65 .41 9.4 43 5.8 3.0 87 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 3.1 1.3 26 280 .0041 0      .50 .32 11   41 6.3 3.3 110 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 25 280 .0041 .0082 .67 .41 8.3 39 6.5 3.4 130 310
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 22 270 .0041 0      .58 .37 10   39 6.5 3.4 140 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 27 280 .0041 2.3    .61 .40 8.1 39 5.9 3.1 98 290
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 26 280 .0041 0      .53 .35 13   40 7.0 3.7 73 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 3.4 1.3 26 280 .0082 .025  .50 .33 11   39 5.5 3.0 110 290
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 24 270 .0041 0      .65 .41 9.1 40 6.0 3.2 120 290
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 3.1 1.3 24 280 .0041 0      .56 .37 11   41 5.8 3.1 110 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 24 280 .0041 0      .50 .32 9.0 40 5.9 3.1 93 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 2.9 1.2 26 280 .0041 0      .50 .32 11   40 6.0 3.2 130 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 2.8 1.2 26 270 .0041 0      .60 .38 8.0 39 6.4 3.4 120 310
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 0 2.8 1.2 27 280 .0041 0      .49 .32 7.1 40 6.2 3.3 140 300
recursive-simple/afterrec_false-unreach-call_true-termination.c 0 2.9 1.2 26 280 .0041 0      .51 .33 5.9 40 5.8 3.1 110 300
recursive-simple/fibo_10_false-unreach-call.c 0 2.9 1.3 27 270 .0041 0      .49 .32 9.2 41 5.9 3.2 120 300
recursive-simple/fibo_15_false-unreach-call.c 0 2.7 1.2 24 270 .0041 0      .49 .31 11   39 6.3 3.3 110 300
recursive-simple/fibo_20_false-unreach-call.c 0 2.8 1.2 28 270 .0041 0      .49 .33 9.9 41 5.4 2.9 110 290
recursive-simple/fibo_25_false-unreach-call.c 0 3.1 1.3 26 280 .0041 0      .52 .38 12   39 6.9 3.6 86 290
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 2.9 1.2 26 280 .0041 0      .50 .34 6.9 40 6.0 3.2 110 290
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 3.0 1.3 29 280 .0041 0      .48 .32 9.2 40 6.2 3.3 130 300
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 2.9 1.2 29 270 .0041 0      .50 .32 10   40 5.5 3.0 77 290
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 3.0 1.2 26 270 .0041 0      .50 .34 9.6 40 5.6 3.0 95 290
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 3.2 1.4 29 280 .0041 0      3.8  2.1  85   270 8.2 4.3 170 320
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 0 3.1 1.3 25 280 .0041 0      .50 .33 4.5 39 5.9 3.1 110 290
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 0 3.2 1.2 29 270 .0041 0      .47 .32 6.6 39 6.0 3.2 110 300
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 0 2.9 1.3 26 270 .0041 0      .49 .30 3.9 39 6.6 3.4 120 310
recursive-simple/fibo_2calls_8_false-unreach-call.c 0 2.8 1.2 24 280 .0041 0      .55 .36 5.8 41 7.2 3.8 130 330
recursive-simple/fibo_5_false-unreach-call_true-termination.c 0 2.9 1.2 24 280 .0041 0      .55 .35 10   40 5.5 3.0 98 300
recursive-simple/fibo_7_false-unreach-call.c 0 2.8 1.2 23 280 .0041 0      .54 .35 13   40 5.7 3.0 120 290
recursive-simple/id2_b3_o2_false-unreach-call.c 0 2.8 1.2 25 270 .0041 0      .60 .37 5.3 39 5.8 3.1 110 290
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 0 2.9 1.2 27 280 .0041 0      .49 .32 5.7 40 6.2 3.3 110 300
recursive-simple/id_b3_o2_false-unreach-call.c 0 2.8 1.2 22 270 .0041 0      .52 .34 8.9 42 5.9 3.1 120 290
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 0 3.0 1.2 25 270 .0041 0      .54 .33 9.7 40 6.3 3.3 110 320
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 0 2.7 1.2 24 270 .0041 0      .50 .33 4.4 40 6.1 3.2 120 300
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 0 2.7 1.2 22 270 .0041 0      .52 .33 11   40 6.2 3.3 110 300
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 0 2.7 1.2 25 280 .0041 0      .49 .31 12   39 5.8 3.1 110 300
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 0 2.8 1.2 26 270 .0041 0      .53 .34 6.5 41 6.1 3.2 120 310
recursive-simple/id_o1000_false-unreach-call.c 0 2.8 1.3 23 280 .0041 0      .46 .31 7.5 39 5.3 2.9 96 290
recursive-simple/id_o100_false-unreach-call.c 0 2.8 1.2 24 280 .0041 0      .48 .32 9.2 41 6.3 3.3 140 300
recursive-simple/id_o10_false-unreach-call.c 0 2.7 1.2 23 270 .0041 0      .55 .35 12   40 6.9 3.6 140 310
recursive-simple/id_o200_false-unreach-call.c 0 2.9 1.2 24 280 .0041 5.6    .61 .39 17   44 6.6 3.5 110 310
recursive-simple/id_o20_false-unreach-call.c 0 2.9 1.2 25 270 .0041 0      .50 .31 9.2 40 6.8 3.5 120 320
recursive-simple/id_o3_false-unreach-call.c 0 2.9 1.2 25 270 .0041 0      .48 .31 13   39 5.9 3.1 120 300
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 0 2.8 1.2 24 270 .0041 0      .50 .33 13   41 5.9 3.1 87 290
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 0 2.8 1.2 24 270 .0041 0      .50 .33 12   40 5.2 2.8 100 290
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 0 2.9 1.2 23 270 .0041 0      .48 .31 7.0 40 6.0 3.2 120 300
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 0 2.8 1.2 27 270 .0041 0      .55 .36 14   41 6.4 3.4 120 300
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 0 2.9 1.2 29 270 .0041 0      .50 .33 6.2 41 6.2 3.2 120 310
recursive-simple/sum_non_eq_false-unreach-call.c 0 2.8 1.2 27 280 .0041 .025  .48 .32 10   40 6.3 3.3 120 300
recursive-simple/sum_non_false-unreach-call_true-termination.c 0 2.9 1.2 24 280 .0041 0      .48 .31 4.6 39 5.9 3.2 120 300
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 2.7 1.1 23 280 0      0      4.0  2.2  49   250 7.6 4.1 140 310
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 2.5 1.1 23 260 0      0      4.2  2.3  49   260 8.0 4.3 110 360
recursive-simple/fibo_10_true-unreach-call.c 0 2.9 1.2 25 270 .0041 0      .58 .37 9.6 39 6.2 3.3 130 290
recursive-simple/fibo_15_true-unreach-call.c 0 2.9 1.2 27 270 .0041 0      .67 .44 8.3 42 7.0 3.6 130 310
recursive-simple/fibo_20_true-unreach-call.c 0 3.0 1.3 25 280 .0041 0      .51 .33 9.0 41 6.1 3.2 110 300
recursive-simple/fibo_25_true-unreach-call.c 0 2.9 1.3 25 270 .0041 .025  .51 .33 11   41 5.3 2.9 110 300
recursive-simple/fibo_2calls_10_true-unreach-call.c 0 3.1 1.3 24 270 .0041 0      .60 .38 7.0 41 5.9 3.1 95 300
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 3.0 1.2 28 280 .0041 0      .61 .39 6.7 39 6.7 3.5 110 300
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 3.2 1.4 26 280 .0041 0      .59 .38 9.7 40 6.5 3.4 120 300
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 3.0 1.3 27 280 .0041 0      .55 .36 12   43 6.0 3.2 110 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 2.8 1.2 25 260 0      0      3.6  2.0  72   260 14   7.6 160 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 0 2.9 1.2 26 280 .0041 0      .51 .33 12   39 5.8 3.1 110 300
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 0 3.0 1.3 28 280 .0041 .020  .59 .37 9.4 43 6.2 3.3 100 310
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 0 3.0 1.4 28 280 .0041 5.8    .61 .39 11   45 7.4 3.9 77 290
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 0 3.0 1.3 27 270 .0041 0      .52 .33 13   42 6.5 3.4 130 310
recursive-simple/fibo_5_true-unreach-call_true-termination.c 0 2.9 1.2 23 280 .0041 0      .68 .42 8.5 41 5.9 3.1 110 300
recursive-simple/fibo_7_true-unreach-call.c 0 2.9 1.2 24 280 .0041 0      .62 .40 8.3 41 5.4 2.9 79 300
recursive-simple/id2_b2_o3_true-unreach-call.c 2 2.9 1.2 26 270 0      0      4.2  2.3  57   260 11   5.7 160 320
recursive-simple/id2_b3_o5_true-unreach-call.c 2 2.8 1.2 27 270 0      0      4.5  2.5  49   260 9.1 4.9 180 330
recursive-simple/id2_b5_o10_true-unreach-call.c 2 2.8 1.2 26 270 0      0      4.1  2.3  53   250 8.8 4.7 140 320
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 0 2.8 1.2 24 270 .0041 0      .62 .39 9.5 42 6.3 3.3 110 310
recursive-simple/id_b2_o3_true-unreach-call.c 2 2.7 1.2 23 270 0      0      4.2  2.4  39   260 8.6 4.7 140 340
recursive-simple/id_b3_o5_true-unreach-call.c 2 2.6 1.2 26 270 0      0      4.3  2.4  47   260 9.1 4.9 160 320
recursive-simple/id_b5_o10_true-unreach-call.c 2 2.7 1.2 26 270 0      0      4.5  2.5  45   260 9.2 4.9 180 350
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 0 2.8 1.2 25 280 .0041 .020  .51 .32 9.3 40 6.0 3.2 110 300
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 0 2.8 1.2 25 280 .0041 0      .61 .39 8.7 40 7.0 3.6 91 300
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 0 2.8 1.2 29 280 .0041 0      .57 .36 10   40 5.5 3.0 120 290
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 0 2.6 1.2 24 270 .0041 0      .57 .37 7.7 40 5.8 3.1 120 300
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 0 2.8 1.2 24 270 .0041 0      .61 .38 8.0 39 6.2 3.3 110 300
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 0 2.8 1.2 24 270 .0041 0      .54 .36 9.8 40 6.4 3.3 130 310
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 0 2.9 1.2 24 270 .0041 0      .56 .36 8.8 41 5.4 2.9 86 290
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 0 2.8 1.2 24 280 .0041 2.3    .50 .32 12   40 7.2 3.8 79 300
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 0 2.9 1.2 24 280 .0041 0      .61 .40 7.3 40 7.3 3.9 74 300
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 0 2.8 1.2 25 280 .0041 0      .53 .34 9.5 39 6.0 3.2 110 300
recursive-simple/sum_non_eq_true-unreach-call.c 0 3.0 1.3 26 290 .0041 5.8    .59 .38 13   43 5.9 3.1 120 310
recursive-simple/sum_non_true-unreach-call_true-termination.c 0 2.8 1.2 26 280 .0041 0      .50 .32 11   40 6.5 3.4 130 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 98 19 280   120   2500 27000 .37   22   98 26   17   480 2000   98 280   150   5100 14000   98 63 37 890 4100   98 360 190 6100 16000  
    correct results 10 19 28   12   260 2700 .0041 0   1 3.8 2.1 85 270   1 8.2 4.3 170 320   3 37 21 460 2300   9 85 46 1400 3000  
        correct true 9 18 24   11   230 2400 0      0   0 0   0   0 0   0 0   0   0 0   3 37 21 460 2300   9 85 46 1400 3000  
        correct false 1 1 3.2 1.4 29 280 .0041 0   1 3.8 2.1 85 270   1 8.2 4.3 170 320   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 19
Run set sv-comp17.ReachSafety-Recursive