Tool skink
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-13 11:09:20 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 01:53:26 CET ]] [[ 2017-01-15 01:38:17 CET ]] [[ 2017-01-15 01:54:04 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/skink.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/skink.2017-01-13_1109.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)
loops/array_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.1 2.0 49 340 .037  0      false(unreach-call) 4.2  2.4  51   280 false(unreach-call) 8.7 4.6 84 320 - -
loops/bubble_sort_false-unreach-call.i unknown 0 wit inspect 38   20   300 1100 .037  0      error (invalid witness file) .57 .37 7.8 40 error (invalid witness file) 7.1 3.8 90 310 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.9 1.7 40 300 .037  0      false(unreach-call) 4.0  2.2  41   270 false(unreach-call) 8.4 4.5 66 310 - -
loops/eureka_01_false-unreach-call.i unknown 0 wit inspect 15   5.9 130 660 .037  0      error (invalid witness file) .51 .32 8.9 40 error (invalid witness file) 6.1 3.3 94 300 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.0 2.3 56 360 .037  0      false(unreach-call) 3.9  2.2  69   270 false(unreach-call) 11   5.8 160 340 - -
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 wit inspect 900   800   8200 1700 .0041 0      error (invalid witness file) .49 .32 9.3 40 error (invalid witness file) 6.6 3.5 93 300 - -
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 14   5.8 130 640 .037  0      timeout 96    80    1100   2300 false(unreach-call) 12   6.4 200 370 - -
loops/linear_search_false-unreach-call.i unknown 0 wit inspect 6.1 1.9 50 350 .037  0      error (invalid witness file) .52 .34 9.1 44 error (invalid witness file) 6.9 3.6 91 300 - -
loops/ludcmp_false-unreach-call.i unknown 0 wit inspect 10   3.9 94 680 .037  0      error (invalid witness file) .52 .33 12   40 error (invalid witness file) 7.5 3.9 76 310 - -
loops/matrix_false-unreach-call_true-termination.i unknown 0 wit inspect 5.9 2.0 47 320 .037  0      error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.8 3.6 91 290 - -
loops/n.c24_false-unreach-call.i unknown 0 wit inspect 5.1 1.6 41 330 .037  0      error (invalid witness file) .51 .34 8.5 41 error (invalid witness file) 7.0 3.7 93 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 5.3 1.8 41 320 .037  0      false(unreach-call) 3.7  2.1  46   280 false(unreach-call) 9.3 4.9 97 320 - -
loops/nec20_false-unreach-call_true-termination.i timeout 0 wit inspect 900   820   12000 1000 .0041 0      error (invalid witness file) .49 .31 7.8 40 error (invalid witness file) 6.7 3.5 71 290 - -
loops/s3_false-unreach-call.i unknown 0 wit inspect 32   13   250 1100 .037  0      error (invalid witness file) .55 .35 9.2 45 error (invalid witness file) 7.2 3.8 110 310 - -
loops/string_false-unreach-call_true-termination.i unknown 0 wit inspect 6.6 2.1 53 330 .037  0      error (invalid witness file) .49 .31 8.6 40 error (invalid witness file) 6.9 3.6 68 310 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 66   50   800 690 .0041 0      false(unreach-call) 4.2  2.3  78   270 false(unreach-call) 12   6.3 160 340 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 8.7 2.8 65 380 .037  3.1    false(unreach-call) 4.1  2.3  74   290 false(unreach-call) 17   9.0 230 380 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 410   360   4200 700 .0041 0      false(unreach-call) 4.5  2.5  81   280 false(unreach-call) 15   8.2 140 560 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 24   13   240 680 .037  0      true 4.2  2.4  43   260 false(unreach-call) 15   8.4 260 510 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 17   7.9 160 570 .037  .0082 false(unreach-call) 4.7  2.6  45   270 false(unreach-call) 12   6.5 98 410 - -
loops/sum_array_false-unreach-call.i false(unreach-call) 1 wit inspect 14   5.6 110 660 .0041 0      timeout 98    84    2100   2700 false(unreach-call) 13   6.9 130 370 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.1 1.7 41 330 .037  0      false(unreach-call) 3.8  2.1  62   270 false(unreach-call) 8.2 4.4 100 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.2 1.7 39 340 .037  0      false(unreach-call) 3.8  2.1  70   280 false(unreach-call) 7.8 4.1 130 320 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.0 1.9 50 340 .037  .0082 false(unreach-call) 3.9  2.2  50   280 false(unreach-call) 9.6 5.0 120 340 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.7 2.4 63 450 .037  0      false(unreach-call) 4.0  2.2  65   280 false(unreach-call) 10   5.3 120 350 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.2 1.7 39 330 .037  0      false(unreach-call) 3.5  2.0  71   270 false(unreach-call) 9.4 5.0 100 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.8 1.9 44 320 .037  0      false(unreach-call) 4.5  2.5  44   280 false(unreach-call) 7.5 4.0 150 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i unknown 0 wit inspect 5.4 1.7 46 340 .037  0      error (invalid witness file) .47 .31 6.1 41 error (invalid witness file) 7.3 3.9 56 290 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i unknown 0 wit inspect 5.7 1.9 39 350 .037  0      error (invalid witness file) .52 .33 12   41 error (invalid witness file) 7.2 3.8 70 300 - -
loops/vogal_false-unreach-call.i unknown 0 wit inspect 6.2 2.0 44 350 .037  0      error (invalid witness file) .49 .33 8.7 40 error (invalid witness file) 7.2 3.8 77 300 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 4.6 1.6 35 330 .037  0      false(unreach-call) 4.2  2.4  39   280 true 8.6 4.6 70 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect 11   3.8 91 440 .037  0      - - true 4.4  2.5  91   300 true 13   6.8 150 360
loops/bubble_sort_true-unreach-call.i unknown 0 wit inspect 6.3 1.9 47 380 .037  0      - - error (invalid witness file) .48 .31 10   40 error (invalid witness file) 6.7 3.6 71 300
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 7.3 2.3 65 360 .037  0      - - out of memory 330    320    7600   7000 true 72   64   1600 400
loops/eureka_01_true-unreach-call.i unknown 0 wit inspect 8.5 2.7 70 430 .037  0      - - error (invalid witness file) .46 .30 9.1 39 error (invalid witness file) 7.4 3.9 79 310
loops/eureka_05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   11000 1400 .0041 0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 7.3 3.9 75 290
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 6.0 1.9 49 350 .037  0      - - true 3.8  2.1  65   270 true 8.8 4.8 100 330
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 6.0 1.9 47 340 .037  0      - - true 3.8  2.1  45   280 true 6.9 3.7 100 320
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   7800 1400 .0041 0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 5.4 2.9 99 290
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect 46   33   580 700 .037  0      - - true 18    11    290   540 true 44   30   1100 730
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect 6.2 2.0 55 360 .037  0      - - error (invalid witness file) .48 .30 9.4 40 error (invalid witness file) 7.3 3.8 89 300
loops/lu.cmp_true-unreach-call.i unknown 0 wit inspect 11   4.1 96 710 .037  0      - - error (invalid witness file) .57 .36 9.3 41 error (invalid witness file) 6.6 3.5 88 310
loops/matrix_true-unreach-call_true-termination.i unknown 0 wit inspect 5.3 1.8 39 330 .037  .0082 - - error (invalid witness file) .50 .32 14   39 error (invalid witness file) 6.6 3.5 83 300
loops/n.c11_true-unreach-call_false-termination.i true 2 wit inspect 39   26   440 700 .037  0      - - out of memory 230    220    4700   7000 true 12   6.7 140 360
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 6.2 1.9 47 340 .037  0      - - true 3.8  2.1  73   270 true 230   220   4400 750
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 6.7 2.2 55 340 .037  0      - - true 4.4  2.4  56   280 true 210   200   5000 790
loops/string_true-unreach-call_true-termination.i unknown 0 wit inspect 470   430   5900 990 .0041 0      - - error (invalid witness file) .46 .30 11   39 error (invalid witness file) 7.5 3.9 83 300
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 8.1 2.6 60 370 .037  0      - - timeout 900    900    21000   3400 true 13   6.9 200 430
loops/sum03_true-unreach-call_false-termination.i true 2 wit inspect 6.7 2.2 52 340 .037  0      - - true 4.0  2.2  72   270 true 7.9 4.2 110 320
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 14   6.2 130 480 .037  0      - - true 4.4  2.4  63   280 true 12   6.5 150 410
loops/sum_array_true-unreach-call.i timeout 0 wit inspect 900   840   12000 1200 .0041 0      - - error (invalid witness file) .51 .32 9.9 40 error (invalid witness file) 6.3 3.3 58 300
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 10   3.4 93 530 .037  0      - - true 4.0  2.2  75   270 true 7.2 3.9 99 320
loops/terminator_03_true-unreach-call_true-termination.i true 2 wit inspect 7.6 2.3 60 350 .037  0      - - true 4.1  2.3  76   280 true 8.4 4.5 120 320
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 9.5 3.0 86 540 .037  .0082 - - out of memory 510    470    8600   7000 true 7.7 4.1 120 320
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 5.9 1.9 50 340 .037  0      - - true 3.9  2.2  64   280 true 9.2 4.9 110 320
loops/trex03_true-unreach-call_true-termination.i timeout 0 wit inspect 900   850   7100 1300 .0041 0      - - error (invalid witness file) .52 .32 10   40 error (invalid witness file) 6.9 3.6 67 290
loops/trex04_true-unreach-call_false-termination.i timeout 0 wit inspect 900   800   12000 1000 .0041 0      - - error (invalid witness file) .46 .30 11   39 error (invalid witness file) 7.4 3.9 83 300
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i unknown 0 wit inspect 5.3 1.7 43 340 .037  0      - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 8.0 4.2 98 310
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i unknown 0 wit inspect 5.5 1.8 50 360 .037  0      - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 5.4 2.9 81 300
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect 38   25   370 700 .037  0      - - true 4.5  2.5  94   290 true 7.9 4.3 100 320
loops/vogal_true-unreach-call.i unknown 0 wit inspect 6.1 1.9 57 330 .037  0      - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 5.6 3.0 91 300
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2 wit inspect 5.4 1.8 40 360 .037  0      - - true 3.6  2.0  61   270 true 8.7 4.7 73 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect 5.4 1.9 40 340 .037  0      - - true 4.8  2.6  40   270 true 9.3 4.9 120 330
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2 wit inspect 5.5 1.7 42 330 .037  0      - - true 3.9  2.2  79   280 true 8.7 4.6 110 320
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   810   8400 1000 .0041 0      error (invalid witness file) .63 .41 7.6 41 error (invalid witness file) 7.3 3.9 72 300 - -
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   820   11000 1100 .0041 0      error (invalid witness file) .51 .32 9.2 40 error (invalid witness file) 6.1 3.2 110 300 - -
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   810   10000 1100 .0041 0      error (invalid witness file) .52 .34 9.7 40 error (invalid witness file) 5.9 3.1 100 300 - -
loop-acceleration/const_false-unreach-call1.i timeout 0 wit inspect 900   800   12000 1000 .0041 0      error (invalid witness file) .56 .36 9.4 45 error (invalid witness file) 7.5 4.0 86 310 - -
loop-acceleration/diamond_false-unreach-call1.i timeout 0 wit inspect 900   810   11000 1000 .0041 0      error (invalid witness file) .53 .35 9.7 39 error (invalid witness file) 6.8 3.5 96 300 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   810   12000 1000 .0041 0      error (invalid witness file) .52 .33 9.6 42 error (invalid witness file) 6.2 3.3 91 300 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect 5.0 1.8 37 330 .037  0      false(unreach-call) 4.4  2.5  47   270 false(unreach-call) 8.5 4.6 100 310 - -
loop-acceleration/nested_false-unreach-call1.i timeout 0 wit inspect 900   800   11000 1100 .0041 .0082 error (invalid witness file) .51 .32 9.8 42 error (invalid witness file) 7.0 3.7 74 300 - -
loop-acceleration/phases_false-unreach-call1.i timeout 0 wit inspect 900   800   10000 1000 .0041 0      error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.0 3.2 94 300 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect 5.0 1.7 40 330 .037  0      false(unreach-call) 3.4  1.9  37   270 false(unreach-call) 8.4 4.4 110 320 - -
loop-acceleration/simple_false-unreach-call1.i timeout 0 wit inspect 900   800   9900 1000 .0041 0      error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.2 3.3 100 300 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect 5.0 1.7 46 340 .037  0      false(unreach-call) 4.5  2.5  47   270 false(unreach-call) 9.0 4.7 85 320 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect 4.9 1.6 38 350 .037  0      false(unreach-call) 3.6  2.0  55   280 false(unreach-call) 8.3 4.5 94 310 - -
loop-acceleration/simple_false-unreach-call4.i timeout 0 wit inspect 900   800   11000 1000 .0041 0      error (invalid witness file) .52 .33 9.8 41 error (invalid witness file) 7.6 4.0 85 300 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect 9.1 3.1 69 380 .037  0      true 4.1  2.3  40   270 true 9.6 5.1 97 320 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect 9.0 3.1 72 360 .0041 0      true 3.3  1.9  54   270 true 8.8 4.8 120 320 - -
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   810   9200 1000 .0041 0      - - error (invalid witness file) .50 .33 9.7 40 error (invalid witness file) 7.5 3.9 93 310
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   820   11000 1000 .0041 0      - - error (invalid witness file) .49 .32 9.0 41 error (invalid witness file) 5.7 3.0 93 300
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   820   9200 1000 .0041 0      - - error (invalid witness file) .48 .32 8.1 39 error (invalid witness file) 6.7 3.6 100 300
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   810   11000 1000 .0041 0      - - error (invalid witness file) .50 .32 14   40 error (invalid witness file) 6.4 3.4 71 290
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect 5.4 1.8 49 340 .037  0      - - true 4.2  2.3  76   290 timeout 960   810   25000 2500
loop-acceleration/diamond_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   810   9900 1000 .0041 0      - - error (invalid witness file) .55 .36 8.8 40 error (invalid witness file) 6.6 3.5 91 310
loop-acceleration/diamond_true-unreach-call2.i timeout 0 wit inspect 900   840   9000 1100 .0041 0      - - error (invalid witness file) .53 .34 9.1 39 error (invalid witness file) 5.8 3.1 100 300
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   810   10000 1000 .0041 0      - - error (invalid witness file) .52 .34 8.2 42 error (invalid witness file) 8.0 4.2 110 320
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 5.8 1.9 43 340 .037  0      - - out of memory 360    350    8800   7000 true 7.5 4.0 110 330
loop-acceleration/nested_true-unreach-call1.i timeout 0 wit inspect 900   800   9500 1000 .0041 .0082 - - error (invalid witness file) .47 .31 6.6 40 error (invalid witness file) 6.1 3.2 87 280
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect 5.9 1.8 46 340 .037  0      - - out of memory 390    380    8500   7000 timeout 960   810   18000 2400
loop-acceleration/phases_true-unreach-call1.i timeout 0 wit inspect 900   800   10000 1000 .0041 0      - - error (invalid witness file) .54 .35 13   44 error (invalid witness file) 6.2 3.3 110 310
loop-acceleration/phases_true-unreach-call2_false-termination.i unknown 0 wit inspect 43   34   500 690 .0041 0      - - error (invalid witness file) .50 .32 9.8 41 error (invalid witness file) 6.2 3.3 89 290
loop-acceleration/simple_true-unreach-call1.i timeout 0 wit inspect 900   800   12000 1000 .0041 .0041 - - error (invalid witness file) .60 .39 5.2 40 error (invalid witness file) 6.6 3.5 80 300
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 5.5 1.8 44 340 .037  0      - - true 3.8  2.1  73   280 true 8.3 4.4 120 320
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect 6.7 2.2 54 350 .037  0      - - timeout 910    900    17000   6300 timeout 960   920   20000 850
loop-acceleration/simple_true-unreach-call4.i timeout 0 wit inspect 900   800   9600 1000 .0041 0      - - error (invalid witness file) .53 .34 9.7 44 error (invalid witness file) 7.5 3.9 77 300
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 11   4.2 92 450 .037  0      - - true 6.7  4.7  110   400 true 66   58   1400 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 9.7 3.5 83 370 .037  0      - - true 3.8  2.1  62   280 true 12   6.4 140 390
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 7.0 2.2 59 360 .037  0      false(unreach-call) 3.7  2.1  47   270 false(unreach-call) 13   7.0 130 360 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 12   4.2 110 530 .037  .0082 - - timeout 900    900    20000   2300 true 13   6.8 140 360
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 11   3.5 79 430 .0041 0      - - out of memory 470    460    9800   7000 true 12   6.4 170 370
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout 0 wit inspect 900   830   9300 1200 .0041 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.9 3.6 95 300
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 780   740   11000 990 .0041 0      - - timeout 900    890    20000   3200 true 15   8.2 170 470
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   11000 1200 .0041 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.7 3.0 86 290
loop-invgen/down_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   12000 1000 .0041 0      - - error (invalid witness file) .52 .32 9.1 39 error (invalid witness file) 7.3 3.8 80 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   11000 1100 .0041 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.5 3.0 75 290
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   12000 1000 .0041 0      - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.7 3.5 100 320
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   840   9900 1300 .0041 0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.5 3.0 77 290
loop-invgen/id_build_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810   7100 1600 .0041 0      - - error (invalid witness file) .61 .38 9.7 39 error (invalid witness file) 7.3 3.8 73 300
loop-invgen/large_const_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810   7900 1500 .0041 0      - - error (invalid witness file) .53 .34 11   42 error (invalid witness file) 7.0 3.7 84 300
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   6300 1600 .0041 0      - - error (invalid witness file) .49 .33 11   40 error (invalid witness file) 7.0 3.7 73 300
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 0 wit inspect 910   850   6100 1500 .0041 .0082 - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.1 3.2 97 310
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 0 wit inspect 900   800   7800 1600 .0041 0      - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 7.5 3.9 84 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 48   34   500 710 .0041 0      - - out of memory 510    500    8500   7000 true 21   12   310 590
loop-invgen/seq_true-unreach-call_true-termination.i timeout 0 wit inspect 900   830   9900 1000 .0041 0      - - error (invalid witness file) .52 .33 9.5 40 error (invalid witness file) 6.9 3.7 91 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   10000 1100 .0041 0      - - error (invalid witness file) .58 .39 6.2 39 error (invalid witness file) 7.7 4.0 71 290
loop-invgen/up_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   12000 1000 .0041 0      - - error (invalid witness file) .60 .39 8.0 40 error (invalid witness file) 8.1 4.2 86 320
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   810   10000 1000 .0041 0      - - error (invalid witness file) .49 .31 8.1 39 error (invalid witness file) 6.9 3.6 58 300
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 29   16   250 670 .037  0      - - timeout 900    900    17000   890 true 14   7.4 140 400
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 9.2 3.1 77 380 .037  0      - - true 4.3  2.4  79   280 true 11   5.8 150 370
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 8.2 2.7 71 350 .037  0      - - out of memory 360    350    7800   7000 true 10   5.7 180 360
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 910   620   6000 1700 .0041 0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 7.2 3.9 63 290
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   830   7100 1400 .0041 0      - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.5 3.4 79 310
loop-lit/ddlm2013_true-unreach-call.i timeout 0 wit inspect 900   830   11000 1100 .0041 0      - - error (invalid witness file) .64 .41 7.0 42 error (invalid witness file) 6.8 3.6 100 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   810   11000 1000 .0041 0      - - error (invalid witness file) .50 .32 9.7 40 error (invalid witness file) 5.5 3.0 110 290
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 28   16   280 680 .037  0      - - timeout 900    900    16000   3700 true 12   6.6 160 370
loop-lit/gr2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   800   9300 1300 .0041 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.3 3.4 95 300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i true 2 wit inspect 17   8.1 170 520 .0041 0      - - timeout 900    900    16000   1300 true 8.1 4.4 150 330
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 7.0 2.3 61 350 .037  0      - - out of memory 330    320    8300   7000 true 11   6.2 180 380
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 6.8 2.2 57 330 .037  0      - - out of memory 370    360    6600   7000 true 14   7.8 190 430
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 9.2 3.1 75 380 .037  0      - - out of memory 320    310    6200   7000 true 13   7.3 160 400
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 5.7 1.8 41 350 .037  0      - - error (invalid witness file) .47 .31 6.1 39 error (invalid witness file) 7.2 3.7 94 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 5.9 1.9 48 350 .037  0      false(unreach-call) 3.7  2.1  50   280 false(unreach-call) 9.4 4.9 93 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   800   11000 1000 .0041 0      - - error (invalid witness file) .51 .33 13   41 error (invalid witness file) 6.4 3.4 89 300
loop-new/count_by_1_variant_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810   10000 1000 .0041 0      - - error (invalid witness file) .51 .32 9.6 40 error (invalid witness file) 7.2 3.8 82 300
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   800   10000 1100 .0041 0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 8.1 4.2 87 310
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810   11000 1000 .0041 0      - - error (invalid witness file) .57 .36 11   42 error (invalid witness file) 6.5 3.5 91 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820   10000 1000 .0041 0      - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.8 3.6 79 300
loop-new/gauss_sum_true-unreach-call_true-termination.i timeout 0 wit inspect 900   870   11000 1000 .0041 0      - - error (invalid witness file) .52 .33 7.3 40 error (invalid witness file) 7.7 4.1 75 300
loop-new/half_true-unreach-call_true-termination.i timeout 0 wit inspect 900   770   7300 1500 .0041 0      - - error (invalid witness file) .57 .36 8.8 39 error (invalid witness file) 7.3 3.9 81 300
loop-new/nested_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810   12000 1100 .0041 0      - - error (invalid witness file) .50 .31 10   40 error (invalid witness file) 5.0 2.7 76 290
loop-industry-pattern/aiob_1_true-unreach-call.c unknown 0 wit inspect 8.6 2.7 70 670 .037  0      - - error (invalid witness file) .58 .37 7.8 41 error (invalid witness file) 7.4 3.9 82 300
loop-industry-pattern/aiob_2_true-unreach-call.c unknown 0 wit inspect 8.9 2.9 62 680 .037  0      - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.0 3.2 61 310
loop-industry-pattern/aiob_3_true-unreach-call.c unknown 0 wit inspect 8.3 2.7 72 670 .037  0      - - error (invalid witness file) .61 .40 8.0 41 error (invalid witness file) 6.0 3.1 91 300
loop-industry-pattern/aiob_4_true-unreach-call.c unknown 0 wit inspect 8.4 2.7 68 660 .037  0      - - error (invalid witness file) .51 .32 8.3 39 error (invalid witness file) 5.7 3.1 110 300
loop-industry-pattern/mod3_true-unreach-call.c unknown 0 wit inspect 6.6 2.1 52 340 .037  0      - - error (invalid witness file) .59 .39 6.8 40 error (invalid witness file) 7.0 3.7 81 300
loop-industry-pattern/nested_true-unreach-call.c timeout 0 wit inspect 900   820   6100 1300 .0041 .0082 - - error (invalid witness file) .48 .32 6.9 40 error (invalid witness file) 7.6 4.0 84 310
loop-industry-pattern/ofuf_1_true-unreach-call.c unknown 0 wit inspect 40   14   260 1300 .037  0      - - error (invalid witness file) .51 .32 9.2 39 error (invalid witness file) 7.7 4.0 78 310
loop-industry-pattern/ofuf_2_true-unreach-call.c unknown 0 wit inspect 38   14   280 1300 .037  0      - - error (invalid witness file) .49 .32 8.3 40 error (invalid witness file) 8.2 4.3 90 310
loop-industry-pattern/ofuf_3_true-unreach-call.c unknown 0 wit inspect 40   14   270 1300 .037  0      - - error (invalid witness file) .48 .31 10   40 error (invalid witness file) 6.1 3.2 78 300
loop-industry-pattern/ofuf_4_true-unreach-call.c unknown 0 wit inspect 61   16   370 1400 .037  0      - - error (invalid witness file) .51 .33 9.6 41 error (invalid witness file) 6.1 3.3 85 290
loop-industry-pattern/ofuf_5_true-unreach-call.c unknown 0 wit inspect 42   14   280 1300 .037  0      - - error (invalid witness file) .48 .32 8.3 40 error (invalid witness file) 7.0 3.7 80 290
loops/heavy_true-unreach-call.c unknown 0 wit inspect 8.4 3.4 73 700 .037  0      - - error (invalid witness file) .50 .31 6.5 39 error (invalid witness file) 7.0 3.6 85 300
loops/compact_false-unreach-call.c timeout 0 wit inspect 900   810   9000 1000 .0041 0      error (invalid witness file) .49 .30 8.2 40 error (invalid witness file) 7.3 3.8 73 290 - -
loops/heavy_false-unreach-call.c unknown 0 wit inspect 8.3 3.3 61 710 .037  0      error (invalid witness file) .47 .32 6.3 40 error (invalid witness file) 7.6 3.9 97 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 156 98 55000 49000   600000 120000 3.5   3.2   156 300   230   4800 13000   156 440 230   5400 17000   156 11000 10000 220000 110000   156 4300 3500 86000 40000  
    correct results 60 96 1900 1500   22000 27000 2.0   3.1   22 280   210   4500 11000   24 250 130   3000 8500   20 9300 9100 190000 91000   35 1900 1500 43000 17000  
        correct true 36 72 1300 980   16000 16000 1.2   .016 1 0   0   0 0   1 0 0   0 0   20 9300 9100 190000 91000   35 1900 1500 43000 17000  
        correct false 24 24 650 480   6400 10000 .79  3.1   21 280   210   4500 11000   23 250 130   3000 8500   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 2 31 10   240 1400 .11  0     2 7.5 4.2 94 550   2 18 9.9 220 640   0 1300 1300 26000 13000   0 1900 1700 37000 3300  
        correct-unconfirmed true 2 2 13 4.0 100 690 .074 0     2 0   0   0 0   2 0 0   0 0   0 1300 1300 26000 13000   0 1900 1700 37000 3300  
        correct-unconfirmed false 2 0 18 6.2 140 750 .041 0     0 7.5 4.2 94 550   0 18 9.9 220 640   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (156 tasks, max score: 261) 98
Run set sv-comp17.ReachSafety-Loops