Tool VeriAbs
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 04:55:34 CET ]] [[ 2017-01-15 05:46:09 CET ]] [[ 2017-01-15 05:17:25 CET ]] [[ 2017-01-15 05:48:02 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.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/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.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 0 830   830   4500 480 .35  0      .57 .36 12   43 5.8 3.1 120 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 900   900   6700 5100 .85  0      .50 .32 3.5 40 6.3 3.3 130 310
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 5.6 2.6 45 270 .086 0      .50 .32 5.2 42 6.8 3.6 140 320
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 5.2 2.7 48 150 .25  0      .48 .33 8.4 40 5.7 3.0 120 290
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 770   760   4600 190 .34  0      .49 .32 13   39 5.1 2.7 70 290
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 770   770   3600 190 .34  0      .51 .33 11   42 5.8 3.1 100 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 540   530   2800 330 .27  .094  .54 .35 11   44 5.7 3.1 110 300
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 740   740   3600 370 .40  0      .48 .31 12   40 6.0 3.1 98 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 740   740   3900 450 .49  0      .53 .34 12   42 6.6 3.5 130 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 740   740   3800 400 .40  0      .54 .35 8.7 39 5.7 3.0 120 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900   900   7900 5000 3.8   0      .57 .37 5.6 42 6.1 3.2 130 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900   900   5900 8400 1.9   0      .48 .33 6.1 40 6.3 3.3 120 290
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 5.3 2.7 52 150 .25  0      .53 .33 9.6 40 6.0 3.2 110 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 770   770   3600 190 .37  0      .49 .32 11   39 6.3 3.3 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 7.6 2.5 63 290 .045 0      3.4  1.9  54   260 32   18   610 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 770   770   3000 190 .38  0      .50 .33 9.5 41 8.0 4.2 120 320
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 660   650   4100 330 .42  0      .51 .34 4.7 40 6.0 3.2 130 310
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 850   850   6400 2500 .70  0      .52 .32 11   39 5.3 2.9 110 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 780   770   6500 2500 1.4   0      .46 .30 6.7 40 5.8 3.1 110 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900   900   7400 6700 .72  .76   .56 .36 6.0 42 6.4 3.4 120 290
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900   900   7300 5400 1.9   0      .48 .30 4.8 39 5.4 2.9 100 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 650   650   3900 180 .45  0      .60 .39 8.8 40 6.2 3.3 110 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 4.9 2.3 42 150 .23  .094  .49 .31 6.4 39 6.1 3.2 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 4.7 2.2 38 150 .23  0      .53 .34 5.2 39 6.0 3.2 110 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 0 5.5 2.5 52 220 .086 0      .51 .33 9.8 42 6.0 3.2 120 290
recursive-simple/afterrec_false-unreach-call_true-termination.c 0 5.4 2.5 46 220 .086 0      .56 .35 13   40 5.4 2.9 110 280
recursive-simple/fibo_10_false-unreach-call.c 0 5.7 2.7 45 220 .086 .094  .54 .33 13   40 6.2 3.3 120 300
recursive-simple/fibo_15_false-unreach-call.c 0 12   9.3 140 230 .086 0      .52 .36 3.8 40 5.9 3.1 110 300
recursive-simple/fibo_20_false-unreach-call.c 0 720   720   5100 200 .36  0      .51 .33 12   41 6.0 3.2 120 300
recursive-simple/fibo_25_false-unreach-call.c 0 4.6 2.2 40 150 .23  0      .57 .36 5.3 43 6.9 3.6 140 320
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 5.7 2.7 46 220 .086 0      .51 .33 12   39 6.4 3.4 130 300
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 12   9.2 130 230 .086 0      .55 .35 5.2 43 5.8 3.1 130 300
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 720   720   6100 200 .35  0      .50 .32 10   40 6.1 3.3 120 300
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 840   840   6600 200 .35  0      .50 .33 4.9 41 6.2 3.3 100 300
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 0 5.7 2.5 49 230 .086 0      .50 .33 13   39 5.4 2.9 95 290
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 0 5.6 2.4 51 230 .086 0      .54 .34 12   39 5.9 3.1 120 300
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 0 5.5 2.5 54 230 .086 0      .53 .34 13   42 6.0 3.1 110 290
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 0 5.5 2.5 47 230 .086 0      .51 .33 11   41 5.5 2.9 92 290
recursive-simple/fibo_2calls_8_false-unreach-call.c 0 5.6 2.5 56 220 .086 0      .50 .33 11   39 6.7 3.5 120 310
recursive-simple/fibo_5_false-unreach-call_true-termination.c 0 5.5 2.5 47 230 .086 .57   .54 .35 5.9 42 6.0 3.3 120 310
recursive-simple/fibo_7_false-unreach-call.c 0 5.5 2.5 54 230 .086 0      .52 .33 12   41 5.7 3.1 130 290
recursive-simple/id2_b3_o2_false-unreach-call.c 0 6.0 2.9 56 270 .086 0      .52 .33 13   41 6.1 3.2 110 300
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 0 5.5 2.5 49 230 .086 0      .51 .32 4.7 41 6.2 3.3 130 310
recursive-simple/id_b3_o2_false-unreach-call.c 0 4.7 2.3 42 160 .23  .094  .48 .32 7.8 40 5.6 3.0 100 290
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 0 5.5 2.5 50 220 .086 0      .56 .35 11   42 6.5 3.4 120 310
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 0 5.7 2.5 51 230 .086 0      .52 .33 8.9 41 6.0 3.2 120 300
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 0 5.4 2.5 51 230 .086 0      .52 .33 12   40 6.1 3.2 130 300
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 0 4.7 2.2 39 150 .23  0      .51 .35 10   39 6.0 3.2 110 300
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 0 5.3 2.4 50 230 .086 0      .47 .31 8.0 39 5.7 3.0 94 300
recursive-simple/id_o1000_false-unreach-call.c 0 4.6 2.2 41 160 .23  0      .55 .36 12   39 6.6 3.5 130 300
recursive-simple/id_o100_false-unreach-call.c 0 4.7 2.2 40 150 .23  0      .51 .35 6.4 39 6.3 3.3 120 300
recursive-simple/id_o10_false-unreach-call.c 0 4.9 2.3 42 160 .23  0      .52 .33 12   41 6.2 3.2 120 300
recursive-simple/id_o200_false-unreach-call.c 0 4.8 2.3 49 150 .23  0      .51 .33 8.5 39 6.7 3.5 130 320
recursive-simple/id_o20_false-unreach-call.c 0 4.7 2.2 44 160 .23  0      .50 .31 4.1 40 5.5 2.9 110 280
recursive-simple/id_o3_false-unreach-call.c 0 4.6 2.2 43 160 .23  0      .56 .35 13   41 6.1 3.2 90 300
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 0 5.3 2.4 57 230 .086 0      .48 .31 9.9 39 5.7 3.0 110 300
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 0 5.4 2.5 44 230 .086 0      .51 .35 5.1 40 5.6 3.0 120 290
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 0 5.5 2.5 57 230 .086 0      .51 .33 11   40 6.3 3.3 120 300
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 0 4.9 2.2 40 150 .24  0      .48 .31 6.0 40 6.0 3.2 98 300
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 0 5.5 2.5 48 220 .086 0      .49 .31 6.3 40 6.1 3.2 110 310
recursive-simple/sum_non_eq_false-unreach-call.c 0 5.8 2.6 46 280 .086 0      .52 .33 9.7 40 5.5 3.0 120 290
recursive-simple/sum_non_false-unreach-call_true-termination.c 0 5.8 2.7 54 280 .086 0      .50 .32 9.7 39 6.1 3.2 130 290
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 7.3 2.4 53 290 .045 0      3.5  1.9  60   260 7.4 4.0 110 320
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 6.8 2.3 55 290 .045 0      3.5  2.0  84   260 7.7 4.2 170 320
recursive-simple/fibo_10_true-unreach-call.c 2 7.5 2.5 61 290 .045 0      3.4  1.9  76   250 45   26   870 3000
recursive-simple/fibo_15_true-unreach-call.c 2 9.8 4.6 95 290 .045 0      3.5  2.0  78   260 600   550   8500 6300
recursive-simple/fibo_20_true-unreach-call.c 0 720   730   5400 200 .36  0      .54 .34 14   40 5.9 3.1 120 310
recursive-simple/fibo_25_true-unreach-call.c 0 4.7 2.2 43 150 .23  0      .49 .33 11   39 5.7 3.0 110 290
recursive-simple/fibo_2calls_10_true-unreach-call.c 2 7.6 2.5 56 300 .045 0      3.6  2.0  82   260 86   53   2100 4500
recursive-simple/fibo_2calls_15_true-unreach-call.c 1 10   4.8 88 290 .045 0      3.6  2.0  71   250 960   900   24000 5400
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 720   720   5900 200 .37  0      .49 .31 7.0 41 5.7 3.0 100 280
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 840   850   6700 200 .30  0      .50 .33 12   40 5.8 3.1 120 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 7.2 2.3 54 290 .045 0      3.5  2.0  73   260 12   6.5 240 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 2 8.1 2.5 71 320 .045 0      3.6  2.0  67   260 20   11   420 530
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 2 7.4 2.4 64 300 .045 0      3.8  2.1  75   260 26   14   500 660
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 2 7.9 2.5 63 290 .045 0      3.5  1.9  49   260 33   19   680 780
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 2 7.9 2.5 61 290 .045 .10   3.5  1.9  53   260 48   28   880 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c 2 7.8 2.5 65 290 .045 0      3.6  2.0  57   250 17   9.2 310 530
recursive-simple/fibo_7_true-unreach-call.c 2 7.8 2.4 59 290 .045 0      3.6  2.0  82   260 22   12   460 570
recursive-simple/id2_b2_o3_true-unreach-call.c 0 5.1 2.6 48 150 .25  0      .50 .33 3.8 40 5.7 3.1 110 300
recursive-simple/id2_b3_o5_true-unreach-call.c 0 5.2 2.7 52 150 .25  0      .56 .37 11   43 6.4 3.3 140 310
recursive-simple/id2_b5_o10_true-unreach-call.c 0 5.2 2.7 51 150 .25  0      .62 .40 8.7 43 6.1 3.3 130 300
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 2 7.6 2.4 54 290 .045 0      3.5  1.9  72   260 16   8.7 360 520
recursive-simple/id_b2_o3_true-unreach-call.c 0 5.0 2.4 43 150 .23  0      .51 .32 8.5 39 6.3 3.3 140 300
recursive-simple/id_b3_o5_true-unreach-call.c 0 5.0 2.4 45 150 .23  0      .52 .33 12   42 5.8 3.1 120 290
recursive-simple/id_b5_o10_true-unreach-call.c 0 4.9 2.4 49 150 .23  0      .51 .32 7.2 40 5.4 2.9 100 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 7.6 2.5 64 300 .045 0      3.5  2.0  74   250 18   10   350 540
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 7.5 2.4 61 290 .045 .0082 3.6  2.0  74   260 24   14   500 620
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 8.0 2.6 70 290 .045 0      3.5  2.0  69   250 32   19   620 730
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 0 4.9 2.3 46 160 .23  0      .49 .32 12   43 5.8 3.1 92 300
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 7.4 2.4 65 290 .045 0      3.5  2.0  64   260 11   6.3 200 380
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 7.7 2.5 69 290 .045 0      3.5  2.0  62   260 20   12   440 580
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 7.6 2.4 61 300 .045 0      3.4  1.9  49   260 27   16   590 660
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 7.9 2.5 61 290 .045 0      3.4  1.9  61   260 39   23   690 720
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 0 4.6 2.2 45 160 .24  0      .51 .34 6.5 40 5.6 3.0 100 290
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 7.4 2.4 59 290 .045 0      3.6  2.0  81   260 11   6.2 230 400
recursive-simple/sum_non_eq_true-unreach-call.c 0 4.7 2.3 43 150 .23  .094  .49 .32 11   39 6.0 3.1 120 300
recursive-simple/sum_non_true-unreach-call_true-termination.c 0 4.9 2.5 48 160 .24  0      .51 .32 12   40 5.5 3.0 100 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 45 19000 19000   130000 57000 27     1.9  98 23 15 420 1800   98 270 140 5200 13000   98 97   56   1800 7100 98 2300 1900 48000 40000
    correct results 22 44 170 56   1400 6500 .99  .11 0 0 0 0 0   0 0 0 0 0   3 77   44   1500 5700 22 1200 870 20000 25000
        correct true 22 44 170 56   1400 6500 .99  .11 0 0 0 0 0   0 0 0 0 0   3 77   44   1500 5700 22 1200 870 20000 25000
        correct false 0
    correct-unconfimed results 1 1 10 4.8 88 290 .045 0    0 0 0 0 0   0 0 0 0 0   0 3.6 2.0 71 250 0 960 900 24000 5400
        correct-unconfirmed true 1 1 10 4.8 88 290 .045 0    0 0 0 0 0   0 0 0 0 0   0 3.6 2.0 71 250 0 960 900 24000 5400
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 45
Run set sv-comp17.ReachSafety-Recursive