Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 600    600    6000   15000 .84 0      error (invalid witness file) .50 .32 9.1 42 error (invalid witness file) 6.3 3.3 130 300 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 810    810    5100   15000 .84 0      error (invalid witness file) .53 .34 14   40 error (invalid witness file) 5.7 3.1 64 300 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 610    610    6500   15000 .84 0      error (invalid witness file) .59 .37 10   39 error (invalid witness file) 7.2 3.7 130 330 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900    900    9700   6100 .84 0      error (invalid witness file) .66 .41 7.3 41 error (invalid witness file) 5.9 3.1 81 300 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 100    100    1200   15000 .84 0      error (invalid witness file) .49 .32 8.4 39 error (invalid witness file) 6.1 3.2 120 290 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 100    100    1200   15000 .84 0      error (invalid witness file) .64 .41 8.2 39 error (invalid witness file) 5.9 3.1 87 310 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 600    600    6200   15000 .84 0      - - error (invalid witness file) .62 .39 9.8 43 error (invalid witness file) 6.0 3.2 92 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 510    510    4200   15000 1.7  0      - - error (recursion) 13    7.0  180   630 true 800   760   13000 1100
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 810    810    5600   15000 .84 0      - - error (invalid witness file) .62 .40 8.6 41 error (invalid witness file) 5.9 3.2 88 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 610    610    6500   15000 .84 0      - - error (invalid witness file) .67 .43 6.2 43 error (invalid witness file) 6.7 3.5 63 290
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   6100 .84 0      - - error (invalid witness file) .66 .42 7.9 41 error (invalid witness file) 5.8 3.1 120 300
heap-manipulation/tree_true-unreach-call.i out of memory 0 wit inspect 100    100    1200   15000 .84 0      - - error (invalid witness file) .47 .31 8.2 39 error (invalid witness file) 6.0 3.2 92 310
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 250    250    2500   15000 1.7  0      timeout 97    87    1800   5200 false(unreach-call) 55   31   690 3600 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 600    600    5900   15000 .84 0      error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.0 3.2 76 290 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 220    220    2300   15000 1.7  0      out of memory 84    78    1900   7000 false(unreach-call) 55   38   720 4000 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 18    18    220   1100 1.7  .094  true 4.8  2.6  54   280 true 8.0 4.3 130 320 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 360    360    4100   15000 1.7  0      timeout 92    82    1900   4100 out of memory 82   57   620 7000 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 350    350    3600   15000 1.7  0      false(unreach-call) 6.6  3.6  76   290 false(unreach-call) 8.5 4.6 150 340 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 250    250    2700   15000 1.8  0      - - timeout 900    890    17000   3200 timeout 960   910   12000 2500
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 840    840    2000   15000 1.7  0      - - timeout 900    890    15000   1600 timeout 960   900   14000 1600
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.4  7.4  86   350 2.8  0      - - true 35    19    370   770 true 48   32   640 900
list-properties/list_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 600    600    5900   15000 .84 0      - - error (invalid witness file) .69 .43 6.2 40 error (invalid witness file) 8.0 4.2 71 320
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 150    150    1900   15000 1.7  0      - - timeout 900    890    14000   3100 timeout 960   930   12000 2000
list-properties/simple_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 360    360    3600   15000 1.7  0      - - timeout 910    890    13000   2300 timeout 960   890   19000 3200
list-properties/splice_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 410    410    3700   15000 1.7  0      - - timeout 910    870    14000   6400 timeout 960   900   14000 2000
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 .16 1.3 23 1.7  0      false(unreach-call) 4.2  2.4  78   270 false(unreach-call) 7.4 4.0 120 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .69 .68 2.6 25 1.7  0      false(unreach-call) 5.9  3.2  99   290 true 7.6 4.1 94 340 - -
ldv-regression/callfpointer.c_false-unreach-call.i unknown 0 wit inspect .13 .13 1.6 23 1.7  0      error (invalid witness file) .56 .36 11   40 error (invalid witness file) 5.7 3.1 96 300 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .25 .24 2.4 25 1.7  0      false(unreach-call) 5.3  2.9  110   290 true 7.5 4.0 130 320 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .14 .14 1.4 23 1.7  .094  false(unreach-call) 3.9  2.2  34   270 true 7.3 3.9 140 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 .13 1.5 23 1.7  .094  false(unreach-call) 3.9  2.2  60   270 false(unreach-call) 6.7 3.6 110 310 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .17 .16 1.6 23 1.7  .094  false(unreach-call) 4.8  2.7  66   290 true 7.1 3.8 120 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 .16 1.5 23 1.7  0      false(unreach-call) 5.8  3.2  55   280 false(unreach-call) 8.9 4.8 150 360 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .24 .24 2.7 25 1.7  0      false(unreach-call) 5.9  3.2  92   290 true 7.6 4.0 110 330 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 150    150    1900   3300 1.7  .094  false(unreach-call) 6.9  3.8  130   310 true 7.1 3.9 110 320 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 .13 1.9 23 1.7  0      false(unreach-call) 4.1  2.3  46   270 true 9.4 4.9 120 330 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .17 .17 1.4 23 1.7  .094  false(unreach-call) 4.6  2.5  36   270 true 6.9 3.7 100 320 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect .12 .12 1.3 23 1.7  0      - - true 3.2  1.9  55   250 true 7.7 4.1 130 320
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect .15 .15 1.6 23 1.7  0      - - true 3.9  2.2  44   250 true 7.5 4.0 120 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect .12 .12 1.3 23 1.7  0      - - true 3.9  2.2  46   260 true 8.6 4.6 82 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 4.2  2.3  45   260 true 7.3 3.9 110 310
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect .23 .23 2.4 24 1.7  0      - - true 17    9.6  290   520 true 27   16   210 740
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .16 .16 1.2 23 1.7  0      - - true 3.9  2.1  40   260 true 7.3 3.9 58 300
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 3.8  2.1  42   260 true 10   5.5 93 310
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .16 .16 1.3 23 1.7  0      - - true 4.2  2.4  40   260 true 9.1 4.9 100 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .13 .13 1.4 23 1.7  0      - - true 4.3  2.4  49   270 true 9.3 5.0 150 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .13 .12 1.5 23 1.7  0      - - true 3.6  2.0  84   270 true 6.8 3.6 89 320
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect .16 .16 1.7 23 1.7  0      - - true 3.5  2.0  63   260 true 8.2 4.3 89 330
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect .13 .13 1.6 23 1.7  0      - - true 4.3  2.4  44   260 true 12   6.5 140 440
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect .13 .12 1.5 23 1.7  0      - - true 4.5  2.5  51   270 true 12   6.9 200 470
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect .15 .16 1.4 23 1.8  0      - - true 4.6  2.5  51   270 true 11   5.8 130 350
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect .13 .13 1.6 23 1.7  0      - - true 4.1  2.3  68   260 true 7.7 4.2 160 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .15 .15 1.6 23 1.7  0      - - true 3.5  2.0  79   250 true 7.1 3.8 110 310
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect .17 .17 1.5 23 1.7  0      - - true 3.9  2.2  76   260 true 10   5.3 150 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .18 .18 1.8 24 1.7  0      - - true 4.3  2.4  49   270 true 11   5.9 120 360
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect .25 .25 3.4 24 1.7  0      - - true 5.9  3.2  75   260 true 28   16   310 710
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .17 .17 1.7 24 1.7  0      - - true 4.8  2.7  70   260 true 8.3 4.4 120 330
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect .16 .16 1.3 23 1.7  0      - - true 3.7  2.1  58   260 true 6.8 3.6 89 310
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect .15 .15 2.0 24 1.7  0      - - true 5.0  2.7  90   270 true 7.6 4.1 87 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .13 .13 1.4 23 1.7  0      - - true 4.2  2.3  43   260 true 8.4 4.5 93 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect .19 .18 1.9 24 1.7  0      - - true 4.6  2.5  97   260 true 7.5 4.1 120 310
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect .18 .18 1.7 24 1.7  0      - - true 4.8  2.6  78   270 true 8.1 4.3 150 330
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .19 .19 1.9 25 1.7  0      - - true 6.2  3.4  71   280 true 8.1 4.3 180 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect .16 .16 1.2 23 1.7  0      - - true 3.3  1.8  61   260 true 6.9 3.7 87 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect .13 .13 1.6 23 1.7  0      - - true 3.8  2.2  37   260 true 7.5 4.0 95 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect .21 .21 2.4 25 2.6  0      - - true 4.2  2.4  51   260 unknown 7.0 3.7 82 310
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect .18 .18 2.1 23 2.5  0      - - true 3.4  1.9  29   260 unknown 7.4 3.9 83 300
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect .20 .20 2.3 23 2.5  0      - - true 4.3  2.4  45   260 unknown 5.8 3.1 70 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect .21 .21 2.1 25 2.5  0      - - true 3.9  2.2  48   260 unknown 6.2 3.3 83 310
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .12 .12 1.4 23 1.7  0      - - true 4.2  2.4  52   260 true 7.7 4.1 100 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .14 .14 1.4 23 1.7  0      - - true 4.2  2.4  49   260 true 7.3 3.9 66 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .16 .16 1.5 23 1.7  0      false(unreach-call) 3.5  1.9  54   280 true 6.7 3.6 100 310 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.4 23 1.7  0      false(unreach-call) 4.4  2.4  71   270 true 8.3 4.3 130 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .14 1.7 23 1.7  0      false(unreach-call) 4.0  2.3  49   290 true 7.2 3.8 120 320 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .20 .20 1.7 23 1.7  0      false(unreach-call) 3.6  2.0  68   260 true 7.1 3.8 120 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .17 .17 2.1 23 1.7  0      false(unreach-call) 4.1  2.3  83   290 false(unreach-call) 7.8 4.1 110 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3  3.3  38   150 1.9  0      timeout 97    85    2300   1100 timeout 96   78   1600 4600 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6  5.6  55   370 1.7  .10   false(unreach-call) 6.8  3.8  81   320 false(unreach-call) 51   36   470 880 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 3.9  3.9  39   160 1.7  0      false(unreach-call) 18    14    240   490 out of memory 76   45   880 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 4.1  4.1  53   150 1.7  0      true 4.3  2.4  83   280 false(unreach-call) 17   9.6 150 570 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .15 .15 1.5 23 1.7  0      false(unreach-call) 4.4  2.5  54   280 true 7.1 3.8 130 310 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 3.1  3.1  35   150 1.7  0      false(unreach-call) 5.1  2.9  75   290 true 7.7 4.1 140 320 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .16 .16 1.8 23 1.7  0      false(unreach-call) 3.7  2.1  62   270 false(unreach-call) 11   5.6 190 380 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .17 .17 1.9 23 1.7  0      true 3.4  1.9  71   270 false(unreach-call) 8.4 4.4 140 340 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.5 23 1.7  0      false(unreach-call) 4.3  2.4  50   270 true 6.9 3.6 57 310 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 4.0  2.2  61   260 true 7.4 4.0 98 310
ldv-regression/test03_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 3.3  1.9  53   260 true 7.3 4.0 83 310
ldv-regression/test04_true-unreach-call.c true 2 wit inspect .15 .15 1.5 23 1.7  0      - - true 3.4  1.9  46   260 true 8.3 4.5 110 320
ldv-regression/test05_true-unreach-call.c true 2 wit inspect .15 .15 1.6 23 1.7  0      - - true 3.7  2.1  43   270 true 12   7.2 120 510
ldv-regression/test07_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 4.1  2.3  50   260 true 10   5.7 130 430
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .14 .14 1.3 23 1.7  0      - - true 4.6  2.6  49   260 true 13   7.2 100 430
ldv-regression/test10_true-unreach-call.c true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 4.5  2.5  46   260 true 15   9.1 160 480
ldv-regression/test11_true-unreach-call.c true 2 wit inspect .14 .14 1.5 23 1.7  0      - - true 4.8  2.7  48   280 true 8.8 4.8 140 320
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 4.3  2.4  43   280 true 7.3 3.9 100 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect .13 .13 1.3 23 1.7  0      - - true 4.6  2.6  41   260 true 8.8 4.8 98 330
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .13 .13 1.3 23 1.7  0      - - true 4.2  2.4  48   260 true 9.5 5.2 140 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .14 .14 1.7 23 1.7  0      - - true 4.0  2.2  48   260 true 9.2 5.1 150 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 3.5  1.9  65   260 true 7.7 4.1 89 330
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 4.4  2.5  54   260 true 9.7 5.3 150 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7  0      - - true 3.9  2.2  44   260 true 11   6.1 160 460
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .16 .16 1.5 23 1.7  0      - - true 3.5  2.0  69   250 true 6.9 3.7 77 310
ldv-regression/test21_true-unreach-call.c true 2 wit inspect .20 .20 1.8 23 1.7  0      - - true 4.2  2.4  57   260 true 9.2 4.9 120 320
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 1.0  1.0  12   96 2.0  0      - - true 9.5  5.4  100   330 true 38   25   690 860
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 6.0  6.0  64   370 2.0  0      - - true 14    9.9  150   420 true 170   140   2000 1000
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 4.0  4.0  48   150 2.0  0      - - true 7.9  4.4  150   330 true 16   8.5 120 380
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 21    21    310   160 2.0  0      - - true 29    21    690   540 true 29   16   260 700
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .15 .15 1.4 23 1.7  0      - - true 4.4  2.5  46   260 true 9.8 5.3 120 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 5.5  5.5  67   150 2.0  0      - - true 10    6.4  150   350 true 110   94   2700 900
ldv-regression/test28_true-unreach-call.c true 2 wit inspect .16 .16 1.4 23 1.7  0      - - true 4.1  2.3  43   250 true 8.5 4.7 84 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect .13 .13 1.4 23 1.7  0      - - true 4.2  2.3  47   260 true 8.2 4.5 120 320
ldv-regression/test30_true-unreach-call.c true 2 wit inspect .15 .15 1.3 23 1.7  0      - - true 4.5  2.5  50   250 true 11   6.3 130 470
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120    120    1400   15000 .84 0      error (invalid witness file) .57 .35 8.0 40 error (invalid witness file) 6.1 3.3 76 310 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120    120    1500   15000 .84 0      error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.3 3.3 98 300 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120    120    1400   15000 .84 0      error (invalid witness file) .53 .33 8.5 40 error (invalid witness file) 6.8 3.5 130 300 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1500   15000 .84 0      - - error (invalid witness file) .56 .35 7.0 40 error (invalid witness file) 5.8 3.1 91 290
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1400   15000 .84 0      - - error (invalid witness file) .50 .33 8.3 42 error (invalid witness file) 5.9 3.1 62 300
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1600   15000 .84 0      - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.5 3.4 48 310
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1200   15000 .84 0      - - error (invalid witness file) .64 .40 8.1 40 error (invalid witness file) 7.4 3.9 57 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1700   15000 .84 0      - - error (invalid witness file) .58 .37 11   40 error (invalid witness file) 6.4 3.4 89 300
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1600   15000 .84 .0082 - - error (invalid witness file) .48 .31 8.4 39 error (invalid witness file) 6.8 3.6 140 300
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1300   15000 .84 0      - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.5 3.4 99 320
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1400   15000 .84 0      - - error (invalid witness file) .60 .39 7.5 42 error (invalid witness file) 6.7 3.5 100 310
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1200   15000 .84 0      - - error (invalid witness file) .59 .38 9.2 39 error (invalid witness file) 6.0 3.2 130 290
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120    120    1400   15000 .84 0      - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 7.6 4.0 70 300
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900    900    6000   8500 .84 .28   error (invalid witness file) .53 .34 10   43 error (invalid witness file) 5.6 3.0 87 300 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 430    430    4800   15000 1.7  0      true 14    7.2  190   430 true 10   5.3 160 460 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 330    330    3000   15000 1.7  0      true 5.1  2.8  110   280 true 8.1 4.3 130 320 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 180    180    1300   15000 1.7  0      true 28    16    290   790 true 14   7.7 240 950 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 92    91    1100   15000 .84 0      error (invalid witness file) .62 .38 8.6 40 error (invalid witness file) 6.5 3.5 110 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 93    93    1200   15000 .84 0      error (invalid witness file) .67 .43 6.5 40 error (invalid witness file) 5.8 3.1 85 290 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 350    350    3100   15000 1.7  0      true 4.9  2.7  77   280 true 7.6 4.1 120 320 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 450    450    4300   15000 1.7  0      true 8.5  4.5  110   290 true 8.7 4.6 130 330 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 410    410    5100   15000 1.7  0      timeout 97    83    2100   6100 true 36   19   430 2800 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900    900    6400   7000 .84 0      error (invalid witness file) .63 .42 8.3 40 error (invalid witness file) 6.6 3.5 120 310 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900    900    6200   10000 .84 0      error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.1 3.2 86 290 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 380    380    4500   15000 1.7  0      true 7.6  4.1  79   280 true 9.3 4.9 130 330 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 240    240    1900   15000 1.7  0      true 5.5  3.0  79   280 true 7.6 4.1 110 310 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 160    160    1300   15000 1.7  0      true 28    15    300   660 true 16   8.1 260 950 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 330    330    4500   15000 .84 0      error (invalid witness file) .50 .33 13   41 error (invalid witness file) 5.4 3.0 96 290 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900    900    12000   12000 .84 0      error (invalid witness file) .52 .34 10   39 error (invalid witness file) 6.0 3.2 97 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 470    470    4800   15000 1.7  0      true 38    22    420   830 true 13   7.0 240 700 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 380    380    3700   15000 1.7  0      true 47    27    550   1200 true 14   7.4 250 710 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 380    380    4600   15000 1.7  0      true 6.3  3.6  120   310 true 12   6.4 180 370 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    6600   8500 .84 0      - - error (invalid witness file) .57 .36 10   40 error (invalid witness file) 5.7 3.0 77 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 450    450    4400   15000 1.7  0      - - timeout 910    890    15000   3500 timeout 960   890   26000 1300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 250    250    2500   15000 1.7  0      - - unknown 32    21    420   750 timeout 960   860   14000 2300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 180    180    1700   15000 1.7  0      - - timeout 910    890    11000   3300 timeout 960   860   13000 1800
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 91    91    1200   15000 .84 0      - - error (invalid witness file) .57 .36 9.2 39 error (invalid witness file) 6.0 3.2 110 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 93    93    1200   15000 .84 0      - - error (invalid witness file) .47 .31 6.2 40 error (invalid witness file) 7.1 3.7 67 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 200    200    1800   15000 .84 0      - - error (invalid witness file) .68 .43 7.6 40 error (invalid witness file) 6.7 3.5 63 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    10000   12000 .84 0      - - error (invalid witness file) .63 .39 9.0 40 error (invalid witness file) 5.7 3.0 87 290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 890    900    10000   14000 1.7  0      - - true 82    61    1300   2100 true 15   8.0 170 920
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 410    410    5000   15000 1.7  0      - - timeout 910    890    14000   4000 timeout 960   930   14000 1000
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    5900   7400 .84 0      - - error (invalid witness file) .52 .34 8.5 42 error (invalid witness file) 5.9 3.1 90 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    6200   10000 .84 0      - - error (invalid witness file) .57 .38 7.4 40 error (invalid witness file) 5.3 2.9 79 290
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 420    420    4500   15000 1.8  0      - - timeout 910    890    15000   3300 timeout 960   900   22000 1300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 230    230    1800   15000 1.7  0      - - unknown 28    17    450   720 timeout 960   890   14000 1800
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 150    150    1700   15000 1.7  0      - - timeout 900    890    15000   3100 timeout 960   910   13000 1500
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 340    340    4000   15000 .84 0      - - error (invalid witness file) .61 .38 9.0 41 error (invalid witness file) 6.8 3.6 100 320
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000   12000 .84 0      - - error (invalid witness file) .62 .41 8.0 39 error (invalid witness file) 6.0 3.2 70 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120    120    1500   15000 .84 0      - - error (invalid witness file) .49 .33 12   40 error (invalid witness file) 5.9 3.1 71 300
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    10000   8300 .84 0      - - error (invalid witness file) .65 .42 8.5 40 error (invalid witness file) 6.5 3.4 53 310
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   9600 .84 0      - - error (invalid witness file) .67 .43 7.7 40 error (invalid witness file) 6.1 3.2 80 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 380    380    4100   15000 1.7  0      - - timeout 910    890    11000   3900 timeout 960   890   12000 2400
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 27    27    320   680 1.7  0      timeout 96    79    2500   2300 true 7.7 4.1 100 320 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 46    46    560   2100 1.7  .094  timeout 97    81    2700   3000 timeout 97   77   1500 1700 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 38    38    400   2100 1.7  0      timeout 97    77    1400   2200 true 8.0 4.2 110 330 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i out of memory 0 wit inspect 170    170    2000   15000 .84 0      error (invalid witness file) .47 .30 6.5 40 error (invalid witness file) 6.8 3.6 48 300 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i out of memory 0 wit inspect 170    170    1700   15000 .84 0      - - error (invalid witness file) .63 .40 7.7 39 error (invalid witness file) 5.8 3.1 70 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i timeout 0 wit inspect 900    900    6500   5000 .84 0      error (invalid witness file) .53 .35 7.2 40 error (invalid witness file) 5.6 3.0 64 300 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900    900    6100   4900 .84 0      - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.2 3.3 120 300
list-ext2-properties/simple_search_value_false-unreach-call.i out of memory 0 wit inspect 390    390    4100   15000 1.7  0      false(unreach-call) 10    6.5  140   430 timeout 97   87   1600 1100 - -
list-ext2-properties/simple_search_value_true-unreach-call.i out of memory 0 wit inspect 370    370    3500   15000 1.7  0      - - timeout 900    890    15000   1600 timeout 960   940   12000 3200
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 173 135 35000 35000 340000 1100000 260   1.0  173 1100 850 21000 45000   173 1100 710 16000 53000   173 11000 11000 180000 62000   173 15000 14000   240000 63000  
    correct results 90 151 350 350 4300 13000 160   .76 25 520 400 11000 16000   26 520 340 7500 23000   61 350 200 4800 17000   57 930 600   13000 24000  
        correct true 61 122 53 53 680 2600 110   0    3 0 0 0 0   18 0 0 0 0   61 350 200 4800 17000   57 930 600   13000 24000  
        correct false 29 29 300 300 3600 11000 49   .76 22 520 400 11000 16000   8 520 340 7500 23000   0 0 0 0 0   0 0 0   0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -16 890 900 10000 14000 1.7 0    0 0 0 0 0   0 0 0 0 0   1 82 61 1300 2100   1 15 8.0 170 920  
        incorrect true 0
        incorrect false 1 -16 890 900 10000 14000 1.7 0    0 0 0 0 0   0 0 0 0 0   0 82 61 1300 2100   0 15 8.0 170 920  
score (173 tasks, max score: 280) 135
Run set sv-comp17.ReachSafety-Heap