Tool SymDIVINE
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:13:29 CET [[ 2017-01-15 02:06:46 CET ]] [[ 2017-01-15 03:46:01 CET ]] [[ 2017-01-15 02:24:39 CET ]] [[ 2017-01-15 04:02:29 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options --fix_volatile --fix_inline --silent -Os [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.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 false(unreach-call) 1 wit inspect 8.4   8.5   130    34   .0082 .88   false(unreach-call) 7.6  4.1  81   300 true 6.5 3.5 110 310 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     7800    28   .0082 0      error (invalid witness file) .66 .42 8.0 42 error (invalid witness file) 5.8 3.1 110 300 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true -32 wit inspect .088 .11  .73 11   .0082 5.6    false(unreach-call) 5.0  2.8  86   280 false(unreach-call) 10   5.6 100 330 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     13000    350   .0082 0      error (invalid witness file) .53 .34 9.2 44 error (invalid witness file) 5.5 2.9 120 300 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     13000    430   .0082 0      error (invalid witness file) .69 .44 8.0 44 error (invalid witness file) 6.9 3.6 74 290 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    440   .0082 0      error (invalid witness file) .62 .39 7.9 40 error (invalid witness file) 6.0 3.2 120 300 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     13000    380   .0082 10      error (invalid witness file) .63 .41 5.2 39 error (invalid witness file) 7.5 4.0 77 290 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 13     13     170    52   .0082 0      - - error (invalid witness file) .65 .41 9.0 43 error (invalid witness file) 5.3 2.9 110 280
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 13     13     170    54   .0082 0      - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.8 3.1 110 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 13     13     260    52   .0082 0      - - error (invalid witness file) .55 .34 13   43 error (invalid witness file) 5.4 2.9 93 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    9300   .0082 10      - - error (invalid witness file) .54 .34 13   45 error (invalid witness file) 6.1 3.2 120 290
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .053 .055 .58 9.8 .0082 0      - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.0 3.2 110 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     10000    340   .0082 .098  - - error (invalid witness file) .69 .44 10   42 error (invalid witness file) 5.5 3.0 94 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     900     14000    440   .0082 4.5    - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.0 3.2 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .074 .074 .80 9.9 .0082 0      - - error (recursion) 3.8  2.1  58   260 true 32   18   470 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    430   .0082 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 7.2 3.8 75 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    360   .0082 0      - - error (invalid witness file) .64 .42 7.7 40 error (invalid witness file) 6.0 3.2 120 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    2800   .0082 .13   - - error (invalid witness file) .53 .33 12   41 error (invalid witness file) 6.3 3.3 95 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900     900     13000    120   .012  3.9    - - error (invalid witness file) .48 .34 10   39 error (invalid witness file) 6.0 3.2 140 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    87   .0082 9.9    - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 5.6 3.0 86 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    72   .012  .37   - - error (invalid witness file) .66 .42 8.3 42 error (invalid witness file) 5.7 3.0 120 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     12000    8000   .0082 0      - - error (invalid witness file) .67 .42 8.6 40 error (invalid witness file) 6.6 3.4 120 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     11000    350   .0082 3.9    - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.3 3.4 91 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     900     13000    350   .0082 0      - - error (invalid witness file) .64 .42 7.4 39 error (invalid witness file) 6.0 3.2 85 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .081 .081 .54 9.8 .0082 0      false(unreach-call) 3.9  2.2  72   280 true 7.6 4.0 140 320 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .079 .079 .50 9.7 .0082 0      false(unreach-call) 4.1  2.3  68   290 true 8.2 4.4 100 320 - -
recursive-simple/fibo_10_false-unreach-call.c false(unreach-call) 1 wit inspect .097 .097 .82 9.5 .0082 0      false(unreach-call) 8.7  4.6  160   450 true 8.3 4.5 82 310 - -
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .66  .66  8.7  77   .0082 0      false(unreach-call) 51    35    450   2000 true 8.4 4.4 87 320 - -
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 0 wit inspect 8.6   8.6   94    790   .0082 0      timeout 97    86    1000   1600 true 8.4 4.5 93 310 - -
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 0 wit inspect 120     120     1400    15000   .0082 0      timeout 97    61    920   5300 true 6.4 3.5 140 310 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .14  .14  1.0  11   .0082 0      false(unreach-call) 8.9  4.8  200   450 true 6.8 3.7 150 310 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .75  .75  8.9  78   .0082 0      false(unreach-call) 52    37    480   1900 true 6.8 3.7 130 310 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 0 wit inspect 11     11     120    1500   .0082 0      timeout 97    84    890   1500 true 8.9 4.7 100 310 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 0 wit inspect 140     140     1800    14000   .0082 0      timeout 98    55    1400   5000 true 7.6 4.0 140 310 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .090 .090 .32 9.9 .0082 0      false(unreach-call) 3.8  2.2  59   270 true 7.6 4.0 110 320 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .078 .56 9.5 .0082 0      false(unreach-call) 4.9  2.8  74   280 true 8.7 4.6 120 320 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .056 .056 .55 9.8 .0082 0      false(unreach-call) 4.9  2.7  84   290 true 8.8 4.6 100 340 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .085 .085 .57 9.7 .0082 0      false(unreach-call) 6.4  3.5  78   290 true 6.9 3.7 140 310 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c false(unreach-call) 1 wit inspect .092 .092 .63 9.6 .0082 0      false(unreach-call) 9.0  4.8  100   310 true 8.2 4.4 90 310 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .056 .056 .54 9.8 .0082 0      false(unreach-call) 5.4  3.0  39   280 true 5.9 3.2 120 300 - -
recursive-simple/fibo_7_false-unreach-call.c false(unreach-call) 1 wit inspect .059 .059 .57 9.8 .0082 0      false(unreach-call) 6.4  3.5  41   290 true 8.3 4.3 110 320 - -
recursive-simple/id2_b3_o2_false-unreach-call.c timeout 0 wit inspect 900     900     12000    370   .0082 0      error (invalid witness file) .57 .35 12   39 error (invalid witness file) 6.4 3.3 94 300 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .053 .053 .57 9.9 .0082 0      false(unreach-call) 4.5  2.5  76   290 true 6.2 3.3 110 310 - -
recursive-simple/id_b3_o2_false-unreach-call.c timeout 0 wit inspect 900     900     12000    370   .0082 0      error (invalid witness file) .48 .31 10   40 error (invalid witness file) 5.5 2.9 120 300 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .072 .072 .52 9.7 .0082 0      false(unreach-call) 5.3  2.9  52   280 true 7.7 4.1 120 320 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .069 .068 .51 9.6 .0082 0      false(unreach-call) 4.5  2.5  52   290 true 7.3 3.9 120 310 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .098 .098 .35 9.8 .0082 0      false(unreach-call) 4.9  2.7  95   280 true 6.5 3.5 120 320 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .053 .053 .49 9.9 .0082 0      false(unreach-call) 5.9  3.2  45   290 true 7.5 4.0 100 310 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .052 .052 .54 9.6 .0082 0      false(unreach-call) 4.8  2.6  37   280 true 7.0 3.8 110 310 - -
recursive-simple/id_o1000_false-unreach-call.c false(unreach-call) 0 wit inspect .062 .062 .43 9.8 .0082 0      timeout 96    82    1900   2800 true 7.7 4.1 100 310 - -
recursive-simple/id_o100_false-unreach-call.c false(unreach-call) 1 wit inspect .059 .059 .55 9.5 .0082 0      false(unreach-call) 13    6.6  120   500 true 8.2 4.4 100 310 - -
recursive-simple/id_o10_false-unreach-call.c false(unreach-call) 1 wit inspect .054 .055 .73 9.8 .0082 .033  false(unreach-call) 5.6  3.1  67   280 true 8.1 4.3 68 310 - -
recursive-simple/id_o200_false-unreach-call.c false(unreach-call) 1 wit inspect .072 .072 .54 9.9 .0082 0      false(unreach-call) 22    12    260   770 true 6.7 3.6 140 320 - -
recursive-simple/id_o20_false-unreach-call.c false(unreach-call) 1 wit inspect .084 .083 .37 9.8 .0082 0      false(unreach-call) 5.2  2.8  59   290 true 6.6 3.6 120 310 - -
recursive-simple/id_o3_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .13  .63 12   .0082 6.7    false(unreach-call) 5.7  3.2  60   290 true 7.2 3.8 120 310 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .080 .080 .53 9.5 .0082 0      false(unreach-call) 4.3  2.4  86   280 true 7.7 4.2 110 320 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .078 .47 10   .0082 0      false(unreach-call) 4.7  2.6  46   280 true 8.8 4.7 76 310 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .078 .078 .60 9.6 .0082 0      false(unreach-call) 6.3  3.4  54   290 true 7.0 3.8 120 320 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .052 .053 .47 9.9 .0082 0      false(unreach-call) 5.4  3.0  100   290 true 6.3 3.4 130 310 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .060 .061 .41 9.5 .0082 0      false(unreach-call) 4.8  2.6  40   270 true 7.4 3.9 140 320 - -
recursive-simple/sum_non_eq_false-unreach-call.c false(unreach-call) 1 wit inspect .083 .083 .48 9.7 .0082 0      false(unreach-call) 4.2  2.4  46   270 true 8.7 4.7 76 300 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  .16  .85 17   .0082 9.7    false(unreach-call) 3.7  2.1  45   280 true 7.5 3.9 110 310 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .050 .051 .62 9.9 .0082 0      - - true 3.6  2.0  57   250 true 7.5 4.0 150 320
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .051 .069 .78 11   .0082 5.9    - - true 3.8  2.1  55   270 true 8.5 4.4 150 330
recursive-simple/fibo_10_true-unreach-call.c true 2 wit inspect .083 .083 1.1  9.8 .0082 0      - - error (recursion) 3.4  1.9  62   260 true 44   26   760 2800
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect .68  .68  8.0  77   .0082 0      - - error (recursion) 3.4  1.9  52   260 true 620   570   11000 6300
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 8.6   8.6   100    800   .0082 6.2    - - error (recursion) 3.2  1.8  48   260 timeout 960   910   15000 5600
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 120     120     1200    15000   .0082 0      - - error (recursion) 3.4  1.9  64   260 timeout 960   910   14000 5700
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .096 .097 1.1  11   .0082 0      - - error (recursion) 3.5  2.0  55   250 true 88   54   1300 4000
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .76  .76  9.0  78   .0082 0      - - error (recursion) 3.5  2.0  74   250 timeout 960   890   13000 5400
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 11     11     120    1500   .0082 0      - - error (recursion) 3.5  1.9  68   260 timeout 960   910   20000 5300
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 140     140     1600    14000   .0082 0      - - error (recursion) 3.4  1.9  75   260 timeout 960   910   15000 5200
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .051 .051 .65 9.8 .0082 0      - - true 4.2  2.4  52   260 true 13   7.0 260 420
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .059 .059 .42 9.9 .0082 0      - - error (recursion) 4.5  2.5  50   260 true 20   11   220 520
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .078 .078 .54 9.6 .0082 0      - - error (recursion) 4.0  2.3  47   260 true 22   13   270 590
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .058 .059 .62 9.8 .0082 0      - - error (recursion) 3.4  1.9  59   260 true 37   21   480 770
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .066 .066 .68 9.9 .0082 0      - - error (recursion) 3.5  1.9  71   250 true 52   30   810 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .051 .051 .72 9.7 .0082 0      - - error (recursion) 4.3  2.4  51   260 true 16   9.0 310 520
recursive-simple/fibo_7_true-unreach-call.c true 2 wit inspect .055 .055 .72 9.9 .0082 0      - - error (recursion) 3.5  2.0  73   250 true 21   12   230 650
recursive-simple/id2_b2_o3_true-unreach-call.c timeout 0 wit inspect 900     900     9900    360   .0082 0      - - error (invalid witness file) .48 .32 13   39 error (invalid witness file) 6.3 3.3 120 300
recursive-simple/id2_b3_o5_true-unreach-call.c timeout 0 wit inspect 900     900     11000    360   .0082 .0041 - - error (invalid witness file) .54 .35 12   39 error (invalid witness file) 5.9 3.1 91 300
recursive-simple/id2_b5_o10_true-unreach-call.c timeout 0 wit inspect 900     900     12000    370   .0082 0      - - error (invalid witness file) .50 .33 7.0 40 error (invalid witness file) 5.2 2.8 91 290
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .050 .051 .57 9.8 .0082 0      - - error (recursion) 3.4  1.9  38   260 true 14   7.7 280 430
recursive-simple/id_b2_o3_true-unreach-call.c timeout 0 wit inspect 900     900     10000    370   .0082 0      - - error (invalid witness file) .50 .33 10   41 error (invalid witness file) 6.1 3.3 120 310
recursive-simple/id_b3_o5_true-unreach-call.c timeout 0 wit inspect 900     900     13000    370   .0082 0      - - error (invalid witness file) .61 .38 7.1 40 error (invalid witness file) 5.4 2.9 110 290
recursive-simple/id_b5_o10_true-unreach-call.c timeout 0 wit inspect 900     900     13000    390   .0082 15      - - error (invalid witness file) .50 .32 8.2 40 error (invalid witness file) 6.1 3.2 79 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .068 .068 .56 9.7 .0082 0      - - error (recursion) 3.9  2.2  57   260 true 16   9.2 250 560
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .053 .052 .54 9.9 .0082 0      - - error (recursion) 3.2  1.8  54   260 true 23   13   390 620
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .050 .050 .58 9.9 .0082 0      - - error (recursion) 4.1  2.3  48   260 true 31   18   330 660
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .049 .050 .55 9.8 .0082 0      - - error (recursion) 4.1  2.3  54   250 true 37   22   430 820
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .053 .053 .45 9.9 .0082 0      - - error (recursion) 3.8  2.1  65   270 true 12   6.4 210 400
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .068 .068 .47 9.9 .0082 .13   - - error (recursion) 3.4  1.9  43   260 true 21   12   370 510
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .067 .067 .51 9.8 .0082 0      - - error (recursion) 3.5  1.9  47   260 true 26   15   460 720
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .054 .054 .47 9.9 .0082 0      - - error (recursion) 4.2  2.4  54   250 true 36   21   340 710
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .068 .068 .42 9.9 .0082 0      - - error (recursion) 3.7  2.1  65   260 true 46   27   550 700
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .080 .080 .44 9.7 .0082 0      - - error (recursion) 3.6  2.0  48   260 true 10   5.8 200 400
recursive-simple/sum_non_eq_true-unreach-call.c true 2 wit inspect .063 .063 .46 9.8 .0082 0      - - error (recursion) 4.1  2.3  51   250 true 9.0 5.0 190 330
recursive-simple/sum_non_true-unreach-call_true-termination.c true 2 wit inspect .082 .082 .86 9.7 .0082 0      - - error (recursion) 4.3  2.4  48   260 true 10   5.5 170 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 57 23000     23000    300000    91000 .81   94   98 780   550   9700 30000   98 330 180   5000 14000   98 130 73   2000 8900   98 6200 5500 99000 60000  
    correct results 58 84 14     14    190    810 .48   23   32 290   170   3300 13000   32 240 130   3600 10000   3 98 55   1400 6700   26 1300 940 20000 27000  
        correct true 26 52 2.3   2.3  24    320 .21   6.1 0 0   0   0 0   32 0 0   0 0   3 98 55   1400 6700   26 1300 940 20000 27000  
        correct false 32 32 12     12    160    480 .26   17   32 290   170   3300 13000   0 240 130   3600 10000   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 10 5 550     550    6500    63000 .082  6.2 0 480   370   6200 16000   5 39 21   580 1600   0 17 9.6 330 1300   0 4800 4500 77000 27000  
        correct-unconfirmed true 5 5 280     280    3100    31000 .041  6.2 0 0   0   0 0   5 0 0   0 0   0 17 9.6 330 1300   0 4800 4500 77000 27000  
        correct-unconfirmed false 5 0 270     270    3500    31000 .041  0   0 480   370   6200 16000   0 39 21   580 1600   0 0 0   0 0   0 0 0 0 0  
    incorrect results 1 -32 .088 .11 .73 11 .0082 5.6 1 5.0 2.8 86 280   1 10 5.6 100 330   0 0 0   0 0   0 0 0 0 0  
        incorrect true 1 -32 .088 .11 .73 11 .0082 5.6 0 5.0 2.8 86 280   0 10 5.6 100 330   0 0 0   0 0   0 0 0 0 0  
        incorrect false 0
score (98 tasks, max score: 151) 57
Run set sv-comp17.ReachSafety-Recursive