Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:37:51 CET [[ 2017-01-15 04:18:56 CET ]] [[ 2017-01-15 04:38:06 CET ]] [[ 2017-01-15 04:27:27 CET ]] [[ 2017-01-15 04:45:45 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.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)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .21 2.8 10 .074 0     error 22    14    300   1700 true 7.3 4.0 120 330 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 .23 2.7 11 .012 0     timeout 92    69    910   4400 false(valid-deref) 8.1 4.3 160 350 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .23 2.8 11 .074 0     error 22    14    340   760 true 7.7 4.2 140 330 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .63 .63 6.1 12 .012 0     false(valid-deref) 3.2  1.8  55   250 false(valid-deref) 7.1 3.8 140 320 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i error 0 wit inspect .41 .40 5.2 10 .074 0     error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.4 3.3 120 320 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i error 0 wit inspect .60 .59 7.3 11 .074 0     error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.2 3.3 110 300 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.2  1.2  11   12 .012 0     false(valid-deref) 3.6  2.0  78   240 false(valid-deref) 7.7 4.1 170 320 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3  1.3  13   12 .012 0     false(valid-deref) 3.6  2.0  75   230 false(valid-deref) 7.9 4.2 140 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error 0 wit inspect .36 .35 3.8 11 .074 0     error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.8 3.6 120 310 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 .25 2.6 12 .012 0     false(valid-deref) 3.9  2.2  86   230 false(valid-deref) 7.7 4.1 150 310 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .30 .29 2.9 13 .074 0     error 4.4  2.4  100   250 false(valid-deref) 10   5.6 190 370 - -
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 wit inspect .29 .28 3.6 14 .074 0     error (invalid witness file) .55 .36 13   40 error (invalid witness file) 5.9 3.1 110 300 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .36 .35 4.5 17 .074 0     error 4.4  2.4  91   260 false(valid-deref) 8.6 4.6 150 360 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .40 .40 4.3 11 .074 0     error 4.1  2.3  68   250 true 17   9.7 200 480 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .22 2.5 11 .074 0     error 4.3  2.3  97   280 false(valid-deref) 10   5.4 150 360 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 2.9 11 .012 0     false(valid-deref) 3.7  2.1  79   250 false(valid-deref) 7.8 4.2 120 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .58 .57 6.7 11 .012 0     false(valid-deref) 3.3  1.9  76   230 false(valid-deref) 7.0 3.8 120 310 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i true 2 wit inspect .26 .25 3.2 10 .074 0     - - error 3.8  2.1  74   250 timeout 960   880   24000 2700
array-memsafety/array01-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   790 .074 0     - - error (invalid witness file) .50 .34 3.6 39 error (invalid witness file) 6.1 3.2 110 310
array-memsafety/array02-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   950 .074 0     - - error (invalid witness file) .53 .34 7.6 40 error (invalid witness file) 7.0 3.7 130 320
array-memsafety/array03-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9700   760 .074 .69  - - error (invalid witness file) .51 .34 7.6 40 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i true 2 wit inspect .24 .24 2.9 11 .074 0     - - error 3.9  2.1  62   250 true 14   7.6 210 410
array-memsafety/count_down-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   570 .074 0     - - error (invalid witness file) .49 .32 10   39 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 1.2  1.2  13   13 .074 0     - - error 4.4  2.4  87   260 timeout 960   880   16000 4400
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect .23 .23 2.3 11 .074 0     - - error 3.9  2.1  74   250 true 16   9.4 240 490
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 3.3  3.3  36   20 .074 .16  - - error 4.2  2.3  74   260 true 39   27   720 730
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect .37 .36 4.0 11 .074 0     - - error 4.0  2.2  74   250 timeout 960   830   20000 2300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9900   550 .074 0     - - error (invalid witness file) .51 .33 4.1 40 error (invalid witness file) 5.9 3.1 110 290
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect .23 .22 2.6 10 .074 0     - - error 3.7  2.1  73   240 true 16   8.9 290 550
array-memsafety/cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 2.7  2.7  31   17 .074 0     - - error 4.4  2.4  85   260 timeout 960   920   16000 1300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 5.4  5.4  65   22 .074 0     - - error 4.0  2.2  74   250 true 33   22   370 660
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect 4.3  4.3  56   28 .074 0     - - error 3.8  2.1  62   240 timeout 960   860   15000 4600
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7000   500 .074 0     - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8300   510 .074 0     - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 5.2 2.8 93 290
array-memsafety/diff-alloca_true-valid-memsafety.i true 2 wit inspect .28 .27 3.0 13 .074 0     - - error 4.4  2.4  82   260 true 23   13   280 610
array-memsafety/insertionsort-alloca_true-valid-memsafety.i true 2 wit inspect .22 .21 2.6 11 .074 0     - - error 3.9  2.2  88   240 true 18   10   300 530
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect .23 .22 2.5 11 .074 .033 - - error 3.9  2.2  86   250 true 14   7.6 190 440
array-memsafety/lis-alloca_true-valid-memsafety.i true 2 wit inspect .24 .23 3.0 12 .074 0     - - error 3.8  2.1  65   250 true 21   12   330 570
array-memsafety/mult_array-alloca_true-valid-memsafety.i true 2 wit inspect .52 .51 6.8 15 .074 0     - - error 4.3  2.4  91   260 true 23   15   440 530
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect .79 .78 9.7 12 .074 0     - - error 4.1  2.3  81   250 true 18   10   380 540
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect 1.2  1.2  14   15 .074 0     - - error 4.1  2.2  80   250 true 16   9.0 280 540
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 2 wit inspect 1.6  1.5  18   15 .074 .012 - - error 3.9  2.2  72   250 true 21   13   360 520
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect .30 .30 3.9 11 .074 0     - - error 4.6  2.5  63   260 true 14   8.0 200 530
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i true 2 wit inspect .37 .36 4.3 11 .074 0     - - error 4.1  2.3  78   250 timeout 960   840   12000 2200
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i true 2 wit inspect 4.2  4.2  53   28 .074 0     - - error 4.2  2.3  87   250 timeout 960   840   11000 1600
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 1.5  1.5  15   13 .074 0     - - error 4.3  2.4  87   250 timeout 960   860   13000 4600
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 3.2  3.2  38   20 .074 .066 - - error 4.1  2.2  87   260 true 41   29   570 670
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect .36 .35 3.5 11 .074 0     - - error 4.7  2.6  80   260 timeout 960   840   14000 2800
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   620 .074 0     - - error (invalid witness file) .50 .32 5.3 40 error (invalid witness file) 5.9 3.1 120 290
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 2 wit inspect 1.3  1.2  12   13 .074 0     - - error 4.6  2.5  86   260 timeout 960   830   15000 2200
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect .21 .20 2.4 10 .074 0     - - error 4.2  2.3  74   250 true 19   11   260 540
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 2.8  2.7  25   16 .074 0     - - error 4.2  2.3  86   260 timeout 960   920   16000 2400
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 4.1  4.1  58   20 .074 0     - - error 4.1  2.3  76   250 true 39   25   350 680
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect 3.4  3.3  44   24 .074 0     - - error 4.1  2.2  83   250 timeout 960   830   25000 1900
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect 1.6  1.5  21   15 .074 0     - - error 4.4  2.4  85   250 true 19   11   320 570
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    12000   580 .074 0     - - error (invalid witness file) .53 .35 13   41 error (invalid witness file) 6.3 3.4 120 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9900   800 .074 0     - - error (invalid witness file) .51 .33 6.5 40 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7600   800 .074 0     - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.7 3.1 110 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect .23 .22 2.4 10 .074 0     - - error 4.6  2.6  63   250 true 26   18   590 550
array-memsafety/selectionsort-alloca_true-valid-memsafety.i true 2 wit inspect .24 .23 2.4 11 .074 0     - - error 3.9  2.2  81   240 true 16   8.8 240 560
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect .23 .23 2.8 10 .074 0     - - error 3.9  2.1  70   250 true 15   8.2 230 410
array-memsafety/stroeder2-alloca_true-valid-memsafety.i true 2 wit inspect 1.2  1.2  15   13 .074 0     - - error 4.0  2.2  93   260 true 13   7.4 160 400
array-memsafety/strreplace-alloca_true-valid-memsafety.i true 2 wit inspect .22 .21 2.6 11 .074 0     - - error 4.1  2.2  88   250 true 28   18   430 570
array-memsafety/subseq-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6900   570 .074 0     - - error (invalid witness file) .51 .33 7.6 40 error (invalid witness file) 6.3 3.4 110 300
array-memsafety/substring-alloca_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9700   760 .074 .38  - - error (invalid witness file) .52 .34 7.5 40 error (invalid witness file) 6.2 3.3 130 290
array-examples/relax_false-valid-deref.i timeout (timeout) 0 wit inspect 900    900    7400   2300 .074 0     error (invalid witness file) .55 .35 12   40 error (invalid witness file) 6.2 3.2 110 300 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout (timeout) 0 wit inspect 900    900    6500   3500 .012 0     error (invalid witness file) .51 .34 8.5 40 error (invalid witness file) 6.1 3.2 120 310 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout (timeout) 0 wit inspect 900    900    9100   1600 .012 0     error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.1 3.3 120 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout (timeout) 0 wit inspect 900    900    11000   1800 .012 0     error (invalid witness file) .48 .32 6.3 39 error (invalid witness file) 6.1 3.2 120 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 69 83 15000   15000   160000 19000 4.5  1.3  69 180 120 2400 9700   69 160 88 2900 6900   69 150 84 2900 9300   69 12000 11000 210000 50000  
    correct results 48 83 55   55   640 650 3.1  .27 6 180 120 2400 9400   13 110 62 1900 4500   0 140 80 2800 8800   23 12000 11000 210000 46000  
        correct true 35 70 49   48   580 500 2.6  .27 0 0 0 0 0   3 0 0 0 0   0 140 80 2800 8800   23 12000 11000 210000 46000  
        correct false 13 13 6.2 6.1 64 150 .53 0    6 180 120 2400 9400   10 110 62 1900 4500   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 (69 tasks, max score: 117) 83
Run set sv-comp17.MemSafety-Arrays