Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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*
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]
Date of execution 2017-12-02 23:08:57 CET 2017-12-03 00:45:11 CET 2017-12-03 01:25:52 CET 2017-12-03 01:32:11 CET 2017-12-03 00:52:42 CET
Run set symbiotic.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-Arrays
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-02_2308.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/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.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 1 .28 12 2.4 1 3.8  270 -32 7.0   260   -32 .77   18    -
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 .24 11 2.7 0 91    490 1 5.5   260   1 .62   18    -
array-memsafety/count_down_unsafe_false-valid-deref.i 1 .24 12 2.3 1 4.0  250 -32 6.2   260   -32 .77   18    -
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 .22 11 2.2 1 3.3  240 1 6.2   250   0 .66   18    -
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 .87 59 8.5 0 3.9  250 -32 6.4   260   1 .70   18    -
array-memsafety/cstrlen_unsafe_false-valid-deref.i 0 .86 59 10   0 4.2  250 -32 7.4   260   -32 .66   18    -
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 .23 11 2.7 1 3.6  250 1 6.3   260   -32 .61   18    -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 .24 11 2.3 1 2.0  250 1 6.3   250   0 .75   20    -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 .62 59 6.4 0 4.4  250 -32 8.1   270   1 .80   18    -
array-memsafety/diff_usafe_false-valid-deref.i 1 .25 11 2.9 0 92    2100 1 5.5   260   0 .66   18    -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 .30 12 3.2 1 3.7  250 -32 5.3   230   1 .78   18    -
array-memsafety/lis_unsafe_false-valid-deref.i 1 .29 12 3.6 1 4.3  250 -32 7.7   260   0 .69   18    -
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 .55 17 6.4 1 3.8  270 -32 7.0   270   1 .69   18    -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 1 .29 12 3.0 1 4.3  250 -32 6.4   270   0 .69   18    -
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 .25 12 2.9 1 3.6  250 -32 8.9   270   -32 .79   19    -
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 .22 12 2.4 0 92    3700 1 5.9   270   1 .66   18    -
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 .24 11 2.2 1 2.0  250 1 5.5   260   0 .68   18    -
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i 2 .27 12 2.9 - - - 0 960     2600  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i 0 900    430 12000   - - - 0 .025 4.8
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i 0 900    610 13000   - - - 0 .020 5.0
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i 0 900    430 12000   - - - 0 .023 5.0
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i 2 .26 12 2.6 - - - 2 7.1   400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i 0 900    390 11000   - - - 0 .025 4.8
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i 2 .34 12 3.2 - - - 0 960     1100  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i 2 .26 12 2.8 - - - 2 16     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i 2 .28 12 2.8 - - - 0 960     840  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 .29 12 2.9 - - - 0 960     1500  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i 2 .28 12 3.8 - - - 0 960     980  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.1 - - - 2 14     480  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i 2 2.6  16 32   - - - 0 960     770  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 .30 12 3.1 - - - 0 960     800  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 .29 12 3.5 - - - 0 960     960  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.1 - - - 0 960     800  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i 2 .29 12 3.2 - - - 0 960     840  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i 2 .27 12 2.7 - - - 0 960     1300  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i 2 .25 12 2.9 - - - 2 11     510  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i 2 .26 12 2.9 - - - 2 15     450  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i 2 .25 14 3.8 - - - 0 960     770  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i 2 .58 17 6.8 - - - 2 18     520  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i 2 .25 12 2.9 - - - 0 960     790  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i 2 .21 11 2.2 - - - 0 960     640  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i 2 .22 11 2.2 - - - 0 960     690  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i 2 .27 12 2.8 - - - 0 960     800  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.3 - - - 0 960     940  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.5 - - - 0 960     880  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i 2 .32 12 3.8 - - - 0 960     1000  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i 2 .29 13 2.9 - - - 0 960     720  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 .29 12 3.0 - - - 0 960     1000  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i 2 .30 12 3.3 - - - 0 960     1000  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i 2 .28 12 3.4 - - - 0 960     1100  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i 2 .26 12 3.1 - - - 2 13     490  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i 2 2.1  16 27   - - - 0 960     750  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 .30 12 3.6 - - - 0 960     840  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 .29 12 3.0 - - - 0 960     1600  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.1 - - - 0 960     770  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i 2 .27 12 2.9 - - - 0 960     790  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i 2 .26 12 3.1 - - - 0 960     830  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i 2 .28 12 3.2 - - - 0 960     820  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i 2 .24 12 3.0 - - - 2 25     520  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i 2 .25 14 2.9 - - - 2 12     490  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i 2 .27 12 3.1 - - - 2 10     420  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i 2 1.2  14 13   - - - 0 960     740  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i 2 .25 12 3.2 - - - 0 960     840  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i 2 .26 12 3.2 - - - 0 960     840  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i 2 .26 12 3.1 - - - 0 960     1100  
array-examples/relax_false-valid-deref.i 1 .32 13 3.7 0 4.2  250 -32 9.4   300   1 .94   18    -
array-examples/sanfoundry_24_false-valid-deref.i 0 900    5500 9700   0 .67 43 0 .019 4.9 0 .0017 .28 -
array-examples/standard_strcpy_false-valid-deref_ground.i 0 900    1700 9300   0 .51 41 0 .024 4.8 0 .0016 .27 -
array-examples/standard_strcpy_original_false-valid-deref.i 0 900    2000 10000   0 .58 43 0 .022 4.9 0 .0022 .29 -
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 105 6300    12000 78000   21 11 330 10000 21 -345 120 4700 21 -153 13   330 48 20 33000 38000
    correct results 61 105 23    850 260   11 11 38 2800 7 7 41 1800 7 7 5.2 130 10 20 140 4800
        correct true 44 88 17    550 200   0 0 0 10 20 140 4800
        correct false 17 17 5.7  300 60   11 11 38 2800 7 7 41 1800 7 7 5.2 130 0
    correct-unconfimed results 1 0 .86 59 10   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 .86 59 10   0 0 0 0
    incorrect results 0 0 11 -352 80 2900 5 -160 3.6 92 0
        incorrect true 0 0 11 -352 80 2900 5 -160 3.6 92 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 105 11 -345 -153 20
Run set symbiotic.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-Arrays