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-03 04:09:48 CET 2017-12-03 05:12:06 CET 2017-12-03 05:44:30 CET 2017-12-03 05:48:14 CET 2017-12-03 05:20:50 CET
Run set symbiotic.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-03_0409.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-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ 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
chgrp-incomplete_false-no-overflow.i 0 900    330 14000   0 .65 44 0 .018 4.9 0 .0014 .26 -
chroot-incomplete_false-no-overflow.i 0 900    210 11000   0 .58 42 0 .018 5.0 0 .0016 .29 -
cut_false-no-overflow.i 0 .47 23 6.7 0 .39 42 0 .019 4.9 0 .0015 .26 -
date_false-no-overflow.i 0 .60 33 7.3 0 .40 41 0 .022 4.9 0 .0018 .30 -
du_false-no-overflow.i 0 .47 24 6.4 0 .54 43 0 .019 4.9 0 .0020 .27 -
echo_false-no-overflow.i 0 900    330 12000   0 .50 41 0 .019 4.9 0 .0013 .27 -
expand_false-no-overflow.i 0 .58 30 6.4 0 .53 41 0 .019 4.9 0 .0015 .26 -
fold_false-no-overflow.i 0 .43 19 5.3 0 .65 43 0 .022 4.8 0 .0013 .27 -
head_false-no-overflow.i 0 .35 16 5.3 0 .58 41 0 .029 4.9 0 .0016 .28 -
logname_false-no-overflow.i 0 900    130 13000   0 .55 41 0 .024 5.0 0 .0011 .26 -
ls-incomplete_false-no-overflow.i 0 .98 64 11   0 .57 43 0 .019 4.9 0 .0013 .29 -
mkdir_false-no-overflow.i 0 .44 19 4.6 0 .58 43 0 .019 4.9 0 .0013 .26 -
mkfifo-incomplete_false-no-overflow.i 0 900    220 13000   0 .52 42 0 .019 5.0 0 .0013 .29 -
od_false-no-overflow.i 0 .91 65 10   0 .55 43 0 .018 4.9 0 .0015 .26 -
printf_false-no-overflow.i 0 .27 13 2.9 0 .54 41 0 .019 4.9 0 .0013 .26 -
readlink_false-no-overflow.i 0 .37 17 4.4 0 .54 41 0 .019 5.0 0 .0012 .29 -
realpath_false-no-overflow.i 0 900    400 14000   0 .40 41 0 .029 4.8 0 .0016 .26 -
rm_false-no-overflow.i 0 .46 21 5.5 0 .69 45 0 .023 4.8 0 .0013 .28 -
seq_false-no-overflow.i 0 .25 13 2.8 0 .41 44 0 .029 4.9 0 .0013 .26 -
sleep_false-no-overflow.i 0 .24 12 3.0 0 .66 42 0 .018 4.8 0 .0015 .26 -
stty_false-no-overflow.i 0 900    370 13000   0 .51 41 0 .025 4.9 0 .0020 .27 -
sync_false-no-overflow.i 0 900    150 15000   0 .53 41 0 .021 4.9 0 .0012 .34 -
tac_false-no-overflow.i 0 .39 16 4.0 0 .55 43 0 .019 5.0 0 .0013 .30 -
tee_false-no-overflow.i 0 .38 16 5.3 0 .50 41 0 .023 4.8 0 .0017 .27 -
test-incomplete_false-no-overflow.i 0 .41 18 5.0 0 .54 41 0 .019 4.8 0 .0016 .26 -
touch_false-no-overflow.i 0 .52 26 5.6 0 .54 42 0 .049 4.8 0 .0012 .26 -
uname_false-no-overflow.i 0 .57 78 5.8 0 .51 41 0 .019 4.8 0 .0012 .35 -
uniq_false-no-overflow.i 0 .41 19 5.6 0 .53 42 0 .019 4.9 0 .0014 .28 -
usleep_false-no-overflow.i 0 900    97 12000   0 .58 44 0 .019 4.8 0 .0015 .27 -
uudecode_false-no-overflow.i 0 .51 23 5.8 0 .54 43 0 .019 4.9 0 .0015 .26 -
wc_false-no-overflow.i 0 .42 18 4.7 0 .43 43 0 .020 4.8 0 .0015 .28 -
who_false-no-overflow.i 0 .40 19 5.1 0 .56 42 0 .018 4.9 0 .0013 .26 -
whoami-incomplete_false-no-overflow.i - 0 .53 43 0 .018 4.8 0 .0014 .27 -
yes_false-no-overflow.i 0 900    140 12000   0 .56 43 0 .019 4.9 0 .0015 .26 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900    130 11000   - - - 0 .018 5.0
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 900    320 12000   - - - 0 .018 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900    210 13000   - - - 0 .019 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .48 23 5.4 - - - 0 .033 4.9
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .62 33 7.9 - - - 0 .019 4.8
dirname_true-no-overflow_true-valid-memsafety.i 0 900    790 11000   - - - 0 .019 4.8
du_true-no-overflow_true-valid-memsafety.i 0 .49 24 6.5 - - - 0 .020 4.9
echo_true-no-overflow_true-valid-memsafety.i 0 900    320 11000   - - - 0 .019 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .59 30 7.9 - - - 0 .018 4.9
fold_true-no-overflow_true-valid-memsafety.i 0 .41 19 4.4 - - - 0 .020 4.9
head_true-no-overflow_true-valid-deref.i 0 .38 16 4.9 - - - 0 .018 4.9
hostid_true-no-overflow_true-valid-memsafety.i 0 900    980 13000   - - - 0 .023 4.8
logname_true-no-overflow_true-valid-memsafety.i 0 900    140 14000   - - - 0 .022 5.0
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .97 63 14   - - - 0 .019 4.9
mkdir_true-no-overflow_true-valid-memsafety.i 0 .41 18 5.7 - - - 0 .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 900    230 12000   - - - 0 .019 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .89 65 12   - - - 0 .018 4.9
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .28 13 2.8 - - - 0 .019 5.0
readlink_true-no-overflow_true-valid-memsafety.i 0 .40 17 4.2 - - - 0 .022 4.8
realpath_true-no-overflow_true-valid-memsafety.i 0 900    400 13000   - - - 0 .020 5.0
rm_true-no-overflow_true-valid-memsafety.i 0 .46 21 5.2 - - - 0 .019 4.9
seq_true-no-overflow_true-valid-memsafety.i 0 .23 13 2.9 - - - 0 .020 5.0
sleep_true-no-overflow_true-valid-deref.i 0 .23 12 3.0 - - - 0 .020 4.9
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900    210 14000   - - - 0 .018 4.8
sync_true-no-overflow_true-valid-memsafety.i 0 900    150 12000   - - - 0 .018 4.9
tac_true-no-overflow_true-valid-memsafety.i 0 .36 16 4.1 - - - 0 .023 4.8
tee_true-no-overflow_true-valid-memsafety.i 0 .36 16 4.7 - - - 0 .018 5.0
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .38 18 5.1 - - - 0 .019 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .55 26 5.6 - - - 0 .019 4.9
uname_true-no-overflow_true-valid-memsafety.i 0 .58 77 6.7 - - - 0 .019 5.0
uniq_true-no-overflow_true-valid-memsafety.i 0 .41 18 4.5 - - - 0 .024 4.8
usleep_true-no-overflow_true-valid-memsafety.i 0 900    98 13000   - - - 0 .019 4.8
uudecode_true-no-overflow_true-valid-memsafety.i 0 .53 22 5.4 - - - 0 .019 5.0
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 .41 18 5.6 - - - 0 .019 4.9
who_true-no-overflow_true-valid-memsafety.i 0 .43 19 5.1 - - - 0 .018 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 900    940 11000   - - - 0 .020 4.9
yes_true-no-overflow_true-valid-memsafety.i 0 900    130 12000   - - - 0 .020 5.0
sv-benchmarks/c/busybox-1.22.0/ 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 70 0 22000 8600 300000 34 0 18 1400 34 0 .73 170 34 0 .049 9.4 37 0 .73 180
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 0 0 0 0 0
Run set symbiotic.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows