Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
chgrp-incomplete_false-no-overflow.i unknown 0 --- inspect 900 900 800 11000 280 .0041 error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .61 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .53 0   0   - --- inspect
chroot-incomplete_false-no-overflow.i unknown 0 --- inspect 900 900 1700 9200 290 0      error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0   error (invalid witness file) 0 --- inspect .97 .63 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0   0   - --- inspect
cut_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 270 21 0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0   error (invalid witness file) 0 --- inspect .0054 .0068 .53 0   0   - --- inspect
date_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 340 21 0      error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .023 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .91 .60 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0024 .53 0   0   - --- inspect
du_false-no-overflow.i out of memory 0 --- inspect 23 22 15000 310 21 0      error (invalid witness file) 0 --- inspect .61 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0038 .0048 .52 0   0   - --- inspect
echo_false-no-overflow.i unknown 0 --- inspect 900 900 1600 9700 290 0      error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .024 .025 5.8 0   0   error (invalid witness file) 0 --- inspect .93 .60 48 0   0   error (invalid witness file) 0 --- inspect .0036 .0046 .53 0   0   - --- inspect
expand_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 290 18 0      error (invalid witness file) 0 --- inspect .79 .48 41 0   0   error (2) 0 --- inspect .021 .022 5.8 0   0   error (invalid witness file) 0 --- inspect .91 .60 48 0   0   error (invalid witness file) 0 --- inspect .0029 .0037 .53 0   0   - --- inspect
fold_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 270 18 0      error (invalid witness file) 0 --- inspect .64 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0   error (invalid witness file) 0 --- inspect .96 .61 48 0   0   error (invalid witness file) 0 --- inspect .0044 .0054 .53 0   0   - --- inspect
head_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 270 21 0      error (invalid witness file) 0 --- inspect .65 .41 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .63 48 0   0   error (invalid witness file) 0 --- inspect .0053 .0067 .53 0   0   - --- inspect
logname_false-no-overflow.i witness invalid (false(no-overflow)) 0 --- inspect 190 190 640 2500 310 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .64 48 0   0   error (invalid witness file) 0 --- inspect .0065 .0085 .41 0   0   - --- inspect
ls-incomplete_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 260 21 0      error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .023 .025 5.7 0   0   error (invalid witness file) 0 --- inspect .96 .63 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0070 .40 0   0   - --- inspect
mkdir_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 270 21 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .90 .59 47 0   0   error (invalid witness file) 0 --- inspect .0039 .0053 .40 0   0   - --- inspect
mkfifo-incomplete_false-no-overflow.i unknown 0 --- inspect 900 900 2000 11000 290 0      error (invalid witness file) 0 --- inspect .68 .42 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .62 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .52 0   0   - --- inspect
od_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 280 21 0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0   error (invalid witness file) 0 --- inspect .0050 .0060 .40 0   0   - --- inspect
printf_false-no-overflow.i unknown 0 --- inspect 900 900 4000 7100 52 0      error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .022 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .63 48 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0   0   - --- inspect
readlink_false-no-overflow.i out of memory 0 --- inspect 23 22 15000 270 18 0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .53 0   0   - --- inspect
realpath_false-no-overflow.i unknown 0 --- inspect 900 900 2100 7800 290 0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .61 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .52 0   0   - --- inspect
rm_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 260 21 0      error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0   error (invalid witness file) 0 --- inspect .0064 .0081 .53 0   0   - --- inspect
seq_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 280 21 0      error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0074 .54 0   0   - --- inspect
sleep_false-no-overflow.i unknown 0 --- inspect 890 900 670 9900 52 0      error (invalid witness file) 0 --- inspect .68 .41 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .60 48 0   0   error (invalid witness file) 0 --- inspect .0025 .0028 .40 0   0   - --- inspect
stty_false-no-overflow.i out of memory 0 --- inspect 23 23 15000 260 21 0      error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (2) 0 --- inspect .023 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .93 .62 48 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0   0   - --- inspect
sync_false-no-overflow.i unknown 0 --- inspect 900 900 840 13000 680 0      error (invalid witness file) 0 --- inspect .66 .39 41 0   0   error (2) 0 --- inspect .023 .024 5.8 0   0   error (invalid witness file) 0 --- inspect .95 .63 48 0   0   error (invalid witness file) 0 --- inspect .0049 .0063 .40 0   0   - --- inspect
tac_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 260 21 .0041 error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .60 47 0   0   error (invalid witness file) 0 --- inspect .0047 .0058 .54 0   0   - --- inspect
tee_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 300 21 0      error (invalid witness file) 0 --- inspect .64 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .62 49 0   0   error (invalid witness file) 0 --- inspect .0056 .0078 .50 0   0   - --- inspect
test-incomplete_false-no-overflow.i unknown 0 --- inspect 900 900 15000 7800 52 0      error (invalid witness file) 0 --- inspect .56 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .53 0   0   - --- inspect
touch_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 320 21 0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect 1.1  .71 48 0   0   error (invalid witness file) 0 --- inspect .0061 .0083 .53 0   0   - --- inspect
uname_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 300 21 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0065 .40 0   0   - --- inspect
uniq_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 250 21 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .60 48 0   0   error (invalid witness file) 0 --- inspect .0023 .0029 .53 0   0   - --- inspect
usleep_false-no-overflow.i unknown 0 --- inspect 900 900 760 11000 660 0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0   error (invalid witness file) 0 --- inspect .0023 .0029 .52 0   0   - --- inspect
uudecode_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 270 21 0      error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0   error (invalid witness file) 0 --- inspect .96 .61 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0022 .53 0   0   - --- inspect
wc_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 260 21 0      error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .64 49 0   0   error (invalid witness file) 0 --- inspect .0061 .0084 .53 0   0   - --- inspect
who_false-no-overflow.i out of memory 0 --- inspect 22 22 15000 300 21 0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0   0   error (invalid witness file) 0 --- inspect .93 .59 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .41 0   0   - --- inspect
whoami-incomplete_false-no-overflow.i unknown 0 --- inspect 900 900 1000 11000 770 .0041 error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0079 .52 0   0   - --- inspect
yes_false-no-overflow.i witness invalid (false(no-overflow)) 0 --- inspect 190 190 860 2000 290 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .93 .60 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0079 .53 0   0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 660 10000 350 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 --- inspect 900 900 800 10000 320 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .025 5.6 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1600 10000 270 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 280 18 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 250 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
dirname_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1800 10000 1100 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
du_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 250 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
echo_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1600 11000 290 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 270 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
fold_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 260 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.7 0   0  
head_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 22 15000 270 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
hostid_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1800 10000 1200 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i false(no-overflow) -16 --- inspect 220 220 860 2200 310 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 310 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 22 15000 260 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0   0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 2000 9400 270 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 23 15000 300 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.8 0   0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 3500 7800 52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .025 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 330 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 2100 7600 290 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
rm_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 22 15000 260 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 290 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
sleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 890 900 680 10000 50 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 23 15000 250 18 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
sync_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 870 11000 690 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
tac_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 22 15000 300 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .056 .057 5.5 0   0  
tee_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 280 18 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.7 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 15000 8000 52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 23 15000 300 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
uname_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 270 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
uniq_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23 22 15000 330 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 810 11000 630 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 260 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 240 18 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .024 5.6 0   0  
who_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22 22 15000 260 21 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 920 12000 770 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
yes_true-no-overflow_true-valid-memsafety.i false(no-overflow) -16 --- inspect 170 170 850 1800 270 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 71 -32 24000 24000 700000 270000 12000 .029 34 0 22 14 1400 0   0   34 0 .74 .77 190 0   0   34 0 32 21 1600 0   0   34 0 .13 .17 17 0   0   37 0 .84 .88 210 0   0  
    correct results 0 0 0 0 0 0
        correct true 0 0 0 0 0 0
        correct false 0 0 0 0 0 0
    incorrect results 2 -32 390 390 1700 4100 570 0     0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 2 -32 390 390 1700 4100 570 0     0 0 0 0 0
score (71 tasks, max score: 108) -32 0 0 0 0 0
Run set depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows