Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon024; apollon065; apollon077; apollon078] [apollon077; apollon078; apollon093] [apollon077; apollon078] [apollon073; apollon077; apollon078; apollon091; apollon099; apollon124]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 00:00:31 CET 2017-12-02 01:15:07 CET 2017-12-02 01:40:08 CET 2017-12-02 01:42:26 CET 2017-12-02 01:17:53 CET
Run set esbmc-incr.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Arrays
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .17 29 2.0 false(valid-deref) 1 wit inspect 3.5  250 true -32 wit inspect 3.4   230   true -32 wit inspect .63   18    - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .17 28 1.5 true -32 wit inspect 2.7  250 true -32 wit inspect 3.4   240   true -32 wit inspect .58   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .21 29 1.9 false(valid-deref) 1 wit inspect 3.6  250 true -32 wit inspect 3.5   230   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 28 1.4 false(valid-deref) 1 wit inspect 3.1  250 true -32 wit inspect 4.5   230   error (2) 0 wit inspect .58   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 29 2.7 false(valid-deref) 1 wit inspect 2.5  250 true -32 wit inspect 5.3   230   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 29 3.0 false(valid-deref) 1 wit inspect 3.8  250 true -32 wit inspect 4.7   230   error (2) 0 wit inspect .64   18    - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .17 28 1.4 false(valid-deref) 1 wit inspect 3.2  250 true -32 wit inspect 3.3   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .36 28 3.2 true -32 wit inspect 3.5  250 true -32 wit inspect 3.4   230   error (2) 0 wit inspect .58   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .31 29 3.3 false(valid-deref) 1 wit inspect 3.4  250 true -32 wit inspect 3.7   250   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 0 wit inspect .19 28 3.6 timeout 0 wit inspect 92    2100 true -32 wit inspect 3.4   230   error (2) 0 wit inspect .59   18    - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .32 30 3.0 false(valid-deref) 1 wit inspect 2.4  250 true -32 wit inspect 3.6   240   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .20 29 2.2 false(valid-deref) 1 wit inspect 3.2  250 true -32 wit inspect 5.3   240   error (2) 0 wit inspect .64   18    - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .43 33 6.2 false(valid-deref) 1 wit inspect 2.6  260 true -32 wit inspect 3.5   230   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .28 29 3.5 false(valid-deref) 1 wit inspect 2.5  260 true -32 wit inspect 4.9   240   error (2) 0 wit inspect .64   18    - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .23 29 2.0 false(valid-deref) 1 wit inspect 3.3  250 true -32 wit inspect 5.2   240   true -32 wit inspect .63   18    - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .14 28 1.3 timeout 0 wit inspect 92    2200 true -32 wit inspect 3.3   240   error (2) 0 wit inspect .59   18    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 28 1.9 false(valid-deref) 1 wit inspect 2.9  240 true -32 wit inspect 4.4   230   error (2) 0 wit inspect .62   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    470 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1200 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    550 14000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1400 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1600 8600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    530 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    710 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    840 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    650 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1400 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    630 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    840 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    570 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    830 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    3400 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    620 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    620 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    300 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    520 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1500 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    980 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1800 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1900 9200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1300 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    560 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1900 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1200 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    3400 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    680 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    880 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1200 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1100 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    360 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    790 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    640 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    1200 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    3400 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    830 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    670 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    240 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    380 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    960 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    310 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    2000 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    770 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    270 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .042 5.0
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    320 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    750 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .29 29 2.6 false(valid-deref) 1 wit inspect 2.9  260 true -32 wit inspect 5.8   240   error (2) 0 wit inspect .66   18    - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900    910 12000   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900    210 13000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900    1000 10000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 69 14 46000    53000 560000   21 -50 230   8400 21 -576 75 4200 21 -90 11   330 48 0 .98 230
    correct results 14 14 3.4  410 37   14 14 43   3500 0 6 6 3.8 110 0
        correct true 0 0 0 0 0
        correct false 14 14 3.4  410 37   14 14 43   3500 0 6 6 3.8 110 0
    correct-unconfimed results 4 0 .86 110 9.6 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 4 0 .86 110 9.6 0 0 0 0
    incorrect results 0 2 -64 6.2 500 18 -576 75 4200 3 -96 1.8 55 0
        incorrect true 0 2 -64 6.2 500 18 -576 75 4200 3 -96 1.8 55 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 14 -50 -576 -90 0
Run set esbmc-incr.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Arrays