Tool ULTIMATE Taipan f7c3ed31
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-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.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 timeout 0 wit inspect 900   880   11000 810 2.5 0      error (invalid witness file) .48 .33 7.3 39 error (invalid witness file) 6.5 3.5 130 300 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   820   12000 1500 2.3 0      error (invalid witness file) .49 .33 9.3 39 error (invalid witness file) 5.9 3.1 110 290 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 11   3.4 91 480 2.5 0      exception 3.1  1.7  53   200 false(unreach-call) 11   5.6 180 370 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   670   5700 8800 2.3 0      error (invalid witness file) .53 .36 12   40 error (invalid witness file) 5.9 3.1 100 300 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   730   6400 8500 2.3 0      error (invalid witness file) .49 .33 5.4 43 error (invalid witness file) 5.5 2.9 80 290 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   790   6300 6200 2.3 0      error (invalid witness file) .53 .34 10   40 error (invalid witness file) 7.4 3.9 120 320 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   13000 770 2.5 0      - - error (invalid witness file) .58 .38 9.6 39 error (invalid witness file) 7.0 3.7 130 320
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   840   12000 2600 2.3 0      - - error (invalid witness file) .63 .39 9.4 39 error (invalid witness file) 6.0 3.2 110 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880   9800 3800 2.3 0      - - error (invalid witness file) .52 .33 10   39 error (invalid witness file) 6.2 3.3 120 290
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   810   9200 4200 2.3 0      - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 6.0 3.1 70 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 840   810   11000 2200 2.5 0      - - error (invalid witness file) .65 .41 8.2 40 error (invalid witness file) 6.7 3.5 140 320
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   780   6400 7000 2.3 0      - - error (invalid witness file) .65 .42 8.6 41 error (invalid witness file) 6.2 3.4 120 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 2.1 53 370 2.5 0      true 5.2  2.8  74   300 false(unreach-call) 7.6 4.0 110 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   760   8100 6800 2.3 0      error (invalid witness file) .56 .37 4.7 43 error (invalid witness file) 6.0 3.2 130 300 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.9 2.4 60 360 2.5 0      true 5.1  2.7  72   290 false(unreach-call) 7.9 4.2 130 320 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   880   6000 1100 2.3 0      error (invalid witness file) .60 .37 14   43 error (invalid witness file) 6.3 3.4 120 300 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.4 2.9 84 380 2.5 0      true 6.5  3.5  79   280 false(unreach-call) 7.8 4.2 160 320 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.5 2.4 68 370 2.5 0      true 5.5  3.0  80   280 false(unreach-call) 9.8 5.1 160 330 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   7000 3700 2.3 0      - - error (invalid witness file) .65 .41 8.2 40 error (invalid witness file) 6.4 3.3 100 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   750   11000 790 2.3 0      - - error (invalid witness file) .48 .32 9.6 40 error (invalid witness file) 7.2 3.8 77 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870   6900 3400 2.3 0      - - error (invalid witness file) .55 .35 9.8 40 error (invalid witness file) 7.2 3.8 84 300
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830   8600 5400 2.3 0      - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 7.0 3.7 150 320
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   810   11000 3800 2.3 0      - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.6 3.0 93 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   570   5000 11000 2.3 0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.2 89 310
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   400   6000 13000 2.3 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.1 3.2 88 300
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.4 2.0 47 320 2.7 0      exception 2.9  1.6  27   160 false(unreach-call) 8.0 4.3 160 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.9 2.1 57 350 2.5 0      true 5.2  2.8  88   290 false(unreach-call) 9.4 5.0 190 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.4 1.8 45 320 2.5 0      false(unreach-call) 3.4  1.9  47   270 false(unreach-call) 7.4 3.9 160 320 - -
ldv-regression/fo_test.c_false-unreach-call.i unknown 0 wit inspect 11   3.6 89 320 2.6 0      error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.2 3.3 110 300 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.7 1.9 46 330 2.5 0      true 3.4  1.9  73   270 false(unreach-call) 7.7 4.0 160 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.1 2.0 47 330 2.5 0      true 3.2  1.8  35   270 false(unreach-call) 7.7 4.1 140 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.0 2.0 49 320 2.5 0      assertion 2.5  1.4  42   160 false(unreach-call) 8.2 4.4 170 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect 7.3 2.2 56 350 2.5 0      true 4.0  2.2  88   270 false(unreach-call) 8.7 4.7 120 360 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 19   6.6 170 710 2.9 0      assertion 3.1  1.7  52   180 false(unreach-call) 8.9 4.8 170 330 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 100   48   1000 1900 2.5 0      false(unreach-call) 5.1  2.8  70   280 false(unreach-call) 9.2 4.8 160 320 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 7.7 2.3 54 370 2.5 0      false(unreach-call) 4.0  2.2  69   280 false(unreach-call) 7.4 3.9 140 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 6.9 2.1 61 370 2.5 0      false(unreach-call) 3.6  2.1  50   270 false(unreach-call) 7.3 3.9 130 310 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 6.1 1.8 47 330 2.5 0      - - true 4.0  2.2  49   260 true 8.0 4.3 150 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 5.9 1.9 44 330 2.7 0      - - true 3.4  1.9  67   260 true 7.9 4.2 150 310
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 6.5 2.1 53 320 2.5 0      - - true 3.6  2.0  69   260 true 8.3 4.4 100 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 5.9 2.0 43 330 2.5 0      - - true 3.3  1.9  72   260 true 6.9 3.7 140 300
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect 37   14   300 700 2.5 0      - - true 20    11    290   530 true 30   17   410 730
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 5.7 1.8 40 330 2.5 0      - - true 4.0  2.3  48   250 true 6.4 3.4 80 320
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 6.5 2.0 56 330 2.5 0      - - true 4.0  2.2  54   260 true 10   5.3 170 360
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 6.6 2.1 53 330 2.5 0      - - true 3.5  2.0  70   260 true 8.1 4.4 130 310
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 8.6 2.4 68 380 2.5 0      - - true 3.6  2.0  60   260 true 9.2 5.0 170 320
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 5.5 1.8 43 320 2.5 0      - - true 4.3  2.4  45   260 true 7.6 4.0 160 320
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 7.3 2.0 50 340 2.5 0      - - true 3.5  1.9  74   270 true 7.2 3.9 160 330
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 12   4.0 91 490 2.5 .0041 - - true 3.5  1.9  69   260 true 13   7.0 190 450
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 11   4.1 96 490 2.5 0      - - true 4.4  2.4  43   270 true 13   7.2 150 480
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 8.1 2.5 68 410 2.5 0      - - true 3.7  2.1  58   270 true 11   6.0 170 360
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 6.0 1.9 50 320 2.5 0      - - true 3.9  2.2  48   260 true 7.8 4.2 120 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 5.5 1.8 46 320 2.5 0      - - true 3.4  1.9  70   260 true 7.4 4.0 160 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect 7.3 2.0 52 350 2.6 0      - - true 5.2  2.9  53   260 true 10   5.4 150 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 8.3 2.6 63 430 2.5 0      - - true 5.5  3.0  81   280 true 11   6.0 190 360
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect 23   7.7 180 740 2.5 0      - - true 5.5  3.0  82   280 true 28   16   260 690
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 5.6 1.8 45 340 2.5 0      - - true 4.4  2.4  67   270 true 7.5 4.0 120 320
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 5.7 1.9 47 320 2.5 0      - - true 3.8  2.1  64   260 true 7.4 3.9 120 320
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 6.6 2.1 47 320 2.5 0      - - true 5.6  3.1  56   260 true 7.8 4.2 140 310
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 6.1 1.9 49 340 2.5 0      - - true 4.2  2.3  48   260 true 7.5 4.0 140 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 6.5 2.0 48 330 2.5 0      - - true 5.3  2.9  52   270 true 8.4 4.5 130 330
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 7.0 2.1 58 360 2.5 0      - - true 5.2  2.9  66   260 true 8.1 4.4 140 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect 6.3 1.9 49 340 2.5 0      - - true 6.4  3.4  68   270 true 7.6 4.1 150 330
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 5.7 1.8 42 320 2.5 0      - - true 3.6  2.1  67   260 true 7.3 3.9 77 320
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 6.0 1.9 46 330 2.5 0      - - true 4.1  2.3  46   250 true 7.1 3.8 98 320
ldv-regression/test_union_cast-1_true-unreach-call.i unknown 0 wit inspect 5.0 1.4 34 310 2.5 0      - - error (invalid witness file) .74 .45 7.1 42 error (invalid witness file) 5.5 2.9 93 290
ldv-regression/test_union_cast-2_true-unreach-call.i unknown 0 wit inspect 5.9 1.7 41 320 2.5 0      - - error (invalid witness file) .64 .40 7.5 40 error (invalid witness file) 6.1 3.2 110 310
ldv-regression/test_union_cast.c_true-unreach-call.i unknown 0 wit inspect 4.8 1.5 37 310 2.5 0      - - error (invalid witness file) .55 .35 7.7 41 error (invalid witness file) 5.9 3.2 110 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown 0 wit inspect 5.8 1.6 40 340 2.5 0      - - error (invalid witness file) .51 .33 12   42 error (invalid witness file) 6.4 3.4 110 320
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 6.6 2.0 53 330 2.5 0      - - true 3.8  2.2  53   260 true 8.3 4.5 140 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 7.1 2.1 52 340 2.5 0      - - true 3.5  2.0  78   260 true 8.1 4.3 130 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect 6.0 1.8 45 340 2.5 0      true 3.3  1.9  55   260 false(unreach-call) 8.2 4.3 140 330 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect 8.1 2.3 58 360 2.5 0      error (invalid witness file) 2.4  1.4  46   170 false(unreach-call) 8.0 4.3 140 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect 5.9 1.9 45 320 2.5 0      true 3.5  2.0  55   280 false(unreach-call) 8.2 4.3 150 320 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect 5.4 1.8 42 320 2.8 0      true 3.8  2.2  46   270 false(unreach-call) 8.1 4.3 140 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect 7.0 1.9 49 340 2.5 0      assertion 2.2  1.3  30   160 false(unreach-call) 7.6 4.1 160 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 9.5 2.8 77 450 2.6 0      assertion 2.4  1.4  60   160 false(unreach-call) 12   6.5 170 390 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 30   15   330 590 2.5 0      assertion 2.3  1.3  35   160 timeout 97   63   1400 4600 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 21   6.0 170 710 2.6 0      error (invalid witness file) 2.5  1.4  21   170 out of memory 87   52   840 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 14   4.4 120 530 2.5 0      true 3.9  2.2  83   270 out of memory 73   45   930 7000 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect 5.8 1.8 42 330 2.5 0      true 3.5  2.0  69   280 false(unreach-call) 7.0 3.8 110 310 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 6.9 2.1 53 370 2.5 0      false(unreach-call) 4.0  2.3  52   280 false(unreach-call) 8.5 4.6 150 320 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect 7.2 2.0 56 350 2.5 0      assertion 2.8  1.6  34   150 false(unreach-call) 8.4 4.6 140 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect 6.5 2.1 52 330 2.5 0      assertion 2.3  1.3  33   160 false(unreach-call) 7.9 4.2 120 340 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect 6.9 1.9 47 360 2.5 0      true 3.4  1.9  55   260 false(unreach-call) 8.5 4.5 120 340 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 5.9 1.9 47 330 2.5 0      - - true 4.4  2.4  43   260 true 7.3 3.9 76 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 6.5 2.0 58 320 2.5 0      - - true 3.9  2.2  51   260 true 9.1 4.9 180 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 6.9 2.1 56 330 2.5 0      - - true 3.6  2.0  68   260 true 8.2 4.5 170 330
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 260   250   3000 1400 2.5 0      - - true 4.1  2.3  47   260 true 13   7.3 250 540
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 26   15   280 1100 2.5 0      - - true 3.9  2.2  55   260 true 12   6.4 200 370
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 26   15   330 1000 2.5 0      - - true 3.7  2.1  68   260 true 10   5.7 140 420
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 81   72   940 560 2.5 0      - - true 4.7  2.6  51   260 true 14   8.6 220 470
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 7.4 2.2 58 340 2.5 0      - - true 3.3  1.9  65   260 true 9.2 5.0 100 350
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 6.4 2.0 48 320 2.5 0      - - true 4.2  2.4  50   260 true 7.5 4.1 150 320
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 7.8 2.2 60 350 2.5 0      - - true 3.9  2.2  78   280 true 8.5 4.6 150 340
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 7.4 2.3 64 370 2.5 0      - - true 4.1  2.3  46   260 true 13   7.0 110 360
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 9.4 2.8 78 500 2.5 0      - - true 3.6  2.0  74   260 true 9.4 5.2 160 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 6.0 1.8 46 340 2.5 0      - - true 3.5  2.0  73   260 true 7.7 4.1 170 320
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 7.3 2.2 54 350 2.5 0      - - true 3.5  2.0  67   260 true 9.3 5.0 200 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 18   12   190 550 2.5 0      - - true 3.8  2.2  58   260 true 10   5.8 190 450
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 6.1 1.9 52 320 2.5 0      - - true 4.1  2.3  38   260 true 7.8 4.1 120 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 7.0 2.1 54 350 2.5 0      - - true 4.8  2.7  49   260 true 10   5.4 180 340
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 31   15   290 710 2.6 0      - - exception 4.2  2.3  58   260 true 38   25   960 750
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 110   94   1200 670 2.5 0      - - assertion 3.6  2.0  71   260 true 160   130   1700 930
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 11   3.2 79 440 2.5 0      - - exception 4.2  2.4  41   260 true 13   7.0 170 400
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 24   6.9 200 750 2.5 0      - - exception 3.6  2.0  79   260 error 9.9 5.4 150 300
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 7.5 2.4 59 400 2.5 0      - - true 3.4  2.0  71   260 true 9.7 5.3 140 330
ldv-regression/test27_true-unreach-call.c timeout 0 wit inspect 900   890   12000 1500 2.3 0      - - error (invalid witness file) .63 .41 7.3 40 error (invalid witness file) 5.4 2.9 80 280
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 6.7 2.1 59 330 2.5 0      - - true 4.7  2.6  47   260 true 8.7 4.7 120 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 6.9 2.1 57 330 2.5 0      - - true 3.7  2.1  74   270 true 9.2 4.9 110 330
ldv-regression/test30_true-unreach-call.c timeout 0 wit inspect 900   600   8100 8400 2.3 0      - - error (invalid witness file) .65 .40 8.3 39 error (invalid witness file) 6.0 3.2 120 300
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 310   270   3000 1500 2.6 0      true 7.9  4.2  160   290 false(unreach-call) 59   37   640 780 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 320   280   2300 1300 2.6 0      true 9.4  5.0  83   290 false(unreach-call) 67   44   1000 840 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 320   280   1900 1300 2.6 0      true 8.6  4.6  83   290 false(unreach-call) 61   39   840 760 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 12   3.1 96 490 3.0 0      - - true 16    8.2  160   440 true 12   6.6 220 440
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.8 79 490 3.0 0      - - true 12    6.3  250   430 true 13   7.1 190 440
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.9 77 470 3.0 0      - - true 12    6.5  240   440 true 12   6.6 200 440
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 11   2.9 82 490 3.0 0      - - true 14    7.6  160   440 true 12   6.3 140 430
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.8 81 480 3.0 0      - - true 14    7.1  210   440 true 13   7.1 290 430
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.7 2.7 71 470 3.0 0      - - true 14    7.5  210   440 true 11   6.2 170 430
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.9 78 480 3.0 0      - - true 14    7.3  170   430 true 12   6.3 210 420
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 11   2.9 82 500 3.0 0      - - true 12    6.4  240   430 true 12   6.3 170 420
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.8 80 470 3.0 0      - - true 13    6.9  160   440 true 12   6.3 180 430
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   2.8 80 480 3.0 0      - - true 13    6.9  200   430 true 13   7.2 220 440
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 26   17   230 680 2.5 0      true 5.5  3.0  96   290 false(unreach-call) 14   7.3 230 390 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 16   6.0 140 540 2.5 0      true 5.0  2.7  59   290 false(unreach-call) 17   8.8 210 410 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.7 2.1 53 340 2.5 0      true 4.8  2.6  85   280 false(unreach-call) 9.8 5.2 160 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   870   8800 1800 2.3 0      error (invalid witness file) .55 .35 13   42 error (invalid witness file) 5.7 3.0 78 310 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 7.3 2.3 65 350 2.5 0      true 4.8  2.6  81   290 false(unreach-call) 10   5.4 170 370 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error 0 wit inspect 8.7 2.8 62 310 2.6 0      error (invalid witness file) .55 .36 9.9 43 error (invalid witness file) 5.3 2.9 84 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.2 2.2 56 350 2.5 0      true 5.1  2.8  65   290 false(unreach-call) 9.4 4.9 150 330 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.6 2.5 65 410 2.5 0      true 7.0  3.8  70   280 false(unreach-call) 12   6.2 200 370 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 16   6.2 130 500 2.5 0      true 4.9  2.6  58   290 false(unreach-call) 10   5.4 220 360 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 49   34   560 700 2.5 0      true 5.6  3.0  80   290 false(unreach-call) 14   7.6 210 400 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   170   3400 13000 2.3 0      error (invalid witness file) .53 .32 9.0 40 error (invalid witness file) 6.3 3.3 140 300 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 11   3.6 88 530 2.5 0      true 5.3  2.8  63   290 false(unreach-call) 16   8.6 240 430 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 2.0 50 360 2.5 0      true 4.6  2.5  49   290 false(unreach-call) 9.7 5.1 160 360 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   880   6400 3000 2.3 0      error (invalid witness file) .53 .34 8.8 40 error (invalid witness file) 6.1 3.2 99 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 8.3 2.4 66 360 2.5 0      true 4.8  2.6  66   280 false(unreach-call) 11   5.7 190 360 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error 0 wit inspect 8.1 2.7 64 310 2.6 0      error (invalid witness file) .46 .31 5.4 39 error (invalid witness file) 6.0 3.2 86 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.8 2.1 50 360 2.5 0      true 4.9  2.7  67   280 false(unreach-call) 8.2 4.4 110 330 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   810   11000 1600 2.3 0      error (invalid witness file) .51 .33 8.6 39 error (invalid witness file) 5.8 3.1 120 300 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.7 2.3 58 350 2.5 0      true 5.6  3.1  88   280 false(unreach-call) 9.2 4.9 130 360 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   390   5200 13000 2.3 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.3 3.3 100 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   640   7700 8400 2.3 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 5.8 3.1 97 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   310   5100 13000 2.3 0      - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.7 3.5 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   9100 2200 2.3 0      - - error (invalid witness file) .55 .36 11   40 error (invalid witness file) 6.1 3.2 94 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   160   3400 13000 2.3 0      - - error (invalid witness file) .63 .40 9.1 40 error (invalid witness file) 6.1 3.2 130 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.3 2.7 64 310 2.6 0      - - error (invalid witness file) .57 .38 10   43 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   240   5000 14000 2.3 0      - - error (invalid witness file) .54 .35 9.6 40 error (invalid witness file) 6.5 3.4 110 290
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   220   3900 13000 2.3 0      - - error (invalid witness file) .59 .37 7.6 41 error (invalid witness file) 6.3 3.3 110 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   590   8700 8500 2.3 0      - - error (invalid witness file) .70 .45 9.6 45 error (invalid witness file) 6.9 3.6 70 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   6500 5000 2.3 0      - - error (invalid witness file) .60 .39 9.3 40 error (invalid witness file) 5.8 3.1 77 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   390   5900 13000 2.3 0      - - error (invalid witness file) .60 .38 7.6 39 error (invalid witness file) 6.0 3.2 100 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   170   3200 13000 2.3 0      - - error (invalid witness file) .57 .35 12   44 error (invalid witness file) 6.0 3.2 130 290
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   13000 2100 2.3 0      - - error (invalid witness file) .67 .43 7.7 39 error (invalid witness file) 5.8 3.1 93 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   5800 5300 2.3 0      - - error (invalid witness file) .56 .36 9.4 40 error (invalid witness file) 5.6 3.0 130 290
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880   6700 3400 2.3 0      - - error (invalid witness file) .65 .42 7.6 40 error (invalid witness file) 6.0 3.2 92 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   820   11000 2600 2.3 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.8 3.1 110 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.8 2.7 74 340 2.6 0      - - error (invalid witness file) .58 .37 10   39 error (invalid witness file) 6.3 3.4 140 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   7100 5300 2.3 0      - - error (invalid witness file) .63 .40 8.0 40 error (invalid witness file) 6.5 3.4 130 290
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   240   5000 13000 2.3 0      - - error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 6.1 3.2 110 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   390   6600 13000 2.3 0      - - error (invalid witness file) .59 .37 9.3 39 error (invalid witness file) 5.6 3.0 88 290
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   780   7200 4900 2.3 0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 5.8 3.0 92 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 6.4 2.0 50 360 2.5 0      true 4.7  2.6  36   290 false(unreach-call) 8.7 4.6 150 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   880   9200 1300 2.3 0      error (invalid witness file) .52 .35 9.6 41 error (invalid witness file) 7.2 3.7 120 320 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.7 2.0 49 370 2.5 0      true 5.2  2.8  61   290 false(unreach-call) 9.5 5.0 120 330 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i timeout 0 wit inspect 900   250   4000 13000 2.3 0      error (invalid witness file) .56 .38 7.2 41 error (invalid witness file) 5.5 3.0 68 300 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i timeout 0 wit inspect 900   770   6600 5900 2.3 0      - - error (invalid witness file) .71 .45 9.9 42 error (invalid witness file) 5.7 3.1 110 290
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 9.8 3.0 81 400 2.5 0      true 5.6  3.1  74   290 false(unreach-call) 8.9 4.7 160 320 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900   760   5200 7300 2.3 0      - - error (invalid witness file) .66 .41 8.2 40 error (invalid witness file) 5.9 3.2 96 300
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 900   850   10000 5300 2.3 0      error (invalid witness file) .50 .32 8.9 40 error (invalid witness file) 6.2 3.3 130 300 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   850   10000 4300 2.3 0      - - error (invalid witness file) .56 .34 11   40 error (invalid witness file) 6.4 3.3 120 310
../../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 177 49000 36000 420000 380000 430 .0041 173 230 130 3300 13000   173 950 550 14000 41000   173 400 220 5900 20000   173 1100 650 17000 38000  
    correct results 113 177 2600 1700 22000 53000 290 .0041 38 220 120 3100 13000   46 850 490 12000 36000   60 370 200 5500 19000   63 830 500 13000 25000  
        correct true 64 128 1100 630 10000 29000 170 .0041 33 0 0 0 0   0 0 0 0 0   60 370 200 5500 19000   63 830 500 13000 25000  
        correct false 49 49 1500 1000 12000 24000 120 0      5 220 120 3100 13000   46 850 490 12000 36000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (173 tasks, max score: 280) 177
Run set sv-comp17.ReachSafety-Heap