Tool ULTIMATE Automizer 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 06:16:04 CET [[ 2017-01-15 05:34:44 CET ]] [[ 2017-01-15 05:49:53 CET ]] [[ 2017-01-15 05:35:06 CET ]] [[ 2017-01-15 05:51:11 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.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 6.2 2.0 47 340 2.5 0    true 5.2  2.8  71 270 false(valid-deref) 9.2 4.9 170 360 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.5 1.9 50 360 2.5 0    false(valid-deref) 4.7  2.6  54 260 false(valid-deref) 8.3 4.4 170 350 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.2 2.1 55 370 2.5 0    true 4.8  2.6  74 260 false(valid-deref) 9.0 4.8 200 360 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 1.8 44 340 2.5 0    true 4.0  2.3  33 240 false(valid-deref) 8.1 4.3 140 340 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 12   3.7 95 490 2.5 0    error 5.2  2.8  58 270 false(valid-deref) 11   5.9 210 360 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.6 2.4 61 400 2.5 0    true 5.7  3.1  67 270 false(valid-deref) 14   7.7 170 350 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.5 1.8 48 320 2.5 0    true 3.4  1.9  32 250 false(valid-deref) 8.9 4.8 150 350 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 1.9 45 320 2.5 0    error (invalid witness file) 2.6  1.5  41 160 false(valid-deref) 8.8 4.6 150 340 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 9.7 2.8 73 400 2.5 0    true 6.4  3.4  62 270 false(valid-deref) 12   6.3 170 370 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.1 1.9 45 320 2.5 0    false(valid-deref) 4.1  2.2  52 250 false(valid-deref) 8.8 4.6 190 330 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 9.5 2.6 71 380 2.5 0    error (invalid witness file) 3.0  1.6  49 180 false(valid-deref) 11   5.7 210 370 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 10   3.1 75 410 2.5 0    error (invalid witness file) 2.9  1.7  46 180 false(valid-deref) 9.8 5.2 190 370 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.6 2.1 50 330 3.1 0    true 5.5  3.0  64 270 false(valid-deref) 8.5 4.6 140 350 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 8.0 2.2 62 360 2.9 0    true 5.0  2.7  63 270 true 15   8.1 270 470 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.0 2.2 50 370 2.5 0    true 6.2  3.4  57 290 false(valid-deref) 11   5.7 190 370 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.7 2.1 49 340 2.5 0    false(valid-deref) 3.8  2.2  73 250 false(valid-deref) 8.2 4.4 140 350 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 1.9 48 320 2.5 0    true 4.0  2.3  49 250 false(valid-deref) 8.2 4.4 170 350 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   820   11000 1600 2.7 0    - - error (invalid witness file) .49 .32 9.1 39 error (invalid witness file) 5.8 3.1 120 290
array-memsafety/array01-alloca_true-valid-memsafety.i true 2 wit inspect 10   3.0 82 430 2.5 0    - - error 3.9  2.2  64   270 true 18   10   230 410
array-memsafety/array02-alloca_true-valid-memsafety.i true 2 wit inspect 9.2 2.9 71 420 2.5 0    - - error 4.7  2.6  48   240 true 14   7.7 300 430
array-memsafety/array03-alloca_true-valid-memsafety.i true 2 wit inspect 9.1 2.9 77 430 2.5 0    - - error 4.1  2.2  63   250 true 13   7.4 310 430
array-memsafety/bubblesort-alloca_true-valid-memsafety.i true 2 wit inspect 10   3.0 76 400 2.5 0    - - error 4.0  2.2  62   250 true 13   7.2 210 400
array-memsafety/count_down-alloca_true-valid-memsafety.i true 2 wit inspect 12   3.8 95 490 2.7 0    - - error 4.7  2.6  35   240 true 17   9.6 320 550
array-memsafety/cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   810   13000 3000 2.3 0    - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 5.5 3.0 110 290
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect 13   3.9 100 490 2.5 0    - - error 3.9  2.1  48   260 true 17   9.6 360 490
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 27   15   260 680 2.5 0    - - error 4.2  2.3  62   250 true 36   25   700 530
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   780   13000 1200 2.3 0    - - error (invalid witness file) .48 .30 9.3 40 error (invalid witness file) 5.7 3.0 94 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i true 2 wit inspect 24   12   250 550 2.6 0    - - error 4.2  2.4  57   250 true 30   20   670 660
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 13   3.5 91 500 2.5 .11 - - error 3.8  2.1  79   240 true 15   8.6 310 520
array-memsafety/cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   870   11000 1000 2.3 0    - - error (invalid witness file) .55 .35 9.7 40 error (invalid witness file) 6.3 3.3 96 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 29   17   300 540 2.6 0    - - error 4.5  2.5  44   250 true 34   23   500 670
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   800   14000 1600 2.3 0    - - error (invalid witness file) .56 .36 9.2 39 error (invalid witness file) 7.0 3.7 120 310
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect 43   28   450 730 2.5 0    - - error 4.7  2.6  41   250 true 53   40   1100 740
array-memsafety/cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect 45   32   510 690 2.6 0    - - error 4.2  2.3  78   260 true 65   48   830 700
array-memsafety/diff-alloca_true-valid-memsafety.i true 2 wit inspect 16   5.7 130 530 2.5 0    - - error 5.6  3.1  59   250 true 23   13   320 650
array-memsafety/insertionsort-alloca_true-valid-memsafety.i true 2 wit inspect 12   3.9 90 480 2.5 0    - - error 4.3  2.3  49   260 true 18   10   360 530
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect 9.7 3.0 76 400 2.5 0    - - error 3.9  2.1  62   250 true 13   7.4 170 430
array-memsafety/lis-alloca_true-valid-memsafety.i true 2 wit inspect 15   5.2 130 500 2.6 0    - - error 4.6  2.5  70   260 true 21   12   300 600
array-memsafety/mult_array-alloca_true-valid-memsafety.i true 2 wit inspect 18   10   180 510 2.5 0    - - error 4.4  2.4  62   280 true 24   16   550 510
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect 12   3.7 94 480 2.5 0    - - error 5.4  2.9  60   260 true 17   9.8 260 520
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect 12   3.6 90 540 2.5 0    - - error 5.0  2.8  60   250 true 15   8.6 260 560
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 2 wit inspect 16   7.3 140 530 2.5 0    - - error 4.1  2.3  60   240 true 21   13   340 540
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect 11   3.5 100 470 2.5 0    - - error 4.6  2.5  52   250 true 15   8.7 250 550
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   780   12000 1100 2.9 0    - - error (invalid witness file) .67 .42 8.0 42 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   790   12000 900 2.3 0    - - error (invalid witness file) .57 .36 9.6 41 error (invalid witness file) 8.7 4.5 100 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   800   11000 2600 2.3 0    - - error (invalid witness file) .54 .34 11   39 error (invalid witness file) 6.3 3.4 110 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 34   21   320 560 2.5 0    - - error 4.5  2.5  42   240 true 40   28   880 670
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   780   12000 1000 2.3 0    - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.8 3.6 140 320
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   860   14000 1600 2.7 0    - - error (invalid witness file) .62 .40 8.0 40 error (invalid witness file) 6.2 3.3 140 310
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   770   15000 1200 2.3 0    - - error (invalid witness file) .54 .34 12   40 error (invalid witness file) 7.7 4.0 120 340
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 12   3.7 92 470 2.5 0    - - error 4.3  2.4  44   250 true 16   9.2 190 520
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   850   10000 1400 2.3 0    - - error (invalid witness file) .63 .40 12   43 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 32   18   300 570 2.5 0    - - error 4.4  2.4  69   270 true 40   27   740 740
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   780   12000 1100 2.7 0    - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.6 3.0 100 300
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect 13   4.1 110 530 2.5 0    - - error 4.1  2.3  40   260 true 18   10   260 570
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect 31   19   320 530 2.5 0    - - error 4.0  2.2  59   250 true 41   31   750 620
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect 39   26   420 720 2.5 0    - - error 4.0  2.2  58   240 true 49   38   980 650
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   810   14000 900 2.3 0    - - error (invalid witness file) .52 .32 11   39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect 23   14   200 510 3.1 0    - - error 4.3  2.4  57   250 true 24   17   450 550
array-memsafety/selectionsort-alloca_true-valid-memsafety.i true 2 wit inspect 13   3.6 99 490 2.5 0    - - error 4.0  2.2  57   250 true 17   9.4 310 550
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect 9.4 2.9 73 470 2.5 0    - - error 4.8  2.7  59   270 true 15   8.3 310 440
array-memsafety/stroeder2-alloca_true-valid-memsafety.i true 2 wit inspect 10   3.1 79 490 2.5 0    - - error 5.0  2.7  60   260 true 13   7.3 220 430
array-memsafety/strreplace-alloca_true-valid-memsafety.i true 2 wit inspect 20   9.4 180 500 2.5 0    - - error 4.3  2.4  68   250 true 26   17   630 590
array-memsafety/subseq-alloca_true-valid-memsafety.i true 2 wit inspect 60   48   730 590 2.5 0    - - error 4.0  2.2  52   280 true 72   60   1400 680
array-memsafety/substring-alloca_true-valid-memsafety.i true 2 wit inspect 61   45   770 620 2.5 0    - - error 4.6  2.5  56   250 true 68   53   1200 830
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect 6.1 2.0 44 330 2.5 0    error (invalid witness file) 3.9  2.1  36 190 false(valid-deref) 10   5.4 200 350 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   740   15000 1500 2.3 0    error (invalid witness file) .51 .34 10 40 error (invalid witness file) 5.7 3.0 110 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900   730   12000 2000 2.3 0    error (invalid witness file) .51 .32 12 39 error (invalid witness file) 6.2 3.3 110 310 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900   730   14000 1400 2.3 0    error (invalid witness file) .51 .34 11 39 error (invalid witness file) 6.3 3.3 130 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 86 16000 14000 220000 50000 170 .11 69 82 45 1000 4500   69 200 110 3600 7400   69 160 87 2100 9200   69 1000 680 19000 24000  
    correct results 52 86 860 430 8100 24000 130 .11 13 80 44 980 4400   18 180 96 3200 6500   0 150 82 1900 8600   34 930 630 17000 19000  
        correct true 34 68 720 390 7100 18000 87 .11 10 0 0 0 0   1 0 0 0 0   0 150 82 1900 8600   34 930 630 17000 19000  
        correct false 18 18 130 41 1000 6500 46 0    3 80 44 980 4400   17 180 96 3200 6500   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) 86
Run set sv-comp17.MemSafety-Arrays