Tool ULTIMATE Taipan f7c3ed31
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-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.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 8.0 2.5 62 360 2.5 0   24    13    170   1000 9.9 5.2 210 370
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 7.1 2.1 58 340 2.5 0   4.4  2.4  78   280 7.8 4.2 150 320
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 6.9 2.2 58 350 2.5 0   3.6  2.0  63   270 7.1 3.9 160 320
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 5.4 1.8 46 310 2.5 0   4.2  2.4  65   270 7.2 3.9 130 320
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 38   10   330 1800 2.5 0   61    42    1100   2100 25   13   250 870
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 42   14   350 1700 2.6 0   98    72    2400   4800 97   70   1400 4600
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 5.9 1.8 40 340 2.5 0   4.0  2.3  72   270 7.4 3.9 130 330
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 900   200   4000 13000 2.3 0   .63 .41 7.7 39 6.1 3.3 86 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 900   210   4600 13000 2.3 0   .60 .38 5.9 40 6.2 3.3 98 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900   210   5200 13000 2.3 0   .61 .39 9.9 41 5.3 2.9 91 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 2 11   3.2 72 510 2.5 0   4.7  2.6  50   250 11   5.9 140 370
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900   780   13000 1400 2.3 0   .49 .33 12   41 5.7 3.1 110 290
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900   770   13000 1100 2.3 0   .71 .44 8.8 42 5.9 3.1 89 310
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 2 56   22   510 2100 2.5 0   3.5  2.0  75   250 24   14   260 610
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 910   280   5500 13000 2.3 0   .51 .32 12   39 6.2 3.3 110 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 2 130   80   1600 3900 2.5 0   4.6  2.6  41   250 36   20   430 1200
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 2 8.7 2.7 76 370 2.5 0   4.0  2.2  56   260 9.6 5.3 190 340
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900   760   10000 6700 2.3 0   .63 .39 13   45 5.9 3.1 110 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900   810   11000 6000 2.3 0   .55 .35 12   40 6.1 3.2 120 310
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 9.1 2.6 72 480 2.5 0   3.5  2.0  57   260 12   6.6 250 370
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900   880   9400 2500 2.3 0   .60 .37 8.8 40 5.8 3.1 110 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 910   360   6200 13000 2.3 0   .61 .37 11   40 6.0 3.2 85 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 10   3.0 77 480 2.5 0   3.4  1.9  62   260 8.3 4.5 120 340
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 900   850   11000 2600 2.5 0   .61 .39 8.1 40 5.9 3.2 100 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 5.8 1.9 45 330 2.5 0   3.4  1.9  46   270 7.4 3.9 110 320
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 5.6 1.7 42 320 2.5 0   3.4  1.9  60   270 8.6 4.7 160 340
recursive-simple/fibo_10_false-unreach-call.c 0 900   300   6500 13000 2.3 0   .48 .31 9.0 39 5.7 3.1 120 300
recursive-simple/fibo_15_false-unreach-call.c 0 910   280   6400 13000 2.3 0   .51 .35 11   39 7.3 3.9 89 310
recursive-simple/fibo_20_false-unreach-call.c 0 910   270   6300 13000 2.3 0   .54 .34 10   39 5.6 3.0 100 290
recursive-simple/fibo_25_false-unreach-call.c 0 910   280   6000 13000 2.3 0   .50 .33 8.8 41 5.9 3.1 120 300
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 900   260   6900 13000 2.3 0   .51 .33 6.4 40 6.5 3.4 130 310
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 910   240   6200 13000 2.3 0   .48 .31 8.1 41 6.2 3.2 100 300
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 900   260   5500 13000 2.3 0   .54 .35 14   40 5.9 3.1 110 290
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 910   260   6700 13000 2.3 0   .52 .34 8.4 41 7.2 3.8 120 340
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 7.6 2.2 56 380 2.5 0   3.9  2.1  61   270 7.7 4.1 160 330
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 16   5.5 140 530 2.5 0   12    6.1  120   520 11   5.5 130 420
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 18   6.7 160 560 2.5 0   20    10    140   740 33   17   450 900
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 32   12   300 860 2.6 0   41    23    520   1900 76   44   650 3700
recursive-simple/fibo_2calls_8_false-unreach-call.c 0 140   75   1500 5400 2.6 0   98    69    2000   4800 97   65   1000 5600
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 13   4.4 100 510 2.5 0   18    9.3  170   720 23   13   270 840
recursive-simple/fibo_7_false-unreach-call.c 1 25   7.8 200 920 2.6 0   62    41    540   4000 65   43   700 4100
recursive-simple/id2_b3_o2_false-unreach-call.c 1 7.6 2.2 61 350 2.5 0   5.6  3.0  76   290 9.4 5.0 110 320
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 11   3.6 88 480 2.5 0   5.9  3.2  110   280 9.0 4.7 150 330
recursive-simple/id_b3_o2_false-unreach-call.c 1 7.6 2.4 62 360 2.5 0   5.5  3.0  74   290 7.4 4.0 120 320
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 26   14   270 740 2.9 0   8.3  4.4  130   410 7.1 3.8 120 310
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 70   50   940 1200 2.5 0   12    6.3  98   460 7.8 4.1 140 320
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 190   150   2600 1100 2.5 0   14    7.5  260   510 8.8 4.6 140 330
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 430   360   5600 1100 2.5 0   16    8.1  150   670 7.9 4.2 120 330
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 11   3.7 92 490 2.5 0   7.0  3.8  51   290 7.5 4.0 130 310
recursive-simple/id_o1000_false-unreach-call.c 0 900   780   12000 1200 2.3 0   .55 .35 10   40 6.3 3.3 120 300
recursive-simple/id_o100_false-unreach-call.c 0 900   770   14000 1300 2.3 0   .47 .30 6.6 40 6.1 3.3 120 300
recursive-simple/id_o10_false-unreach-call.c 1 23   11   250 820 2.5 0   12    6.0  120   510 8.5 4.4 160 330
recursive-simple/id_o200_false-unreach-call.c 0 900   770   14000 1200 2.3 0   .48 .31 9.6 39 6.5 3.4 120 310
recursive-simple/id_o20_false-unreach-call.c 1 160   130   2100 1300 2.5 0   27    15    380   1400 8.2 4.3 130 330
recursive-simple/id_o3_false-unreach-call.c 1 7.9 2.5 62 370 2.5 0   5.5  2.9  67   290 7.4 4.0 140 310
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 27   13   270 840 2.5 0   7.6  4.1  78   300 6.8 3.7 130 310
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 67   47   750 1100 2.5 0   10    5.4  97   460 8.0 4.2 110 320
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 180   150   2500 1400 2.5 0   9.5  5.0  110   460 7.0 3.8 110 310
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 420   360   6000 1400 2.5 0   11    5.7  110   500 8.3 4.4 140 330
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 7.8 2.3 62 370 2.5 0   4.0  2.2  70   280 7.2 3.9 150 320
recursive-simple/sum_non_eq_false-unreach-call.c 1 5.3 1.7 40 310 2.5 0   3.8  2.1  60   270 7.5 3.9 140 320
recursive-simple/sum_non_false-unreach-call_true-termination.c 1 5.6 1.8 47 320 2.5 0   3.6  2.0  28   280 8.9 4.6 160 330
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 5.9 1.9 45 330 2.5 0   4.2  2.4  51   260 7.8 4.2 90 330
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 6.1 2.0 49 340 2.5 0   4.2  2.4  48   260 7.7 4.1 150 320
recursive-simple/fibo_10_true-unreach-call.c 0 900   290   5600 13000 2.3 0   .71 .45 7.3 40 6.2 3.2 110 300
recursive-simple/fibo_15_true-unreach-call.c 0 910   270   5800 13000 2.3 0   .60 .38 9.1 39 5.9 3.2 91 310
recursive-simple/fibo_20_true-unreach-call.c 0 910   270   6700 13000 2.3 0   .63 .40 7.3 39 6.4 3.3 94 310
recursive-simple/fibo_25_true-unreach-call.c 0 910   270   6000 13000 2.3 0   .53 .32 10   40 6.1 3.2 110 300
recursive-simple/fibo_2calls_10_true-unreach-call.c 0 900   250   5700 13000 2.3 0   .51 .32 9.8 40 5.9 3.1 100 300
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 910   250   6200 13000 2.3 0   .65 .40 7.5 40 6.6 3.5 84 300
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 900   260   5800 13000 2.3 0   .48 .31 11   39 5.8 3.1 110 300
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 900   260   6200 13000 2.3 0   .50 .32 10   41 5.9 3.1 100 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 10   2.9 76 500 2.5 0   4.4  2.5  50   260 12   6.8 230 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 18   6.3 170 680 2.5 0   3.7  2.1  74   260 20   11   260 520
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 28   10   250 700 2.5 0   3.6  2.0  71   260 24   13   320 630
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 45   17   420 1200 2.5 0   3.4  1.9  70   260 32   18   380 750
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 170   80   1500 5300 2.5 0   3.7  2.1  67   260 50   29   730 1100
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 20   7.0 180 730 2.5 0   3.6  2.0  64   250 17   9.6 320 510
recursive-simple/fibo_7_true-unreach-call.c 2 42   15   400 1300 2.5 0   3.6  2.0  62   260 21   12   220 660
recursive-simple/id2_b2_o3_true-unreach-call.c 2 7.1 2.1 50 340 2.5 0   4.2  2.3  52   260 8.5 4.6 120 330
recursive-simple/id2_b3_o5_true-unreach-call.c 2 7.6 2.2 59 350 2.5 0   3.5  2.0  76   260 8.3 4.5 170 320
recursive-simple/id2_b5_o10_true-unreach-call.c 2 8.0 2.2 62 340 2.5 0   3.6  2.0  78   250 8.7 4.7 160 320
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 14   5.2 110 540 2.5 0   3.4  1.9  66   250 14   7.8 210 470
recursive-simple/id_b2_o3_true-unreach-call.c 2 9.6 3.1 76 470 2.5 0   4.3  2.4  45   260 8.3 4.5 150 320
recursive-simple/id_b3_o5_true-unreach-call.c 2 9.3 2.8 76 420 2.5 0   4.0  2.2  56   260 8.2 4.5 150 330
recursive-simple/id_b5_o10_true-unreach-call.c 2 9.8 3.0 75 470 2.5 0   3.9  2.2  57   260 8.5 4.6 170 350
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 28   14   300 730 2.5 0   4.2  2.3  45   260 18   10   310 560
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 70   50   810 1400 2.5 0   4.0  2.2  54   250 22   13   220 620
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 180   150   2200 1100 2.5 0   4.5  2.5  46   260 33   19   390 710
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 430   360   5800 1100 2.5 0   4.5  2.5  45   260 38   22   390 800
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 12   4.0 96 490 2.5 0   3.4  1.9  77   260 13   6.9 230 390
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 36   21   410 830 2.5 0   4.6  2.6  49   250 19   11   310 580
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 95   70   1100 1400 2.5 0   4.0  2.3  44   260 27   15   400 650
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 230   190   3000 1200 2.5 0   4.4  2.5  47   260 38   22   380 800
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 530   440   6900 1400 2.5 0   3.9  2.2  55   260 49   29   640 950
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 12   3.4 95 570 2.5 0   3.7  2.1  49   260 11   6.2 200 400
recursive-simple/sum_non_eq_true-unreach-call.c 2 8.6 2.5 68 370 2.9 0   3.5  2.0  62   260 8.9 4.9 120 330
recursive-simple/sum_non_true-unreach-call_true-termination.c 2 8.5 2.6 66 390 2.5 0   4.2  2.3  53   260 9.9 5.4 150 350
../../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 100 31000 16000 280000 370000 240   0   98 630 390 9700 31000   98 700 420 9800 33000   98 150 82 2100 9500   98 760 430 11000 24000  
    correct results 66 100 4100 2900 50000 55000 170   0   32 430 250 5300 21000   32 440 240 6100 19000   3 130 75 2000 8700   34 640 360 9000 18000  
        correct true 34 68 2300 1600 27000 33000 86   0   3 0 0 0 0   10 0 0 0 0   3 130 75 2000 8700   34 640 360 9000 18000  
        correct false 32 32 1800 1400 23000 22000 81   0   29 430 250 5300 21000   22 440 240 6100 19000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 2 0 180 88 1900 7100 5.2 0   0 200 140 4300 9600   0 190 140 2500 10000   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 2 0 180 88 1900 7100 5.2 0   0 200 140 4300 9600   0 190 140 2500 10000   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) 100
Run set sv-comp17.ReachSafety-Recursive