Tool SMACK+Corral 1.7.2
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS 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-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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 1 1.6 1.6 20 75 .86 0      4.7  2.6  87   290 9.0 4.8 93 320
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 1.6 1.6 20 78 .86 0      5.2  2.9  87   300 9.4 5.0 75 320
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 1.5 1.6 21 76 .85 0      3.4  1.9  50   270 7.9 4.3 130 320
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 1.5 1.5 18 74 .86 0      4.4  2.4  83   280 7.4 4.0 160 320
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 1.6 1.6 22 72 .84 0      4.5  2.5  70   290 7.5 4.0 60 330
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 1 2.0 2.0 25 82 .84 0      4.7  2.6  84   300 7.5 4.0 97 320
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 1.5 1.5 19 70 .84 0      3.7  2.1  52   280 6.8 3.6 110 320
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 2 880   880   8200 500 .86 0      3.6  2.0  73   260 12   7.1 170 410
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 2 1.4 1.4 18 72 .86 0      4.2  2.3  52   260 33   19   500 720
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 2 880   880   8500 390 .86 0      3.5  1.9  57   250 26   15   390 620
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 2 880   880   11000 380 .86 0      4.4  2.5  45   280 11   6.0 210 380
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 2 880   880   11000 400 .86 16      3.8  2.1  69   260 380   280   6200 4600
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 1 880   880   10000 150 .86 0      3.7  2.1  67   260 960   810   18000 2300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 2 890   880   8900 10000 .84 0      3.4  1.9  54   260 31   18   340 710
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 1.7 1.7 23 78 .83 0      3.7  2.1  65   260 39   22   550 1400
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 440   430   4500 15000 .84 0      .62 .40 6.9 39 6.8 3.6 89 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 880   880   9000 400 .84 16      3.9  2.2  58   260 11   5.7 180 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 1 880   880   11000 110 .86 0      4.0  2.2  64   260 960   840   22000 2300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 1 880   880   9400 260 .91 0      4.2  2.3  62   260 960   840   20000 1800
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 880   880   12000 370 .87 0      3.6  2.0  64   260 11   6.3 230 400
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 1 880   880   11000 83 .88 0      4.7  2.6  42   260 960   810   17000 1900
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 1 890   880   8000 6800 .86 0      3.7  2.1  74   260 460   370   8500 7000
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 1.7 1.7 22 66 .84 0      3.7  2.0  48   260 8.8 4.7 110 330
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 1 1.9 1.9 27 70 .84 0      3.3  1.8  35   260 960   950   25000 2500
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 1.5 1.5 21 77 .83 0      3.6  2.0  40   280 6.8 3.7 110 310
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 1.5 1.5 17 73 .82 0      3.2  1.8  53   270 8.9 4.8 56 310
recursive-simple/fibo_10_false-unreach-call.c 1 3.1 2.9 46 91 .83 0      8.3  4.4  130   440 7.1 3.9 83 320
recursive-simple/fibo_15_false-unreach-call.c 1 110   110   960 570 .83 0      42    31    650   2100 7.2 3.8 97 320
recursive-simple/fibo_20_false-unreach-call.c 0 890   880   7800 2800 .84 2.2    .50 .33 7.0 43 5.8 3.1 94 300
recursive-simple/fibo_25_false-unreach-call.c 0 890   880   10000 2900 .84 2.2    .56 .36 8.7 43 6.3 3.3 83 310
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 3.1 2.9 38 92 .84 0      8.0  4.3  110   450 7.6 4.1 160 320
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 110   110   1000 570 .84 0      41    30    890   2000 7.5 4.1 110 310
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 890   930   8100 2700 .84 0      .49 .34 3.9 39 6.6 3.4 60 330
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 900   930   11000 2900 .84 0      .50 .35 6.4 43 5.8 3.1 100 300
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 1.5 1.5 20 69 .84 0      4.2  2.3  75   280 7.9 4.2 87 330
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 1.6 1.6 21 72 .84 0      4.5  2.5  100   270 7.7 4.1 110 320
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 1.6 1.6 22 74 .84 0      4.7  2.6  91   270 8.2 4.3 83 320
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 1.7 1.7 20 81 .84 0      4.9  2.7  73   280 7.3 3.9 94 320
recursive-simple/fibo_2calls_8_false-unreach-call.c 1 2.0 1.9 27 89 .84 0      6.4  3.5  120   300 7.4 3.9 88 320
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 1.6 1.6 19 69 .83 0      4.6  2.5  99   280 6.9 3.7 73 320
recursive-simple/fibo_7_false-unreach-call.c 1 1.7 1.6 25 72 .83 0      5.3  2.9  110   290 8.1 4.3 150 340
recursive-simple/id2_b3_o2_false-unreach-call.c 1 1.5 1.6 20 77 .84 0      4.6  2.5  78   290 8.3 4.4 62 360
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 1.6 1.6 18 77 .83 0      4.0  2.2  59   280 7.0 3.8 110 320
recursive-simple/id_b3_o2_false-unreach-call.c 1 1.5 1.6 20 78 .84 .12   4.5  2.5  95   280 8.7 4.7 110 340
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 1.6 1.6 20 73 .83 0      4.3  2.4  65   280 6.7 3.6 72 320
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 1.6 1.7 22 69 .83 0      4.5  2.6  78   280 7.3 3.9 110 320
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 1.7 1.7 23 77 .83 0      4.7  2.6  100   280 7.6 4.0 130 330
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 1.9 1.9 21 75 .83 .25   4.9  2.7  100   280 7.3 3.9 66 330
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 1.5 1.6 20 78 .83 0      4.8  2.7  36   270 7.0 3.8 57 330
recursive-simple/id_o1000_false-unreach-call.c 0 880   930   11000 220 .84 0      .53 .35 9.4 40 5.8 3.1 100 300
recursive-simple/id_o100_false-unreach-call.c 0 16   16   200 110 .84 .25   4.6  2.5  74   280 7.7 4.1 97 320
recursive-simple/id_o10_false-unreach-call.c 0 1.6 1.6 17 77 .84 0      4.7  2.6  100   290 10   5.3 87 330
recursive-simple/id_o200_false-unreach-call.c 0 160   160   2000 240 .84 0      4.3  2.4  65   280 7.6 4.1 84 330
recursive-simple/id_o20_false-unreach-call.c 0 1.8 1.8 20 74 .84 0      4.4  2.5  71   290 7.3 3.9 94 330
recursive-simple/id_o3_false-unreach-call.c 0 1.5 1.6 19 84 .84 0      4.6  2.6  79   280 7.3 4.0 110 330
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 1.5 1.5 19 75 .83 0      4.4  2.4  60   280 7.8 4.1 85 320
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 1.6 1.5 19 68 .83 0      4.6  2.6  79   290 7.6 4.0 110 330
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 1.7 1.7 22 74 .83 0      4.6  2.6  94   290 8.9 4.7 72 320
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 1.8 1.8 21 73 .83 0      4.9  2.7  85   290 7.3 3.9 83 320
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 1.5 1.5 19 74 .83 .0041 4.1  2.3  85   280 8.3 4.4 72 330
recursive-simple/sum_non_eq_false-unreach-call.c 1 1.5 1.6 23 76 .84 0      3.9  2.2  58   280 7.2 3.8 68 310
recursive-simple/sum_non_false-unreach-call_true-termination.c 1 1.5 1.6 18 70 .84 0      3.8  2.1  66   270 7.9 4.2 91 310
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 1.2 1.2 16 72 .83 0      3.4  1.9  79   250 9.9 5.2 95 320
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 1.2 1.2 15 69 .82 0      3.5  1.9  69   260 8.6 4.6 110 320
recursive-simple/fibo_10_true-unreach-call.c 2 2.2 2.1 30 93 .83 0      3.4  1.9  66   250 46   27   990 3000
recursive-simple/fibo_15_true-unreach-call.c 2 110   110   1100 590 .83 0      3.5  2.0  73   260 680   620   19000 6300
recursive-simple/fibo_20_true-unreach-call.c 1 890   880   8100 2700 .84 2.2    4.3  2.4  55   260 960   910   26000 5400
recursive-simple/fibo_25_true-unreach-call.c 1 890   880   11000 2900 .84 2.2    4.3  2.5  49   260 960   910   20000 5100
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 2.3 2.3 30 93 .84 0      3.3  1.9  58   260 89   54   2100 3900
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 66   65   550 550 .84 16      3.5  2.0  74   250 960   890   33000 5500
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 890   930   7400 2700 .84 0      .52 .34 14   40 6.2 3.3 95 300
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 890   930   10000 2900 .84 0      .63 .39 8.6 41 7.6 4.0 79 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 1.2 1.2 16 67 .84 0      3.6  2.0  77   260 16   8.5 160 420
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 1.2 1.3 17 73 .84 0      3.7  2.1  75   260 21   11   430 520
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 1.3 1.3 15 71 .84 .0041 3.8  2.2  60   260 30   16   360 590
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 1.3 1.3 15 73 .84 0      3.7  2.1  81   260 36   21   510 750
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 1.4 1.4 18 73 .84 0      3.6  2.0  74   260 58   34   1100 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 1.3 1.3 17 70 .83 0      3.6  2.1  53   260 20   11   220 520
recursive-simple/fibo_7_true-unreach-call.c 2 1.3 1.3 15 66 .83 0      3.4  2.0  70   250 23   13   290 690
recursive-simple/id2_b2_o3_true-unreach-call.c 2 1.2 1.2 15 68 .84 0      3.5  2.0  61   250 8.6 4.6 160 310
recursive-simple/id2_b3_o5_true-unreach-call.c 2 1.2 1.2 15 70 .84 0      3.6  2.0  73   270 9.8 5.3 130 320
recursive-simple/id2_b5_o10_true-unreach-call.c 2 1.2 1.2 14 67 .84 0      3.7  2.1  53   260 11   5.8 110 320
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 1.2 1.3 18 72 .83 0      3.5  1.9  72   260 13   7.5 220 430
recursive-simple/id_b2_o3_true-unreach-call.c 2 1.2 1.1 14 66 .84 0      3.3  1.8  65   250 10   5.6 130 330
recursive-simple/id_b3_o5_true-unreach-call.c 2 1.2 1.2 14 62 .84 .12   3.3  1.9  53   260 8.7 4.7 150 320
recursive-simple/id_b5_o10_true-unreach-call.c 2 1.2 1.2 16 61 .84 0      3.9  2.2  48   260 10   5.5 66 320
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 1.2 1.3 18 68 .83 0      3.4  1.9  43   260 21   11   250 540
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 1.3 1.3 16 70 .83 0      3.6  2.0  57   260 30   17   240 610
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 1.4 1.4 18 70 .83 0      3.3  1.9  57   260 32   18   550 550
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 1.5 1.5 17 68 .83 0      3.3  1.8  60   250 47   27   740 790
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 1.2 1.3 13 69 .83 0      3.4  1.9  69   260 13   7.3 190 430
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 1.2 1.3 16 68 .83 0      4.5  2.5  47   260 28   15   280 580
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 1.3 1.3 15 74 .83 0      3.9  2.2  47   250 25   15   460 700
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 1.3 1.3 18 68 .83 .25   3.5  2.0  63   260 36   21   780 700
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 1.3 1.4 16 66 .83 .25   3.8  2.2  48   250 49   29   730 930
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 1.2 1.2 15 68 .83 0      3.5  2.0  58   260 15   8.2 140 430
recursive-simple/sum_non_eq_true-unreach-call.c 2 880   880   12000 530 .84 0      3.6  2.0  76   260 9.8 5.4 170 330
recursive-simple/sum_non_true-unreach-call_true-termination.c 2 880   880   11000 260 .84 16      3.4  1.9  60   260 10   5.5 150 340
../../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 125 22000 22000 240000 66000 83   74    98 260 160 4600 15000   98 340 180 4200 14000   98 190 100 3100 13000   98 10000 8800 230000 72000  
    correct results 75 116 8400 8300 96000 20000 63   49    34 230 150 4100 13000   34 260 140 3200 11000   3 150 83 2500 11000   41 2000 1400 39000 38000  
        correct true 41 82 8100 8100 94000 16000 34   48    1 0 0 0 0   26 0 0 0 0   3 150 83 2500 11000   41 2000 1400 39000 38000  
        correct false 34 34 280 270 2700 3600 29   .37 33 230 150 4100 13000   8 260 140 3200 11000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 15 9 6400 6400 71000 14000 13   21    1 26 14 440 1700   6 48 26 610 2000   0 36 20 520 2300   0 8100 7300 190000 34000  
        correct-unconfirmed true 9 9 6300 6200 69000 14000 7.8 20    1 0 0 0 0   6 0 0 0 0   0 36 20 520 2300   0 8100 7300 190000 34000  
        correct-unconfirmed false 6 0 180 180 2300 660 5.1 .25 0 26 14 440 1700   0 48 26 610 2000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 125
Run set sv-comp17.ReachSafety-Recursive