Tool VeriAbs 1.3.10 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 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*
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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap
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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ 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) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i 1 330   320   10000 3200 .95 0      -32 6.4  3.5  260 0   0      0 19     11     340   .71 0      0 5.1  2.8  270 0     0      1 .68   .68   21    .11  0      - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 340   320   1300 3700 2.1  0      -32 6.2  3.3  270 0   0      0 20     12     330   .75 0      0 5.0  2.8  260 0     0      -32 .72   .72   22    .094 0      - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 340   320   550 4100 .88 0      1 4.7  2.6  260 0   0      0 17     9.7   330   .75 0      0 4.2  2.4  250 0     0      1 .63   .63   20    .082 0      - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 1 230   220   3200 2300 .82 .32   -32 5.7  3.1  260 0   0      0 21     12     310   .75 0      0 5.2  2.9  260 0     0      1 .67   .66   21    .082 0      - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 110   92   760 1400 .51 .0041 0 4.6  2.6  270 0   0      0 16     9.0   310   .68 0      0 4.6  2.6  250 0     0      1 .63   .63   21    .074 .025  - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 1 110   93   760 1200 .52 0      0 4.8  2.6  260 0   0      0 19     11     300   .75 0      0 5.0  2.9  260 0     0      1 .63   .65   21    .074 0      - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 660   640   10000 6600 1.2  .0041 - - - - 0 .57 .35 40 0   0      0 .025 .025 5.6 0    0     
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900   890   2700 9300 .66 0      - - - - 0 .58 .35 40 0   0      0 .020 .021 5.6 0    0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 540   520   1300 6300 1.8  0      - - - - 0 .79 .48 42 0   0      0 .020 .021 5.6 0    0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 560   540   3300 6600 1.1  0      - - - - 0 .63 .38 40 0   0      0 .021 .021 5.6 0    0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 730   720   4000 4500 .99 0      - - - - 0 .59 .37 41 0   0      0 .020 .021 5.7 0    0     
heap-manipulation/tree_true-unreach-call.i 0 900   890   1600 9600 .71 0      - - - - 0 .61 .39 40 0   0      0 .024 .025 5.6 0    0     
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 24   8.6 280 200 .50 .0041 1 5.6  3.0  260 0   0      1 9.8   5.6   310   .66 0      0 4.3  2.5  260 0     0      1 .62   .62   20    .066 0      - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 1 150   140   600 2100 .58 .29   -32 6.4  3.5  280 0   0      0 56     36     7000   .70 0      0 6.4  3.5  280 0     0      1 .71   .71   22    .066 0      - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 22   7.9 290 170 .46 .0041 1 5.4  3.0  260 0   0      1 8.8   4.8   310   .66 0      0 4.3  2.4  250 0     0      1 .62   .62   21    .066 0      - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 18   6.6 280 150 .46 0      -32 6.1  3.3  260 0   0      -32 9.8   5.9   340   .66 0      0 5.2  2.9  250 0     .47   1 .61   .61   21    .070 0      - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 22   8.2 280 160 .45 0      1 4.5  2.4  260 0   .025  1 11     6.0   310   .66 0      0 4.1  2.4  250 0     0      1 .63   .63   20    .066 0      - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 31   16   290 310 .49 0      1 5.3  2.9  270 0   0      1 8.5   4.7   320   .62 0      0 4.2  2.4  250 0     0      1 .62   .62   21    .070 0      - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900   890   5200 8000 .72 0      - - - - 0 .65 .43 40 0   0      0 .020 .021 5.7 0    0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900   890   3300 8100 .70 0      - - - - 0 .70 .43 42 0   0      0 .020 .021 5.6 0    0     
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 77   40   1100 650 140    0      - - - - 2 26    16    620 0   0      2 110     96     780   .62 0     
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 900   890   13000 8800 .63 .0082 - - - - 0 .72 .45 40 0   0      0 .021 .021 5.6 0    0     
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 830   810   5900 8100 .95 .025  - - - - 0 .76 .46 40 0   0      0 .024 .024 5.6 0    0     
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900   890   6100 10000 .64 .27   - - - - 0 .59 .36 40 0   0      0 .020 .021 5.6 0    0     
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900   880   5000 9000 .65 0      - - - - 0 .73 .45 41 0   0      0 .021 .022 5.6 0    0     
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 8.9 3.5 270 85 .12 0      1 4.0  2.2  250 0   0      1 8.6   5.1   310   .66 0      1 4.6  2.6  250 0     0      1 .58   .58   20    .057 0      - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 22   7.6 280 170 .53 0      1 5.4  2.9  250 0   0      1 9.6   5.4   330   .66 0      0 4.2  2.4  250 0     0      1 .68   .68   20    .086 0      - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 1 8.7 3.4 270 70 .11 .0041 1 3.7  2.0  250 0   0      1 6.5   3.8   300   .66 0      1 4.1  2.4  240 0     0      1 .59   .59   20    .045 0      - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 22   7.4 280 160 .50 0      -32 4.4  2.4  250 0   0      0 16     9.1   320   .75 0      0 4.4  2.5  250 0     0      1 .67   .67   20    .074 0      - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 8.6 3.5 270 73 .11 0      1 3.6  2.0  250 0   0      1 8.4   4.6   300   .66 0      1 4.6  2.6  250 0     0      1 .60   .60   20    .049 0      - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 8.7 3.5 270 68 .11 .0041 1 3.7  2.1  250 0   0      1 7.5   4.2   310   .66 0      1 3.8  2.2  250 0     0      1 .56   .56   20    .045 0      - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 9.0 3.6 270 75 .12 .0041 1 3.8  2.2  250 0   0      1 7.4   4.1   310   .66 0      1 3.6  2.1  250 0     0      1 .57   .57   20    .049 0      - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 1 9.8 3.8 280 81 .12 0      1 4.2  2.3  260 0   0      1 10     6.1   320   .66 .0041 0 3.9  2.2  250 0     0      1 .59   .60   20    .061 0      - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 21   7.1 290 170 .46 0      1 4.8  2.6  260 0   0      1 13     7.2   480   .66 0      0 4.2  2.4  250 0     .020  1 .63   .63   21    .078 0      - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 16   6.1 280 130 .38 .16   1 4.4  2.4  260 0   0      1 8.3   4.6   310   .66 0      1 4.1  2.3  250 0     0      1 .58   .58   21    .057 0      - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 14   5.0 270 110 .32 .020  1 4.4  2.4  250 0   .0041 1 7.5   4.2   300   .66 0      1 3.9  2.2  250 0     0      1 .59   .58   20    .045 0      - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 13   4.8 280 89 .23 .0041 1 4.1  2.3  250 0   0      1 6.8   4.3   300   .66 0      1 3.5  2.0  240 0     .0041 1 .57   .58   20    .045 .0041 - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 14   6.5 460 110 150    .0041 - - - - 2 3.4  1.9  250 0   0      2 7.7   4.8   310   .66 0     
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 13   6.4 470 120 140    0      - - - - 2 4.6  2.6  250 0   0      2 8.1   4.5   310   .66 0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 14   6.5 450 110 150    .0041 - - - - 2 3.6  2.0  250 0   0      2 7.6   4.3   310   .66 0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 13   6.4 450 120 140    0      - - - - 2 3.5  2.0  250 0   0      2 8.1   4.8   310   .66 0     
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 43   19   930 380 140    .11   - - - - 2 15    8.9  480 0   0      2 97     78     810   .62 0     
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 12   6.3 440 110 150    0      - - - - 2 4.2  2.3  240 0   0      2 7.9   4.7   290   .66 0     
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 14   6.6 470 110 140    .27   - - - - 2 4.3  2.4  250 0   .0041 2 8.0   5.0   310   .62 0     
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 14   6.6 460 120 150    0      - - - - 2 4.3  2.4  250 0   0      2 7.7   4.7   310   .62 0     
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 12   6.3 440 110 140    0      - - - - 2 3.3  1.9  250 0   0      2 8.4   5.0   310   .62 0     
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 14   6.5 480 130 140    0      - - - - 2 3.7  2.1  250 0   0      2 7.9   4.5   310   .62 0     
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 16   7.7 580 130 150    0      - - - - 2 4.9  2.7  250 0   0      2 7.1   4.0   300   .66 0     
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 16   7.6 500 140 150    0      - - - - 2 4.1  2.3  250 0   0      2 7.8   4.9   310   .66 0     
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 15   6.7 470 120 150    0      - - - - 2 3.7  2.1  250 0   0      2 8.7   5.1   310   .66 0     
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 14   6.8 450 110 150    0      - - - - 2 4.5  2.5  250 0   0      2 7.1   4.5   310   .66 0     
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 13   6.5 450 120 150    0      - - - - 2 4.4  2.5  250 0   0      2 7.8   4.8   310   .66 0     
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 13   6.6 460 110 150    0      - - - - 2 4.9  2.7  250 0   .0041 2 7.1   4.5   310   .66 0     
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 16   7.4 450 150 150    0      - - - - 2 5.0  2.8  260 0   0      2 10     6.1   330   .66 .0041
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 36   15   840 340 140    0      - - - - 2 5.1  2.8  260 0   0      2 20     13     650   .62 0     
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 24   10   520 220 140    .0041 - - - - 2 4.3  2.4  260 0   .016  2 12     7.0   400   .62 0     
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 24   10   440 180 150    0      - - - - 2 5.1  2.8  250 0   0      2 9.3   5.4   310   .62 0     
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 12   6.3 440 100 150    0      - - - - 2 3.9  2.2  250 0   0      2 8.0   4.5   310   .66 0     
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 17   7.7 450 150 150    0      - - - - 2 4.2  2.3  250 0   0      2 9.1   5.4   310   .66 0     
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 13   6.3 460 130 140    0      - - - - 2 4.5  2.5  250 0   0      2 8.2   4.9   310   .66 0     
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 23   9.9 450 180 140    .43   - - - - 2 3.9  2.2  260 0   0      2 8.1   4.6   310   .62 0     
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 23   9.8 450 200 140    0      - - - - 2 4.5  2.5  260 0   0      2 8.4   5.1   320   .66 0     
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 19   8.4 450 150 140    .0041 - - - - 2 5.2  2.9  260 0   .033  2 8.7   4.8   320   .66 0     
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 12   6.3 470 110 140    .0041 - - - - 2 4.4  2.5  250 0   0      2 7.0   4.5   310   .66 0     
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 13   6.5 470 120 140    0      - - - - 2 4.6  2.6  250 0   0      2 7.2   4.6   310   .66 0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 13   6.3 450 100 150    .0041 - - - - 2 4.2  2.4  250 0   0      2 6.9   4.0   310   .66 0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 13   6.4 470 110 150    0      - - - - 2 3.5  2.0  250 0   0      2 7.2   4.5   310   .66 0     
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 13   6.3 470 100 150    .0041 - - - - 2 4.2  2.4  250 0   0      2 7.1   4.0   290   .66 0     
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 13   6.5 470 110 140    0      - - - - 2 3.6  2.0  250 0   0      2 6.8   3.9   300   .62 0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 13   6.6 470 99 140    0      - - - - 2 4.4  2.5  250 0   0      2 6.6   3.8   310   .66 0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 13   6.4 460 120 150    0      - - - - 2 3.4  1.9  250 0   0      2 7.7   4.6   310   .66 0     
ldv-regression/test02_false-unreach-call_true-termination.c 1 8.8 3.6 270 77 .11 .016  1 3.7  2.0  250 0   0      1 6.9   3.9   310   .66 0      1 3.8  2.2  260 0     .0041 1 .57   .57   20    .045 0      - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 8.4 3.4 270 72 .11 .0041 -32 3.9  2.2  250 0   0      1 8.4   4.7   310   .66 0      1 3.8  2.1  250 0     0      1 .62   .64   20    .057 0      - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 8.9 3.5 270 69 .11 0      1 4.5  2.5  250 0   0      1 8.0   4.5   310   .66 0      1 3.5  2.0  250 0     .0041 1 .57   .57   20    .045 0      - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 8.8 3.5 270 84 .11 .0082 1 3.9  2.2  250 0   0      1 6.7   3.9   310   .62 .0041 1 3.4  2.0  250 0     0      1 .58   .58   20    .045 0      - -
ldv-regression/test21_false-unreach-call_true-termination.c 1 9.4 3.6 280 82 .11 .0041 1 4.5  2.5  250 0   0      1 7.0   4.0   310   .66 0      0 4.2  2.5  250 0     0      1 .58   .58   20    .057 .0041 - -
ldv-regression/test22_false-unreach-call.c 1 13   4.8 280 100 .29 .016  1 4.4  2.4  260 0   0      1 11     6.2   400   .66 0      0 3.6  2.1  240 0     0      -32 .59   .59   21    .057 0      - -
ldv-regression/test23_false-unreach-call.c 1 24   13   300 270 .34 .012  1 4.6  2.6  270 0   0      0 98     62     7000   1.5  0      0 5.0  2.9  250 0     .0041 -32 .60   .59   21    .057 0      - -
ldv-regression/test24_false-unreach-call.c 1 22   8.7 330 190 .36 0      1 5.9  3.4  270 0   .0041 0 83     52     7000   .68 0      0 3.9  2.2  250 0     0      -32 .61   .61   21    .057 0      - -
ldv-regression/test25_false-unreach-call_true-termination.c 1 27   14   310 240 .36 .0041 1 6.1  3.4  280 0   0      0 97     74     3300   .63 0      0 4.2  2.4  270 0     0      -32 .62   .61   21    .057 .0041 - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 7.9 3.3 270 70 .11 0      1 4.0  2.2  250 0   0      1 7.9   4.4   310   .66 0      1 3.7  2.2  250 0     0      1 .57   .56   20    .045 0      - -
ldv-regression/test27_false-unreach-call_true-termination.c 1 22   9.0 300 180 .37 .0041 1 5.4  3.0  270 0   0      0 87     55     7000   .68 0      0 3.9  2.3  250 0     0      0 .58   .58   21    .057 0      - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 8.7 3.5 280 75 .11 0      1 3.7  2.1  250 0   0      1 7.6   4.3   310   .66 0      -32 3.4  2.0  250 0     0      1 .59   .59   20    .049 .0041 - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 7.6 3.1 270 74 .11 .0041 1 4.9  2.7  250 0   0      1 9.7   5.6   310   .66 0      1 3.5  2.1  250 0     0      1 .57   .57   20    .049 0      - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 8.7 3.5 270 76 .11 0      1 4.4  2.5  260 0   0      1 7.3   4.2   310   .66 0      1 4.6  2.6  250 0     0      1 .57   .57   20    .049 0      - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 13   6.6 460 110 150    0      - - - - 2 3.5  1.9  250 0   0      2 7.1   4.1   310   .66 0     
ldv-regression/test03_true-unreach-call_true-termination.c 2 13   6.7 470 110 150    0      - - - - 2 4.2  2.4  250 0   0      2 9.2   5.5   310   .66 0     
ldv-regression/test04_true-unreach-call_true-termination.c 2 14   6.5 480 130 170    0      - - - - 2 3.8  2.1  250 0   0      2 7.6   4.3   310   .66 0     
ldv-regression/test05_true-unreach-call_true-termination.c 2 18   8.1 680 140 140    .0041 - - - - 2 4.1  2.2  250 0   0      2 12     6.7   330   .66 0     
ldv-regression/test07_true-unreach-call_true-termination.c 2 15   7.3 520 130 140    0      - - - - 2 4.2  2.4  250 0   0      2 9.4   5.8   320   .66 0     
ldv-regression/test09_true-unreach-call_true-termination.c 2 15   7.2 500 140 150    0      - - - - 2 3.6  2.0  260 0   0      2 10     5.5   320   .66 0     
ldv-regression/test10_true-unreach-call_true-termination.c 2 20   9.0 650 200 140    0      - - - - 2 3.7  2.1  260 0   0      2 11     6.5   440   .66 0     
ldv-regression/test11_true-unreach-call_true-termination.c 2 14   6.8 460 130 140    .0041 - - - - 2 4.2  2.4  260 0   0      2 8.5   5.2   310   .66 0     
ldv-regression/test13_true-unreach-call_true-termination.c 2 14   6.6 460 110 150    0      - - - - 2 4.1  2.3  250 0   0      2 7.9   4.5   320   .66 0     
ldv-regression/test14_true-unreach-call_true-termination.c 2 14   6.7 460 110 170    0      - - - - 2 3.6  2.0  250 0   0      2 8.0   4.5   310   .66 0     
ldv-regression/test15_true-unreach-call_true-termination.c 2 14   6.8 460 120 140    0      - - - - 2 3.8  2.1  250 0   .0041 2 8.4   4.7   310   .66 0     
ldv-regression/test16_true-unreach-call_true-termination.c 2 14   6.7 480 140 140    0      - - - - 2 3.4  1.9  250 0   0      2 8.4   4.9   310   .66 0     
ldv-regression/test17_true-unreach-call_true-termination.c 2 13   6.4 450 120 150    .0041 - - - - 2 4.3  2.5  250 0   0      2 7.2   4.6   310   .66 0     
ldv-regression/test18_true-unreach-call_true-termination.c 2 15   7.1 460 120 140    0      - - - - 2 3.6  2.0  250 0   0      2 8.0   4.5   310   .66 0     
ldv-regression/test19_true-unreach-call_true-termination.c 2 16   7.3 510 160 140    0      - - - - 2 4.7  2.7  250 0   0      2 8.7   4.9   310   .66 0     
ldv-regression/test20_true-unreach-call_true-termination.c 2 14   6.8 470 120 150    0      - - - - 2 4.6  2.6  250 0   0      2 7.7   4.3   300   .66 0     
ldv-regression/test21_true-unreach-call_true-termination.c 2 15   7.0 490 130 140    0      - - - - 2 4.7  2.6  250 0   0      2 9.2   5.6   310   .66 0     
ldv-regression/test22_true-unreach-call.c 2 28   14   820 290 140    0      - - - - 2 8.2  4.7  320 0   0      2 22     14     660   .62 0     
ldv-regression/test23_true-unreach-call.c 2 66   38   740 650 140    6.3    - - - - 2 9.7  5.8  330 0   0      2 67     59     610   .62 0     
ldv-regression/test24_true-unreach-call_true-termination.c 2 21   8.9 580 170 150    0      - - - - 2 8.3  4.6  310 0   0      2 27     22     470   .62 0     
ldv-regression/test25_true-unreach-call.c 2 47   28   690 490 140    .13   - - - - 0 4.8  2.7  260 0   0      0 10     6.0   280   .74 0     
ldv-regression/test26_true-unreach-call_true-termination.c 2 15   6.9 480 120 140    .0041 - - - - 2 4.2  2.4  250 0   0      2 8.5   4.8   310   .66 0     
ldv-regression/test27_true-unreach-call_true-termination.c 2 75   50   780 780 150    .057  - - - - 2 29    22    550 0   0      2 86     70     840   .62 0     
ldv-regression/test28_true-unreach-call_true-termination.c 2 14   6.8 470 140 140    0      - - - - 2 4.4  2.5  250 0   0      2 8.7   5.0   310   .66 0     
ldv-regression/test29_true-unreach-call_true-termination.c 2 12   6.5 440 120 140    0      - - - - 2 4.5  2.5  250 0   0      2 8.7   5.4   320   .62 0     
ldv-regression/test30_true-unreach-call_true-termination.c 2 17   8.3 620 160 170    0      - - - - 2 4.8  2.7  260 0   0      2 10     6.2   340   .66 0     
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 0 14   4.9 240 120 .17 0      0 .66 .41 41 0   0      0 .024 .025 5.6 0    0      0 1.2  .78 48 0     0      0 .0048 .0058 .54 0     0      - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 15   4.9 250 130 .14 0      0 .72 .46 40 0   0      0 .021 .022 5.6 0    0      0 1.2  .75 47 0     0      0 .0020 .0026 .53 0     0      - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 15   5.0 240 130 .17 0      0 .58 .35 41 0   0      0 .024 .025 5.7 0    0      0 .90 .59 47 0     0      0 .0019 .0036 .54 0     0      - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 34   12   630 300 150    0      - - - - 2 7.6  4.0  290 0   0      0 27     15     530   .75 0     
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 34   12   650 270 140    .0082 - - - - 2 8.4  4.4  300 0   0      0 27     15     530   .75 0     
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 33   12   640 270 150    0      - - - - 2 9.2  4.9  290 0   0      0 27     15     520   .71 0     
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 33   12   620 260 150    0      - - - - 2 9.1  4.8  310 0   0      0 27     15     540   .75 0     
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 35   12   650 260 150    0      - - - - 2 8.4  4.4  300 0   .086  0 30     17     530   .75 0     
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 34   12   610 280 150    0      - - - - 2 12    6.0  310 0   0      0 27     15     510   .71 0     
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 33   12   620 250 150    0      - - - - 2 9.7  5.1  290 0   0      0 27     15     520   .75 0     
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 33   12   620 310 150    0      - - - - 2 7.9  4.2  300 0   0      0 27     15     520   .75 0     
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 33   12   620 280 150    0      - - - - 2 7.9  4.2  290 0   .086  0 27     16     530   .71 0     
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 33   12   660 270 150    0      - - - - 2 7.8  4.1  300 0   0      0 28     16     520   .75 0     
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 27   10   280 220 .84 .0041 -32 4.4  2.4  250 0   0      0 15     8.6   300   .75 0      0 4.0  2.4  250 0     .070  1 .63   .63   20    .074 0      - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 32   17   270 300 .52 0      0 4.8  2.6  260 0   0      0 15     8.2   310   .75 0      0 4.3  2.5  250 0     0      1 .63   .63   20    .070 0      - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 22   7.7 280 180 .48 0      1 4.8  2.6  260 0   0      0 15     8.7   310   .71 0      0 4.1  2.4  250 0     0      1 .63   .63   20    .070 0      - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 25   8.3 280 180 .58 0      -32 5.0  2.7  260 0   0      0 16     9.5   310   .68 .025  0 4.4  2.5  260 0     0      1 .64   .65   20    .074 .025  - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 230   210   2000 2300 .61 .0082 -32 4.5  2.4  260 0   0      0 20     12     310   .75 0      0 4.2  2.4  250 0     0      1 .63   .63   20    .074 0      - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 260   240   2200 2800 .72 .18   -32 4.5  2.5  260 0   0      0 21     13     320   .71 0      0 4.3  2.4  250 0     .25   -32 .64   .64   20    .074 0      - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 28   13   280 250 .49 0      1 5.3  2.9  260 0   0      0 14     8.4   310   .75 0      0 4.4  2.5  250 0     0      1 .63   .63   21    .070 0      - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 30   13   290 260 .57 0      -32 5.9  3.2  270 0   0      0 18     11     300   .75 0      0 5.4  3.0  260 0     0      1 .63   .63   21    .074 0      - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 25   11   280 230 .51 0      0 4.3  2.4  260 0   0      0 18     10     310   .75 0      0 5.3  3.0  250 0     0      1 .64   .64   20    .070 0      - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 28   11   280 220 .84 .0041 -32 5.3  2.9  250 0   .025  0 16     9.3   310   .71 0      0 4.7  2.7  250 0     .18   0 .64   .64   20    .074 0      - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 290   270   350 3100 .84 .0041 -32 4.6  2.5  270 0   0      0 17     11     310   .71 0      0 4.6  2.6  250 0     .11   1 .63   .63   20    .074 0      - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 31   15   280 260 .52 .0082 -32 4.7  2.5  260 0   0      0 17     9.8   310   .75 .025  0 4.3  2.5  260 0     0      1 .62   .62   21    .070 0      - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 22   7.8 280 170 .48 0      1 4.5  2.5  260 0   0      0 15     9.3   310   .71 0      0 5.4  3.1  250 0     0      1 .67   .67   20    .070 0      - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 24   8.2 280 190 .58 0      -32 4.5  2.5  260 0   0      0 19     11     310   .71 0      0 4.4  2.5  260 0     0      1 .63   .63   20    .074 0      - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 210   190   900 1400 .61 14      -32 4.5  2.4  250 0   0      0 15     8.8   310   .75 0      0 4.3  2.5  250 0     .070  1 .63   .63   20    .070 0      - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 0 220   200   970 1600 .64 .0041 -32 4.7  2.6  260 0   0      0 15     8.5   310   .75 0      0 4.9  2.8  250 0     .025  -32 .63   .63   20    .074 .025  - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 24   10   280 190 .48 0      1 4.6  2.5  260 0   0      0 15     8.6   300   .71 0      0 4.3  2.4  260 0     0      1 .63   .63   20    .070 0      - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 27   11   280 220 .54 0      -32 5.4  3.0  260 0   0      0 17     9.7   300   .75 0      0 4.3  2.5  250 0     .070  1 .63   .63   21    .074 0      - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 23   9.1 280 190 .51 .025  -32 4.5  2.4  260 0   0      0 15     9.2   310   .75 0      0 4.9  2.8  250 0     .16   1 .66   .66   20    .070 0      - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900   880   2900 10000 1.3  0      - - - - 0 .59 .36 42 0   0      0 .020 .020 5.6 0    0     
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900   880   8200 8000 .72 0      - - - - 0 .58 .36 41 0   0      0 .023 .024 5.6 0    0     
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900   890   3100 9800 .81 0      - - - - 0 .63 .38 42 0   0      0 .021 .022 5.7 0    0     
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900   880   5500 8200 .95 0      - - - - 0 .74 .45 42 0   0      0 .021 .022 5.6 0    0     
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 680   670   2400 5400 .92 0      - - - - 0 .64 .39 42 0   0      0 .020 .020 5.6 0    0     
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 720   700   2600 4400 .92 0      - - - - 0 .69 .44 41 0   0      0 .020 .020 5.7 0    0     
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900   880   1500 8800 .69 0      - - - - 0 .58 .35 40 0   0      0 .021 .022 5.6 0    0     
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   890   4100 9100 .67 0      - - - - 0 .71 .43 40 0   0      0 .021 .021 5.6 0    0     
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   880   1500 11000 .78 0      - - - - 0 .74 .45 40 0   0      0 .023 .024 5.6 0    0     
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900   890   4600 9500 .69 0      - - - - 0 .59 .36 41 0   0      0 .023 .025 5.7 0    0     
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900   880   2800 9000 1.4  0      - - - - 0 .78 .48 42 0   0      0 .025 .026 5.5 0    0     
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 450   430   350 4900 1.2  0      - - - - 0 .63 .40 41 0   0      0 .022 .022 5.6 0    0     
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900   880   8200 9500 .70 0      - - - - 0 .68 .40 43 0   0      0 .020 .020 5.6 0    0     
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900   890   3000 9300 .73 0      - - - - 0 .74 .44 41 0   0      0 .020 .022 5.6 0    0     
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900   880   5500 9800 .94 0      - - - - 0 .60 .37 40 0   0      0 .021 .021 5.6 0    0     
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 600   590   1000 4100 .83 0      - - - - 0 .62 .37 40 0   0      0 .021 .022 5.6 0    0     
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 620   600   1100 4400 .83 0      - - - - 0 .73 .44 41 0   0      0 .022 .023 5.7 0    0     
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900   880   2700 9700 .70 0      - - - - 0 .57 .34 40 0   0      0 .023 .024 5.6 0    0     
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   890   5500 8400 .70 0      - - - - 0 .63 .40 41 0   0      0 .023 .024 5.6 0    0     
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   880   2100 7700 .84 0      - - - - 0 .64 .38 41 0   0      0 .024 .025 5.6 0    0     
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900   890   5500 8600 .69 0      - - - - 0 .59 .37 41 0   0      0 .025 .026 5.6 0    0     
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 35   19   280 330 .49 0      1 5.4  2.9  250 0   0      1 8.6   4.8   320   .66 0      0 4.4  2.5  260 0     0      1 .63   .63   21    .070 0      - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 28   12   290 230 .52 0      0 98    83    2000 0   0      -32 9.9   5.6   300   .66 0      0 4.2  2.3  250 0     0      0 .63   .63   21    .049 0      - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 1 24   9.0 280 180 .50 .0041 1 5.4  3.0  250 0   0      1 10     5.6   310   .66 0      0 4.2  2.4  260 0     0      1 .65   .65   20    .066 0      - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 1 330   320   2400 2500 .66 0      -32 5.0  2.8  260 0   0      1 20     12     530   .66 0      0 4.3  2.4  260 0     0      0 .71   .70   21    .053 .025  - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 650   630   2400 6700 .82 0      - - - - 0 .59 .37 41 0   0      0 .020 .021 5.6 0    0     
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 330   310   490 4100 .61 0      1 4.7  2.6  260 0   0      1 8.3   5.0   320   .66 0      0 4.9  2.8  260 0     0      1 .66   .66   20    .078 0      - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 520   510   490 5800 .80 .025  - - - - 0 .77 .46 41 0   0      0 .020 .021 5.6 0    0     
list-ext2-properties/simple_search_value_false-unreach-call.i 1 25   9.1 300 180 .52 0      0 97    76    2000 0   0      0 75     47     7000   .62 0      0 4.6  2.5  260 0     0      1 .64   .64   21    .066 0      - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900   880   5400 11000 .59 0      - - - - 0 .75 .46 40 0   0      0 .024 .025 5.6 0    0     
ldv-sets/test_add_false-unreach-call_true-termination.i 1 20   7.1 290 170 .48 .029  1 5.0  2.7  260 0   0      1 8.9   5.0   320   .66 0      0 4.4  2.5  260 0     .11   0 .57   .57   21    .020 0      - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 1 23   9.2 300 180 .52 0      1 6.4  3.4  260 0   0      1 9.6   5.7   360   .66 0      0 4.6  2.6  250 0     0      0 .57   .57   21    .020 0      - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 1 49   34   750 540 .55 0      -32 6.9  3.7  260 0   0      1 13     7.6   530   .66 0      0 4.5  2.5  250 0     0      0 .57   .57   21    .020 0      - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 330   310   1400 3400 .91 0      0 98    68    2200 0   0      0 97     75     4500   1.5  0      0 5.1  130    220 .016 .029  0 .60   .60   23    .020 0      - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 1 47   32   780 480 .55 .0041 -32 6.4  3.4  260 0   .029  1 13     6.8   500   .66 0      0 4.4  2.5  250 0     0      0 .57   .57   21    .020 0      - -
ldv-sets/test_add_true-unreach-call_true-termination.i 2 76   40   820 710 150    0      - - - - 2 6.8  3.8  310 0   0      0 960     950     590   .64 0     
ldv-sets/test_mutex_true-unreach-call.i 2 130   72   1100 1200 150    0      - - - - 2 810    780    3400 0   0      0 960     920     2000   1.5  0     
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 780   750   2000 8800 .91 0      - - - - 0 .75 .45 40 0   0      0 .020 .020 5.6 0    0     
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i 2 140   69   2100 1600 140    61      - - - - 2 17    12    470 0   0      0 960     940     690   .74 0     
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i 2 150   68   1200 1600 150    .025  - - - - 2 18    12    490 0   0      0 960     940     720   .83 0     
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1000 1500 150    .061  - - - - 2 21    15    540 0   0      0 11     6.4   290   .74 0     
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 150   69   1200 1500 140    6.2    - - - - 2 30    22    740 0   0      0 12     6.8   290   .74 0     
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1200 1400 170    0      - - - - 2 14    9.2  450 0   0      0 960     940     650   1.4  0     
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 150   69   1100 1300 150    0      - - - - 2 16    11    480 0   0      0 960     930     790   .70 0     
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 100   69   940 1100 150    6.3    - - - - 2 11    6.7  380 0   0      0 8.4   4.7   290   .66 0     
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i 2 100   68   860 1100 150    6.1    - - - - 2 10    6.3  390 0   0      0 7.2   4.2   280   .66 0     
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 100   68   800 1200 150    0      - - - - 2 17    9.5  590 0   0      0 960     930     1600   .67 0     
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i 2 68   34   1100 700 150    .0041 - - - - 2 14    7.6  480 0   0      2 64     46     830   .62 0     
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i 2 140   69   1100 1400 140    0      - - - - 2 48    37    760 0   0      0 960     940     1000   .71 0     
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i 2 150   69   980 1500 160    6.5    - - - - 2 57    44    830 0   0      0 960     930     1700   .68 0     
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i 2 140   69   1000 1200 150    6.3    - - - - 2 52    39    660 0   0      0 12     7.2   280   .75 0     
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   970 1500 150    0      - - - - 2 64    48    1000 0   0      0 11     6.4   280   .71 0     
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 140   69   1300 1300 140    6.1    - - - - 2 20    13    520 0   0      0 960     930     810   .69 0     
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   1300 1300 140    0      - - - - 2 19    13    510 0   0      0 390     370     690   .68 0     
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 120   69   1100 1100 150    0      - - - - 2 10    5.8  450 0   0      2 72     59     720   .62 0     
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i 2 110   69   980 1100 150    0      - - - - 2 6.8  3.8  310 0   0      2 31     20     650   .62 0     
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 26   10   480 240 150    .025  - - - - 2 16    8.5  510 0   0      2 9.1   5.4   330   .66 0     
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i 2 56   27   820 470 140    0      - - - - 2 13    7.3  470 0   0      2 48     36     730   .62 0     
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1100 1400 150    6.7    - - - - 2 28    21    590 0   0      0 960     940     980   .63 0     
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   930 1500 150    6.1    - - - - 0 15    8.2  540 0   .025  0 960     950     820   .68 0     
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1100 1400 150    6.4    - - - - 2 18    11    520 0   0      0 13     7.4   290   .75 0     
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 150   69   850 1500 150    0      - - - - 0 14    8.0  510 0   0      0 13     7.5   290   .75 0     
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1000 1600 150    0      - - - - 2 25    17    610 0   0      0 960     950     730   .64 0     
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   1000 1200 140    6.1    - - - - 2 28    20    600 0   0      0 960     940     890   1.6  0     
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 110   68   1000 1300 150    0      - - - - 2 20    12    530 0   0      0 12     6.6   290   .75 0     
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i 2 110   68   1000 1000 140    .0041 - - - - 2 21    14    550 0   0      0 6.2   3.8   290   .66 0     
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 52   24   1000 460 140    0      - - - - 2 22    12    580 0   0      2 43     31     580   .62 0     
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i 2 59   30   990 530 140    0      - - - - 2 15    8.4  480 0   0      2 41     30     770   .62 0     
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1000 1500 200    6.5    - - - - 2 35    25    650 0   0      0 960     930     1400   .71 0     
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i 2 150   69   960 1400 140    0      - - - - 2 34    24    730 0   0      0 960     930     1700   .68 .11  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i 2 140   69   1100 1400 140    19      - - - - 2 21    14    560 0   0      0 15     8.4   280   .75 0     
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   930 1400 140    6.1    - - - - 2 41    29    910 0   0      0 12     6.6   280   .75 0     
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 150   69   1200 1500 150    0      - - - - 2 15    9.0  490 0   0      0 960     930     750   .70 0     
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 140   69   1300 1500 150    6.1    - - - - 2 15    9.3  500 0   1.2    0 960     930     810   .68 0     
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 110   68   1000 1100 150    .75   - - - - 2 9.7  5.2  440 0   .025  2 97     78     870   .62 0     
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i 2 110   68   910 1200 150    .090  - - - - 2 8.3  4.5  310 0   0      2 37     27     760   .66 0     
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 49   23   790 420 140    0      - - - - 2 16    8.7  530 0   0      2 41     29     570   .66 0     
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i 2 52   25   1000 550 140    0      - - - - 2 13    7.2  470 0   0      2 55     41     760   .62 0     
heap-data/calendar_true-unreach-call.i 0 900   890   1800 8700 .64 0      - - - - 0 .61 .37 40 0   0      0 .021 .021 5.6 0    0     
heap-data/cart_true-unreach-call.i 0 760   740   660 10000 .73 0      - - - - 0 .76 .46 40 0   0      0 .022 .023 5.6 0    0     
heap-data/hash_fun_true-unreach-call.i 2 69   38   790 630 200    .061  - - - - 0 900    900    1100 0   0      0 960     920     2200   .72 0     
heap-data/min_max_true-unreach-call.i 0 900   890   700 8300 .61 0      - - - - 0 .58 .36 40 0   0      0 .022 .022 5.6 0    0     
heap-data/packet_filter_true-unreach-call.i 0 900   890   2200 9900 .73 0      - - - - 0 .61 .39 41 0   0      0 .021 .022 5.6 0    0     
heap-data/process_queue_true-unreach-call.i 0 640   620   3100 5100 .86 0      - - - - 0 .63 .38 42 0   0      0 .022 .022 5.6 0    0     
heap-data/quick_sort_split_true-unreach-call.i 2 20   8.6 450 160 140    0      - - - - 0 900    890    3800 0   0      2 9.0   5.1   330   .62 0     
heap-data/running_example_true-unreach-call.i 0 550   530   5300 3800 .79 0      - - - - 0 .76 .47 41 0   0      0 .021 .022 5.7 0    0     
heap-data/shared_mem1_true-unreach-call.i 0 900   890   4500 11000 .66 0      - - - - 0 .77 .48 40 0   0      0 .020 .021 5.6 0    0     
heap-data/shared_mem2_true-unreach-call.i 0 900   890   4300 9500 .68 .025  - - - - 0 .73 .44 41 0   0      0 .021 .021 5.6 0    0     
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i 1 22   7.9 300 180 .47 .029  1 75    72    410 0   0      1 35     24     2900   .62 0      0 4.9  2.7  260 0     0      1 .64   .64   21    .074 0      - -
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i 1 240   210   3500 2600 .54 0      0 98    82    1700 0   0      0 88     58     7000   .63 0      0 4.5  2.5  260 0     0      1 .64   .64   21    .070 0      - -
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i 1 60   41   410 610 .53 0      0 96    80    1600 0   0      1 72     55     2400   .62 .025  0 5.1  2.9  260 0     0      -32 .65   .65   21    .078 0      - -
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i 0 510   490   1100 4900 .83 0      0 97    79    1300 0   0      0 97     85     760   1.7  0      0 4.8  2.6  270 0     0      0 .66   .66   21    .053 0      - -
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i 2 150   69   1400 1500 150    0      - - - - 2 51    44    590 0   0      0 960     920     1600   .64 0     
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i 2 110   69   1100 1100 140    0      - - - - 2 70    61    580 0   0      0 960     910     1700   .64 0     
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i 2 150   69   1300 1300 160    .061  - - - - 2 17    11    540 0   0      0 960     940     1200   1.5  .025 
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i 2 150   70   940 1700 150    0      - - - - 0 900    870    4200 0   0      0 960     880     2800   .63 0     
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i 2 120   77   800 1300 150    .012  - - - - 0 510    440    7000 0   0      0 960     920     2300   .64 0     
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i 0 690   660   1000 6600 1.2  0      - - - - 0 .72 .43 41 0   0      0 .023 .024 5.6 0    0     
sv-benchmarks/c/ 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) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 241 305 50000 45000 310000 500000 18000   190    75 -697 980 710 28000 0   .086 75 -29 1600 1100 76000 52   .082 75 -17 320   310   18000 .016 1.6   75 -202 45   45   1500 4.5  .11  166 226 5500 4800 65000 0   1.5 166 144 25000 24000 70000 84 .14  
    correct results 185 305 11000 6800 130000 110000 18000   190    39 39 250 170 10000 0   .033 35 35 410 250 17000 23   .033 15 15 59   34   3700 0     .012 54 54 34   34   1100 3.5  .061 113 226 2200 1700 46000 0   1.5 72 144 1400 1000 29000 46 .0041
        correct true 120 240 7300 3700 89000 71000 18000   170    0 0 0 0 113 226 2200 1700 46000 0   1.5 72 144 1400 1000 29000 46 .0041
        correct false 65 65 4000 3200 42000 40000 28   15    39 39 250 170 10000 0   .033 35 35 410 250 17000 23   .033 15 15 59   34   3700 0     .012 54 54 34   34   1100 3.5  .061 0 0
    correct-unconfimed results 7 0 1700 1600 7500 17000 6.5 .19 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 7 0 1700 1600 7500 17000 6.5 .19 0 0 0 0 0 0
    incorrect results 0 23 -736 120 65 6000 0   .053 2 -64 20 12 640 1.3 0     1 -32 3.4 2.0 250 0     0     8 -256 5.0 5.0 170 .55 .029 0 0
        incorrect true 0 23 -736 120 65 6000 0   .053 2 -64 20 12 640 1.3 0     1 -32 3.4 2.0 250 0     0     8 -256 5.0 5.0 170 .55 .029 0 0
        incorrect false 0 0 0 0 0 0 0
score (241 tasks, max score: 407) 305 -697 -29 -17 -202 226 144
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap