Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 .18 .18 1.6 10   .012 .45   false(unreach-call) 4.7  2.7  70   290 false(unreach-call) 10   5.5 110 340 - -
loops/bubble_sort_false-unreach-call.i false(unreach-call) 1 wit inspect .25 .25 2.4 10   .066 0      false(unreach-call) 8.6  4.6  91   330 error 13   6.8 150 300 - -
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 .16 1.6 9.5 .012 0      false(unreach-call) 3.5  2.0  67   270 false(unreach-call) 7.3 3.9 150 300 - -
loops/eureka_01_false-unreach-call.i false(unreach-call) 0 wit inspect .44 .44 5.2 13   .012 0      timeout 98    81    1700   2300 true 9.2 4.9 120 330 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .18 .18 1.6 9.2 .012 0      timeout 97    79    2400   3700 true 7.8 4.1 130 320 - -
loops/insertion_sort_false-unreach-call_true-termination.i unknown 0 wit inspect .18 .18 1.7 10   .012 0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.4 3.4 93 290 - -
loops/invert_string_false-unreach-call_true-termination.i error 0 wit inspect .19 .19 1.8 10   .012 0      error (invalid witness file) .69 .44 5.3 40 error (invalid witness file) 8.1 4.2 82 310 - -
loops/linear_search_false-unreach-call.i error 0 wit inspect .24 .38 2.2 21   .012 12      error (invalid witness file) .56 .36 12   43 error (invalid witness file) 6.3 3.4 90 300 - -
loops/ludcmp_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .15 1.9 9.4 .012 0      false(unreach-call) 13    9.8  270   950 out of memory 52   41   1000 7000 - -
loops/matrix_false-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    8800   2400   .012 0      error (invalid witness file) .52 .35 12   40 error (invalid witness file) 6.0 3.1 110 300 - -
loops/n.c24_false-unreach-call.i timeout (timeout) 0 wit inspect 900    900    10000   3800   .037 0      error (invalid witness file) .58 .39 12   41 error (invalid witness file) 7.5 3.9 74 300 - -
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .16 .16 1.7 9.3 .012 0      false(unreach-call) 3.6  2.0  62   260 false(unreach-call) 6.9 3.7 120 320 - -
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 .17 1.6 9.4 .012 0      false(unreach-call) 4.1  2.3  72   290 true 7.9 4.3 130 320 - -
loops/s3_false-unreach-call.i error 0 wit inspect .36 .35 4.6 12   .20  0      error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.5 3.4 96 290 - -
loops/string_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 .18 2.0 9.9 .012 0      false(unreach-call) 5.4  3.0  75   300 true 8.2 4.4 170 330 - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15 .15 1.7 9.3 .012 0      false(unreach-call) 5.8  3.2  49   290 false(unreach-call) 19   11   210 480 - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 .17 1.6 9.3 .012 0      false(unreach-call) 4.4  2.5  63   270 false(unreach-call) 15   8.1 210 370 - -
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 .16 2.0 9.4 .012 0      false(unreach-call) 4.4  2.5  79   280 false(unreach-call) 18   9.9 290 540 - -
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .14 .14 2.0 9.4 .012 0      true 4.0  2.2  77   280 true 8.3 4.4 120 330 - -
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .16 .15 1.5 9.2 .012 0      false(unreach-call) 4.0  2.2  85   280 true 7.6 4.0 110 330 - -
loops/sum_array_false-unreach-call.i unknown 0 wit inspect .20 .19 1.8 10   .012 0      error (invalid witness file) .47 .31 11   39 error (invalid witness file) 7.0 3.8 81 290 - -
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 .16 1.4 9.5 .012 0      false(unreach-call) 3.6  2.0  72   280 true 7.2 3.8 84 320 - -
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 .18 1.8 9.4 .012 0      false(unreach-call) 3.8  2.1  74   280 false(unreach-call) 8.4 4.4 140 330 - -
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .17 .17 1.6 9.3 .012 0      false(unreach-call) 3.7  2.1  61   280 false(unreach-call) 7.4 3.9 120 320 - -
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 .18 1.8 9.4 .012 0      false(unreach-call) 3.8  2.2  80   280 false(unreach-call) 9.6 5.1 100 320 - -
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .15 .15 1.8 10   .012 0      false(unreach-call) 3.4  1.9  65   270 false(unreach-call) 7.3 4.0 130 320 - -
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 .19 1.8 10   .012 .45   false(unreach-call) 3.6  2.0  48   270 false(unreach-call) 7.2 3.8 160 320 - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .16 .16 1.6 9.3 .012 0      true 3.9  2.2  60   270 true 9.6 5.2 100 320 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .21 .21 2.2 10   .016 0      timeout 92    80    3100   1600 false(unreach-call) 18   9.9 150 570 - -
loops/vogal_false-unreach-call.i false(unreach-call) 1 wit inspect .18 .18 1.9 10   .012 0      false(unreach-call) 8.9  5.0  150   340 true 15   7.8 150 360 - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .13 .13 1.6 9.3 .012 0      false(unreach-call) 4.6  2.6  51   270 false(unreach-call) 6.9 3.7 140 320 - -
loops/array_true-unreach-call_true-termination.i true 2 wit inspect .15 .15 1.7 10   .012 0      - - true 4.4  2.5  74   280 true 10   5.4 160 360
loops/bubble_sort_true-unreach-call.i true 2 wit inspect .18 .18 1.6 9.4 .012 0      - - true 4.0  2.2  85   270 true 7.3 4.0 140 320
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect .14 .14 1.3 9.3 .012 0      - - out of memory 320    320    5800   7000 true 57   50   1400 410
loops/eureka_01_true-unreach-call.i true 1 wit inspect .17 .17 1.6 9.1 .012 0      - - out of memory 640    610    8800   7000 timeout 960   840   21000 4000
loops/eureka_05_true-unreach-call_true-termination.i true 2 wit inspect .16 .16 1.4 9.2 .012 0      - - true 500    470    6600   5200 true 35   20   400 740
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 890    930    13000   15000   .012 0      - - error (invalid witness file) .53 .35 10   44 error (invalid witness file) 7.0 3.7 120 330
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 890    930    11000   15000   .012 0      - - error (invalid witness file) .61 .39 9.1 43 error (invalid witness file) 5.9 3.2 110 300
loops/insertion_sort_true-unreach-call_true-termination.i unknown 0 wit inspect .16 .16 2.0 9.9 .012 0      - - error (invalid witness file) .62 .38 8.3 43 error (invalid witness file) 7.0 3.7 83 300
loops/invert_string_true-unreach-call_true-termination.i true 2 wit inspect .17 .16 1.8 9.3 .012 0      - - true 27    16    280   560 true 42   27   970 690
loops/linear_sea.ch_true-unreach-call.i unknown 0 wit inspect .19 .18 1.9 10   .012 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.2 3.3 130 300
loops/lu.cmp_true-unreach-call.i true 1 wit inspect .17 .17 1.6 9.4 .012 0      - - timeout 910    860    17000   5600 out of memory 52   42   1000 7000
loops/matrix_true-unreach-call_true-termination.i true 2 wit inspect .18 .17 1.7 10   .012 0      - - true 8.4  6.2  210   420 true 12   6.8 220 380
loops/n.c11_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    900    13000   76   .012 0      - - error (invalid witness file) .68 .42 11   44 error (invalid witness file) 5.8 3.1 110 290
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect .18 .18 1.3 9.5 .012 0      - - true 4.0  2.2  70   270 true 200   190   3900 770
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect .14 .14 1.7 9.1 .012 .32   - - true 3.9  2.2  69   270 true 230   220   4200 740
loops/string_true-unreach-call_true-termination.i true 2 wit inspect .18 .18 2.0 9.3 .012 0      - - true 6.4  3.5  110   290 true 10   5.6 190 350
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect .15 .14 1.7 10   .012 0      - - timeout 900    900    10000   3700 true 16   8.5 150 420
loops/sum03_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 880    930    12000   15000   .012 0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.3 3.3 110 310
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect .19 .31 2.2 18   .012 8.7    - - true 4.7  2.7  82   280 true 16   8.7 160 420
loops/sum_array_true-unreach-call.i unknown 0 wit inspect .17 .17 2.2 9.8 .012 0      - - error (invalid witness file) .52 .32 12   39 error (invalid witness file) 6.0 3.2 110 300
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect .19 .19 1.8 10   .012 0      - - true 4.1  2.3  88   270 true 8.2 4.5 77 320
loops/terminator_03_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   64   .012 0      - - error (invalid witness file) .60 .39 8.8 40 error (invalid witness file) 6.1 3.3 120 300
loops/trex01_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   2400   .012 0      - - error (invalid witness file) .60 .39 6.2 39 error (invalid witness file) 5.9 3.1 120 290
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect .17 .17 1.7 9.4 .012 0      - - true 5.4  3.0  58   280 true 9.9 5.2 140 340
loops/trex03_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9800   3800   .012 0      - - error (invalid witness file) .58 .38 8.0 40 error (invalid witness file) 5.8 3.1 120 290
loops/trex04_true-unreach-call_false-termination.i true 2 wit inspect .18 .18 2.0 9.4 .012 0      - - true 4.4  2.5  100   280 true 8.1 4.4 150 330
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect .16 .15 1.4 9.5 .012 0      - - out of memory 290    280    3800   7000 true 11   6.2 140 370
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true 2 wit inspect .52 .51 6.5 11   .016 0      - - true 8.4  4.5  120   350 true 10   5.6 110 340
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true 2 wit inspect .14 .14 1.5 9.2 .012 0      - - true 4.7  2.6  90   280 true 7.3 3.9 150 330
loops/vogal_true-unreach-call.i true 2 wit inspect .17 .17 1.7 9.4 .012 0      - - true 58    47    1300   970 true 200   150   4800 3100
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    910    14000   15000   .012 0      - - error (invalid witness file) .51 .33 11   43 error (invalid witness file) 6.1 3.2 110 300
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2 wit inspect .13 .13 1.3 9.3 .012 0      - - true 4.6  2.6  50   270 true 7.5 4.0 140 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 890    930    12000   15000   .012 .0041 - - error (invalid witness file) .64 .41 9.1 42 error (invalid witness file) 5.8 3.1 86 300
loop-acceleration/array_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect .15 .14 2.0 10   .012 0      timeout 97    88    2300   2400 timeout 97   75   2100 4700 - -
loop-acceleration/array_false-unreach-call2_true-termination.i false(unreach-call) 0 wit inspect .16 .16 1.6 14   .012 0      out of memory 49    39    1400   7000 timeout 96   67   1800 6100 - -
loop-acceleration/array_false-unreach-call3_true-termination.i false(unreach-call) 0 wit inspect 2.0  2.0  32   12   .012 0      timeout 96    84    1700   2700 true 49   33   890 3000 - -
loop-acceleration/const_false-unreach-call1.i false(unreach-call) 1 wit inspect .17 .17 1.4 11   .012 0      false(unreach-call) 29    16    400   1000 timeout 96   76   2100 4600 - -
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) 1 wit inspect .16 .16 1.9 9.9 .012 0      false(unreach-call) 51    40    1300   910 true 8.1 4.3 150 330 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i false(unreach-call) 0 wit inspect .13 .13 1.5 9.3 .012 0      timeout 98    85    1600   2200 true 9.0 4.8 97 330 - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .17 .16 1.4 9.4 .012 0      false(unreach-call) 3.5  2.0  70   280 false(unreach-call) 7.1 3.8 130 320 - -
loop-acceleration/nested_false-unreach-call1.i false(unreach-call) 0 wit inspect .16 .16 1.5 9.4 .012 0      timeout 98    85    1300   2100 true 7.1 3.8 140 320 - -
loop-acceleration/phases_false-unreach-call1.i out of memory 0 wit inspect 230    250    3500   15000   .012 8800      error (invalid witness file) .64 .41 8.4 40 error (invalid witness file) 7.2 3.8 73 290 - -
loop-acceleration/phases_false-unreach-call2.i false(unreach-call) 1 wit inspect .15 .15 1.5 9.4 .012 0      false(unreach-call) 4.4  2.4  64   280 false(unreach-call) 7.6 4.0 100 330 - -
loop-acceleration/simple_false-unreach-call1.i false(unreach-call) 0 wit inspect .14 .13 1.6 9.3 .012 0      timeout 96    86    2100   2000 true 7.7 4.1 110 330 - -
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .16 .16 1.7 9.4 .012 0      false(unreach-call) 4.6  2.6  63   270 false(unreach-call) 7.7 4.1 130 330 - -
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) 1 wit inspect .17 .17 1.3 9.3 .012 0      false(unreach-call) 4.4  2.5  50   270 false(unreach-call) 7.7 4.2 110 310 - -
loop-acceleration/simple_false-unreach-call4.i false(unreach-call) 0 wit inspect .13 .13 1.6 9.4 .012 0      timeout 97    85    1900   2000 true 7.9 4.3 140 320 - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) 1 wit inspect .16 .16 1.5 9.3 .012 0      false(unreach-call) 4.6  2.6  57   270 true 8.5 4.5 130 330 - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) 1 wit inspect .13 .13 1.5 9.2 .012 0      false(unreach-call) 3.7  2.1  61   280 true 8.3 4.5 130 320 - -
loop-acceleration/array_true-unreach-call1_true-termination.i true 2 wit inspect .13 .13 1.6 9.3 .012 0      - - true 4.3  2.4  64   280 timeout 960   790   17000 4000
loop-acceleration/array_true-unreach-call2_true-termination.i true 1 wit inspect .15 .15 1.6 10   .012 0      - - out of memory 280    280    6200   7000 timeout 960   800   18000 4200
loop-acceleration/array_true-unreach-call3_true-termination.i true 1 wit inspect 6.6  6.6  79   13   .012 0      - - timeout 900    890    13000   6100 timeout 960   850   20000 3000
loop-acceleration/array_true-unreach-call4_true-termination.i true 1 wit inspect 6.6  6.6  87   13   .012 0      - - out of memory 290    280    6400   7000 timeout 960   830   17000 2700
loop-acceleration/const_true-unreach-call1.i true 2 wit inspect .14 .14 1.7 9.4 .012 0      - - true 4.2  2.3  66   270 timeout 960   810   22000 2700
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect .16 .16 1.9 9.8 .012 0      - - true 18    14    330   530 true 660   560   15000 1600
loop-acceleration/diamond_true-unreach-call2.i true 2 wit inspect .20 .31 2.4 17   .012 7.7    - - true 7.6  4.3  110   330 true 39   27   940 690
loop-acceleration/functions_true-unreach-call1_true-termination.i true 1 wit inspect .13 .13 2.0 9.5 .012 0      - - out of memory 380    370    6700   7000 timeout 960   800   18000 3300
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect .14 .14 1.5 9.1 .012 0      - - out of memory 380    370    6400   7000 true 7.7 4.1 160 310
loop-acceleration/nested_true-unreach-call1.i true 2 wit inspect .16 .15 1.4 9.4 .012 0      - - true 5.5  3.1  110   290 timeout 960   830   22000 4700
loop-acceleration/overflow_true-unreach-call1.i true 1 wit inspect .15 .15 1.4 9.5 .012 0      - - out of memory 440    430    8100   7000 timeout 960   810   21000 2400
loop-acceleration/phases_true-unreach-call1.i true 1 wit inspect 210    230    2900   15000   .012 .0041 - - out of memory 410    410    8900   7000 timeout 960   810   19000 2500
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout (timeout) 0 wit inspect 900    900    8800   11000   .012 0      - - error (invalid witness file) .56 .35 7.1 40 error (invalid witness file) 7.6 4.0 61 300
loop-acceleration/simple_true-unreach-call1.i true 1 wit inspect .13 .13 1.5 9.5 .012 0      - - out of memory 390    380    6500   7000 timeout 960   810   13000 2900
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect .13 .13 1.7 9.3 .012 0      - - true 4.7  2.6  54   270 true 9.1 4.9 83 310
loop-acceleration/simple_true-unreach-call3_true-termination.i true 1 wit inspect .17 .17 1.8 9.3 .012 0      - - timeout 910    900    13000   6200 timeout 960   910   16000 850
loop-acceleration/simple_true-unreach-call4.i true 2 wit inspect .14 .13 1.5 9.6 .012 0      - - true 3.7  2.1  56   270 true 9.2 4.9 110 310
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect .16 .15 1.4 9.2 .012 0      - - true 7.6  5.4  110   400 true 64   57   1400 410
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect .14 .14 1.4 9.5 .012 0      - - true 4.5  2.5  62   270 true 12   6.4 160 380
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .20 .19 1.8 10   .012 0      timeout 96    79    2700   3700 true 9.4 5.1 140 330 - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    11000   2200   .012 0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.3 3.4 96 290
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    11000   1200   .012 0      - - error (invalid witness file) .48 .30 9.0 39 error (invalid witness file) 6.0 3.2 110 290
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i timeout (timeout) 0 wit inspect 900    900    6700   1700   .012 0      - - error (invalid witness file) .52 .32 8.7 41 error (invalid witness file) 7.1 3.8 75 300
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    10000   3500   .012 0      - - error (invalid witness file) .52 .34 5.0 40 error (invalid witness file) 5.9 3.1 110 300
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    8200   4400   .012 0      - - error (invalid witness file) .59 .38 7.8 40 error (invalid witness file) 6.1 3.2 99 300
loop-invgen/down_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    11000   730   .012 0      - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.6 3.4 130 310
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9400   3400   .012 0      - - error (invalid witness file) .63 .41 7.8 40 error (invalid witness file) 7.2 3.8 99 310
loop-invgen/half_2_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    10000   2000   .012 0      - - error (invalid witness file) .53 .33 9.1 39 error (invalid witness file) 5.9 3.1 120 300
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    8300   1600   .012 0      - - error (invalid witness file) .68 .43 6.7 42 error (invalid witness file) 7.1 3.7 96 310
loop-invgen/id_build_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9200   1900   .012 0      - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.7 3.5 84 290
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect .16 .15 1.9 10   .012 0      - - true 6.0  3.3  64   290 true 12   6.5 160 380
loop-invgen/nest-if3_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   77   .012 0      - - error (invalid witness file) .64 .41 7.5 39 error (invalid witness file) 6.9 3.6 130 310
loop-invgen/nested6_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9000   4700   .012 0      - - error (invalid witness file) .59 .37 12   43 error (invalid witness file) 6.4 3.4 92 290
loop-invgen/nested9_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   1100   .012 0      - - error (invalid witness file) .51 .33 8.8 40 error (invalid witness file) 5.8 3.1 130 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    11000   1000   .012 .20   - - error (invalid witness file) .67 .44 8.5 41 error (invalid witness file) 7.2 3.8 73 300
loop-invgen/seq_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    10000   1900   .012 0      - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.9 3.2 98 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    11000   120   .012 0      - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 6.5 3.4 94 300
loop-invgen/up_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    9200   2000   .012 0      - - error (invalid witness file) .51 .34 7.6 40 error (invalid witness file) 6.2 3.2 110 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true 2 wit inspect 6.2  6.2  83   13   .012 0      - - out of memory 430    420    6400   7000 true 11   6.0 96 350
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    900    11000   50   .012 0      - - error (invalid witness file) .55 .36 8.1 42 error (invalid witness file) 7.5 3.9 72 290
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect .13 .13 1.6 9.4 .012 0      - - true 5.0  2.8  74   280 true 11   6.1 120 370
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .17 .17 1.5 9.3 .012 0      - - out of memory 330    320    8400   7000 true 10   5.6 180 360
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true 2 wit inspect .15 .15 1.6 9.4 .012 0      - - true 5.4  3.0  74   280 true 11   6.1 120 330
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 7.1  7.1  98   360   .012 0      - - true 4.1  2.3  79   280 true 8.2 4.3 170 330
loop-lit/ddlm2013_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    10000   74   .012 0      - - error (invalid witness file) .49 .33 12   39 error (invalid witness file) 6.3 3.3 100 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 2 wit inspect .16 .15 1.5 9.4 .012 0      - - true 60    55    1700   770 true 100   65   2300 1600
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    900    9000   1700   .012 0      - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.4 3.4 130 320
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 2 wit inspect .15 .15 1.7 9.3 .012 0      - - true 62    54    930   1100 true 100   61   1600 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout (timeout) 0 wit inspect 900    900    11000   60   .012 0      - - error (invalid witness file) .56 .35 13   41 error (invalid witness file) 6.6 3.5 100 300
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect .17 .17 1.5 9.3 .012 0      - - out of memory 370    370    7000   7000 true 12   6.8 140 370
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect .16 .16 1.7 9.8 .012 .32   - - out of memory 330    320    7700   7000 true 12   6.8 200 450
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect .15 .15 1.7 9.9 .012 0      - - out of memory 350    340    4300   7000 true 15   8.2 200 450
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i unknown 0 wit inspect 140    140    1800   330   .012 0      - - error (invalid witness file) .57 .36 9.8 39 error (invalid witness file) 7.7 4.0 61 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .16 .15 1.8 9.4 .012 0      false(unreach-call) 4.0  2.2  52   270 false(unreach-call) 8.5 4.5 130 320 - -
loop-new/count_by_1_true-unreach-call_true-termination.i true 2 wit inspect .15 .15 1.3 9.4 .012 0      - - true 3.8  2.1  53   270 timeout 960   790   18000 4100
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true 2 wit inspect 2.9  2.9  48   370   .012 0      - - true 3.9  2.2  74   280 true 13   6.8 140 350
loop-new/count_by_2_true-unreach-call_true-termination.i true 1 wit inspect .16 .16 1.5 9.2 .012 0      - - out of memory 310    300    4600   7000 timeout 960   800   21000 4400
loop-new/count_by_k_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   11   .012 0      - - error (invalid witness file) .61 .38 8.7 40 error (invalid witness file) 6.3 3.3 120 290
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    12000   110   .012 0      - - error (invalid witness file) .48 .32 8.2 40 error (invalid witness file) 6.4 3.4 96 300
loop-new/gauss_sum_true-unreach-call_true-termination.i true 1 wit inspect .23 .22 2.1 10   .012 .32   - - timeout 900    900    12000   5200 timeout 960   820   16000 3000
loop-new/half_true-unreach-call_true-termination.i timeout (timeout) 0 wit inspect 900    900    8800   2200   .012 0      - - error (invalid witness file) .51 .33 8.4 40 error (invalid witness file) 7.3 3.9 83 300
loop-new/nested_true-unreach-call_true-termination.i true 2 wit inspect .16 .16 1.7 11   .012 0      - - timeout 900    890    16000   1700 true 42   24   750 830
loop-industry-pattern/aiob_1_true-unreach-call.c true 2 wit inspect .17 .17 2.0 9.9 .029 0      - - true 27    21    540   610 error 11   5.6 200 310
loop-industry-pattern/aiob_2_true-unreach-call.c true 2 wit inspect .19 .19 1.9 9.9 .029 0      - - true 33    26    450   590 error 12   6.3 120 310
loop-industry-pattern/aiob_3_true-unreach-call.c true 2 wit inspect .19 .19 2.1 10   .029 0      - - true 31    25    350   590 error 11   5.7 200 310
loop-industry-pattern/aiob_4_true-unreach-call.c true 2 wit inspect .17 .17 2.0 10   .029 0      - - true 26    20    320   560 error 13   6.9 140 310
loop-industry-pattern/mod3_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    12000   89   .012 0      - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 6.0 3.2 99 300
loop-industry-pattern/nested_true-unreach-call.c error 0 wit inspect .50 .49 6.9 78   .012 0      - - error (invalid witness file) .49 .32 9.5 39 error (invalid witness file) 5.2 2.8 93 280
loop-industry-pattern/ofuf_1_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    11000   150   .041 0      - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.7 3.5 80 290
loop-industry-pattern/ofuf_2_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    11000   160   .041 0      - - error (invalid witness file) .66 .42 8.1 44 error (invalid witness file) 6.6 3.5 99 300
loop-industry-pattern/ofuf_3_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    12000   160   .041 8.5    - - error (invalid witness file) .57 .37 9.0 40 error (invalid witness file) 7.1 3.7 73 300
loop-industry-pattern/ofuf_4_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    12000   160   .041 0      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.5 3.4 110 310
loop-industry-pattern/ofuf_5_true-unreach-call.c timeout (timeout) 0 wit inspect 900    900    9500   160   .041 0      - - error (invalid witness file) .64 .41 8.2 40 error (invalid witness file) 6.0 3.2 100 290
loops/heavy_true-unreach-call.c true 1 wit inspect .40 .40 4.7 30   .012 0      - - timeout 900    890    13000   4100 timeout 960   890   12000 6500
loops/compact_false-unreach-call.c timeout (timeout) 0 wit inspect 900    900    11000   60   .012 0      error (invalid witness file) .59 .37 8.5 40 error (invalid witness file) 6.2 3.3 100 300 - -
loops/heavy_false-unreach-call.c false(unreach-call) 0 wit inspect .37 .36 4.7 29   .012 0      timeout 98    82    2100   2100 timeout 97   78   2200 5600 - -
../../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 136 39000   40000   470000 170000 2.4  8900    156 1300 1100 28000 44000   156 890 580 16000 46000   156 13000 13000 220000 170000   156 18000 15000 340000 99000  
    correct results 76 123 29   29   360 1500 1.1  18    28 300 210 6700 11000   26 410 260 7000 21000   37 5600 5400 92000 81000   39 5900 4900 120000 39000  
        correct true 47 94 24   24   310 1200 .65 17    0 0 0 0 0   8 0 0 0 0   37 5600 5400 92000 81000   39 5900 4900 120000 39000  
        correct false 29 29 4.9 4.8 50 280 .41 .90 28 300 210 6700 11000   18 410 260 7000 21000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 26 13 230   250   3200 15000 .32 .32 2 1000 880 21000 33000   10 410 290 8100 22000   0 7700 7500 120000 83000   0 12000 10000 210000 47000  
        correct-unconfirmed true 13 13 230   240   3100 15000 .16 .32 2 0 0 0 0   10 0 0 0 0   0 7700 7500 120000 83000   0 12000 10000 210000 47000  
        correct-unconfirmed false 13 0 4.4 4.3 59 150 .16 0    0 1000 880 21000 33000   0 410 290 8100 22000   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) 136
Run set sv-comp17.ReachSafety-Loops