Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
loops/array_false-unreach-call_true-termination.i 1 .19 .19 1.9 23 1.7  .094  4.2  2.4  64   280 7.5 4.0 110 330
loops/bubble_sort_false-unreach-call.i 0 230    230    1900   15000 .84 0      .59 .39 10   44 5.8 3.1 100 300
loops/count_up_down_false-unreach-call_true-termination.i 1 1.2  1.2  13   130 1.7  0      4.5  2.5  52   270 6.7 3.6 91 310
loops/eureka_01_false-unreach-call.i 0 900    900    6800   7800 .84 0      .47 .31 9.3 39 5.8 3.1 110 300
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 890    890    9200   4300 1.7  0      17    9.3  280   740 23   12   240 1100
loops/insertion_sort_false-unreach-call_true-termination.i 0 900    900    7800   3000 .84 0      .66 .42 7.7 39 5.8 3.1 91 290
loops/invert_string_false-unreach-call_true-termination.i 1 890    890    13000   1700 1.7  0      3.9  2.2  81   270 11   6.2 140 370
loops/linear_search_false-unreach-call.i 0 1.3  1.3  17   85 1.7  .094  5.5  3.0  130   280 97   83   1100 700
loops/ludcmp_false-unreach-call.i 0 9.7  9.4  120   15000 .84 0      .53 .34 11   43 5.8 3.1 110 290
loops/matrix_false-unreach-call_true-termination.i 0 900    900    7100   6500 .84 0      .53 .33 11   40 6.2 3.2 97 300
loops/n.c24_false-unreach-call.i 0 80    80    760   15000 .84 0      .61 .39 9.1 40 5.6 3.0 91 300
loops/nec11_false-unreach-call_false-termination.i 1 1.8  1.8  20   140 1.7  0      4.5  2.5  46   280 6.9 3.7 120 330
loops/nec20_false-unreach-call_true-termination.i 1 1.0  1.0  11   130 1.9  .094  31    17    450   1000 97   76   1600 4900
loops/s3_false-unreach-call.i 0 350    350    3900   15000 1.7  0      15    8.0  180   480 10   5.5 200 350
loops/string_false-unreach-call_true-termination.i 1 890    900    9100   1000 1.7  0      6.9  3.8  77   300 25   13   260 490
loops/sum01_bug02_false-unreach-call_true-termination.i 1 .92 .92 10   130 1.7  0      5.6  3.0  120   290 15   8.2 150 450
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 0 1.8  1.8  27   140 1.9  0      23    12    420   670 97   78   1700 5000
loops/sum01_false-unreach-call_true-termination.i 1 .63 .63 8.0 81 1.7  0      7.3  3.9  73   290 16   9.0 300 490
loops/sum03_false-unreach-call_true-termination.i 1 .22 .22 2.8 23 1.7  0      4.9  2.7  76   290 7.0 3.7 110 320
loops/sum04_false-unreach-call_true-termination.i 1 .17 .17 1.3 23 1.7  .094  4.1  2.3  85   280 6.7 3.6 110 310
loops/sum_array_false-unreach-call.i 1 52    52    720   2100 1.7  0      4.0  2.2  70   260 8.7 4.7 170 350
loops/terminator_01_false-unreach-call_true-termination.i 1 .60 .60 6.7 81 1.7  0      6.0  3.3  49   290 28   15   410 1500
loops/terminator_02_false-unreach-call_true-termination.i 1 16    16    170   920 1.7  0      3.8  2.2  59   270 7.0 3.7 100 320
loops/terminator_03_false-unreach-call_true-termination.i 1 13    13    150   160 1.8  .094  3.8  2.1  58   290 7.2 3.8 90 320
loops/trex01_false-unreach-call_true-termination.i 1 42    42    490   1800 1.8  .094  5.3  2.9  52   280 7.3 3.9 120 320
loops/trex02_false-unreach-call_true-termination.i 0 15    15    200   890 2.5  0      47    26    520   1300 97   66   1300 6800
loops/trex03_false-unreach-call_true-termination.i 1 9.7  9.7  110   510 1.7  .094  4.6  2.6  62   280 7.5 3.9 86 320
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 10    10    110   1200 1.7  0      4.3  2.4  55   280 10   5.7 170 350
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 0 900    900    10000   1800 .84 0      .56 .35 10   40 5.8 3.1 90 290
loops/vogal_false-unreach-call.i 0 140    140    1400   15000 1.7  0      92    79    1600   710 29   16   340 660
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 .22 .22 2.1 23 1.7  .094  4.0  2.3  72   280 6.6 3.6 76 320
loops/array_true-unreach-call_true-termination.i 2 .19 .19 1.8 23 1.7  0      5.5  3.1  61   290 11   5.9 120 350
loops/bubble_sort_true-unreach-call.i 0 900    900    5500   7000 .84 0      .54 .34 11   43 5.7 3.0 77 300
loops/count_up_down_true-unreach-call_true-termination.i -16 1.3  1.3  18   140 2.0  0      920    890    16000   4300 440   380   8800 7000
loops/eureka_01_true-unreach-call.i 1 20    20    270   3000 1.8  0      700    670    11000   7000 960   840   15000 4600
loops/eureka_05_true-unreach-call_true-termination.i 2 7.9  7.9  100   1100 1.7  .0041 440    420    10000   5100 36   21   550 750
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 .23 .23 2.5 31 1.9  0      7.0  3.8  86   300 8.6 4.5 140 340
loops/for_infinite_loop_2_true-unreach-call_false-termination.i -16 .19 .19 2.1 23 1.7  .094  910    890    13000   4200 10   5.3 93 340
loops/insertion_sort_true-unreach-call_true-termination.i 0 900    900    8200   6000 .84 0      .58 .38 6.8 40 7.1 3.8 56 290
loops/invert_string_true-unreach-call_true-termination.i 2 .18 .18 2.1 24 1.7  0      21    13    350   560 41   27   430 780
loops/linear_sea.ch_true-unreach-call.i 1 4.8  4.8  67   110 2.0  0      880    870    17000   7000 960   940   16000 830
loops/lu.cmp_true-unreach-call.i 0 9.8  9.5  110   15000 .84 0      .47 .31 9.6 39 5.3 2.8 75 290
loops/matrix_true-unreach-call_true-termination.i 2 26    26    330   1700 1.7  0      10    7.3  160   420 15   8.0 120 370
loops/n.c11_true-unreach-call_false-termination.i 2 2.2  2.2  25   220 2.3  0      280    270    4700   7000 11   6.0 180 390
loops/n.c40_true-unreach-call_true-termination.i 2 .16 .16 1.9 23 1.7  0      4.8  2.7  55   270 190   180   3500 1100
loops/nec40_true-unreach-call_true-termination.i 2 .14 .14 1.8 23 1.7  0      3.8  2.1  38   270 170   160   3300 780
loops/string_true-unreach-call_true-termination.i 2 12    12    140   500 3.4  0      15    8.4  240   490 13   6.7 160 420
loops/sum01_true-unreach-call_true-termination.i -16 1.4  1.4  17   130 1.9  0      910    890    18000   940 120   95   2000 4800
loops/sum03_true-unreach-call_false-termination.i 2 .27 .27 3.6 41 2.0  0      11    6.3  83   310 7.7 4.1 100 320
loops/sum04_true-unreach-call_true-termination.i 2 .13 .13 1.8 23 1.7  0      6.0  3.4  65   290 13   7.1 120 430
loops/sum_array_true-unreach-call.i 0 900    900    11000   1300 .84 0      .53 .33 9.8 41 6.3 3.3 130 300
loops/terminator_02_true-unreach-call_true-termination.i 2 35    35    370   4700 44    .0082 29    16    360   2700 22   12   400 1500
loops/terminator_03_true-unreach-call_true-termination.i -16 43    43    490   320 1.9  0      20    10    140   640 73   57   1500 4800
loops/trex01_true-unreach-call_true-termination.i -16 42    42    490   1800 1.8  .094  120    93    2600   1200 130   81   1800 7000
loops/trex02_true-unreach-call_true-termination.i -16 15    15    180   890 2.2  .094  40    23    530   1300 98   66   1200 7000
loops/trex03_true-unreach-call_true-termination.i -16 560    560    8000   890 2.2  0      57    35    600   1700 110   73   870 7000
loops/trex04_true-unreach-call_false-termination.i -16 22    22    250   300 1.9  0      27    16    280   770 69   53   1300 5000
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 11    11    140   1200 2.5  0      340    330    7100   7000 13   7.2 130 370
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 0 900    900    11000   1800 .84 0      .51 .33 7.4 41 6.9 3.6 72 300
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 2.0  2.0  21   290 2.5  .0082 12    7.0  110   330 9.6 5.1 110 340
loops/vogal_true-unreach-call.i 2 290    290    3300   14000 4.7  0      71    54    1000   910 200   160   2800 3100
loops/while_infinite_loop_1_true-unreach-call_false-termination.i -16 .19 .19 1.7 23 1.7  0      4.4  2.5  47   270 6.2 3.4 76 310
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 .19 .19 1.9 23 1.8  0      7.6  4.1  82   310 7.6 4.0 120 330
loops/while_infinite_loop_3_true-unreach-call_false-termination.i -16 .20 .20 2.2 23 1.7  .094  3.8  2.1  73   280 7.0 3.7 150 310
loop-acceleration/array_false-unreach-call1_true-termination.i 0 140    140    1900   160 1.8  .094  97    89    2300   2400 97   79   1500 4600
loop-acceleration/array_false-unreach-call2_true-termination.i 0 140    140    2000   180 1.9  0      96    86    3100   1200 96   77   1200 4500
loop-acceleration/array_false-unreach-call3_true-termination.i 0 150    150    2000   230 1.9  0      98    81    1700   2900 97   76   2300 5000
loop-acceleration/const_false-unreach-call1.i 1 .14 .14 1.7 23 1.7  0      28    15    480   1000 7.5 4.0 140 310
loop-acceleration/diamond_false-unreach-call1.i 0 1.3  1.3  17   130 1.7  .094  4.8  2.6  110   310 78   47   930 7000
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 .16 .16 1.8 23 1.7  0      98    82    1800   1800 6.8 3.7 110 320
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 2.9  2.9  34   170 2.0  0      37    23    860   2400 97   69   1200 5500
loop-acceleration/nested_false-unreach-call1.i 0 3.3  3.3  33   450 1.7  0      98    83    1900   1900 7.0 3.7 110 320
loop-acceleration/phases_false-unreach-call1.i 0 .15 .15 1.8 23 1.7  .10   98    83    1800   2000 6.8 3.6 110 300
loop-acceleration/phases_false-unreach-call2.i 1 56    56    640   3200 1.7  0      3.6  2.0  45   270 7.3 3.9 120 320
loop-acceleration/simple_false-unreach-call1.i 0 .14 .14 1.8 23 1.7  0      96    82    1300   1900 6.2 3.4 85 310
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 2.6  2.6  27   120 1.8  .094  98    82    2400   1300 66   52   1500 4500
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 1.3  1.3  14   83 1.8  0      28    15    340   950 69   54   1300 4800
loop-acceleration/simple_false-unreach-call4.i 0 .14 .14 1.7 23 1.7  .094  97    86    2200   2200 6.6 3.6 96 310
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 .14 .14 1.5 23 1.7  .094  4.7  2.6  44   270 7.3 3.8 120 320
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 .14 .14 1.5 23 1.7  .094  4.9  2.7  52   270 7.5 4.0 94 310
loop-acceleration/array_true-unreach-call1_true-termination.i -16 140    140    1800   160 1.8  0      44    38    950   1300 270   230   3800 7000
loop-acceleration/array_true-unreach-call2_true-termination.i -16 140    140    1900   180 1.9  0      260    250    5700   7000 510   470   7800 7000
loop-acceleration/array_true-unreach-call3_true-termination.i 1 .83 .83 9.4 130 2.2  0      910    890    18000   5000 960   850   21000 2700
loop-acceleration/array_true-unreach-call4_true-termination.i 1 .82 .82 10   130 2.2  0      340    320    6900   7000 960   840   12000 2800
loop-acceleration/const_true-unreach-call1.i 2 .19 .19 2.2 30 1.9  0      9.6  5.2  130   330 960   810   18000 2500
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 1.4  1.4  17   180 2.3  0      18    14    360   530 600   510   6800 1500
loop-acceleration/diamond_true-unreach-call2.i 2 96    96    1000   2600 6.7  0      15    8.3  150   620 42   28   430 890
loop-acceleration/functions_true-unreach-call1_true-termination.i 1 .26 .26 2.3 39 2.0  0      340    330    8600   7000 960   800   13000 3500
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 1.1  1.1  15   160 2.2  0      380    370    6700   7000 12   6.2 140 320
loop-acceleration/nested_true-unreach-call1.i 2 3.6  3.6  35   550 2.8  0      44    37    730   650 960   830   11000 4700
loop-acceleration/overflow_true-unreach-call1.i 1 .16 .16 2.1 23 1.8  0      430    420    8200   7000 960   810   12000 2700
loop-acceleration/phases_true-unreach-call1.i -16 .15 .15 1.9 23 1.7  0      920    890    15000   4200 6.3 3.4 75 300
loop-acceleration/phases_true-unreach-call2_false-termination.i -16 57    57    540   3200 1.8  .094  16    8.2  160   570 51   37   1100 3600
loop-acceleration/simple_true-unreach-call1.i 1 .18 .18 1.9 23 1.8  0      430    420    7100   7000 960   810   17000 2500
loop-acceleration/simple_true-unreach-call2_true-termination.i -16 2.6  2.6  33   120 1.8  .094  910    890    15000   2400 70   54   760 4800
loop-acceleration/simple_true-unreach-call3_true-termination.i 1 .67 .67 7.4 94 2.0  0      910    900    18000   6200 960   920   16000 750
loop-acceleration/simple_true-unreach-call4.i 2 .19 .19 2.1 23 1.8  0      10    5.4  120   310 7.9 4.3 120 330
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 .16 .16 1.4 23 1.7  0      8.5  6.0  97   400 55   49   950 390
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 .14 .14 1.6 24 1.7  .30   4.8  2.6  68   280 11   5.8 130 380
loop-invgen/id_trans_false-unreach-call_true-termination.i 0 24    24    300   2300 1.8  0      17    8.8  330   600 7.5 3.9 120 320
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 2 900    900    10000   2400 1.7  0      900    890    17000   2200 11   6.1 130 380
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 9.3  9.3  120   870 2.4  .0082 500    490    8300   7000 12   6.2 160 390
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 34    33    380   15000 .84 0      .48 .31 8.4 39 6.5 3.4 63 290
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900    900    13000   650 .84 0      .71 .45 6.8 41 5.2 2.8 72 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 140    140    1500   15000 1.7  0      28    14    300   820 29   16   420 3700
loop-invgen/down_true-unreach-call_true-termination.i 1 18    18    250   1000 3.0  0      260    250    3800   7000 960   790   13000 4700
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 1 13    13    130   1400 4.0  0      540    480    8800   7000 960   800   14000 4700
loop-invgen/half_2_true-unreach-call_true-termination.i 1 31    31    410   1000 3.0  0      910    890    10000   6800 960   820   12000 2500
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 39    38    370   15000 .84 0      .54 .34 11   43 7.1 3.7 47 300
loop-invgen/id_build_true-unreach-call_true-termination.i 0 70    70    970   15000 1.7  0      35    29    760   720 9.2 4.9 140 340
loop-invgen/large_const_true-unreach-call_true-termination.i 2 31    31    410   2000 4.4  0      200    190    3100   980 12   6.6 140 440
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 900    900    8700   11000 .84 0      .50 .32 12   41 5.7 3.1 95 300
loop-invgen/nested6_true-unreach-call_true-termination.i 0 52    52    540   15000 .84 0      .51 .33 12   40 6.5 3.5 62 300
loop-invgen/nested9_true-unreach-call_true-termination.i 0 32    31    310   15000 .84 0      .49 .32 9.2 40 5.5 2.9 62 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 2 38    38    460   3500 3.6  0      460    450    7300   7000 22   12   160 650
loop-invgen/seq_true-unreach-call_true-termination.i 1 92    92    1000   1200 3.6  0      660    610    12000   7000 960   790   12000 3200
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 900    900    10000   2800 .84 0      .67 .42 7.2 40 6.1 3.2 100 300
loop-invgen/up_true-unreach-call_true-termination.i 1 17    17    210   1000 3.0  0      320    310    4300   7000 960   790   19000 4200
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 2 2.5  2.5  29   230 2.3  0      500    490    8500   7000 13   7.0 120 360
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i -16 130    130    1600   880 2.0  .094  910    890    17000   1500 130   71   1100 7000
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 .14 .14 1.6 23 1.7  0      5.0  2.8  68   280 9.6 5.2 110 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i -16 3.0  3.0  38   220 2.2  0      28    15    310   1100 100   66   940 7000
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 6.8  6.8  63   990 1.7  0      8.8  4.7  88   300 9.0 4.8 170 350
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 5.0  5.0  62   510 2.3  0      17    11    190   420 8.1 4.3 85 320
loop-lit/ddlm2013_true-unreach-call.i 1 4.7  4.7  62   440 3.1  0      330    320    6100   7000 960   840   12000 3200
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 .15 .14 2.0 23 1.7  0      72    64    1600   790 110   71   1200 1500
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 2 8.1  8.1  94   380 2.5  0      900    890    17000   3700 11   6.0 93 380
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 .18 .18 1.5 23 1.7  0      63    55    1200   1100 84   50   800 1200
loop-lit/gsv2008_true-unreach-call_true-termination.c.i -16 7.3  7.3  79   220 2.0  0      30    16    470   990 390   340   8100 6700
loop-lit/hhk2008_true-unreach-call_true-termination.c.i -16 2.7  2.7  33   150 2.0  .094  19    9.8  170   750 410   360   11000 7000
loop-lit/jm2006_true-unreach-call_true-termination.c.i -16 1.4  1.4  16   140 2.0  0      920    890    14000   4200 760   700   8800 7000
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i -16 2.0  2.0  27   210 2.2  0      100    77    1500   1900 130   91   1700 7000
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 900    900    11000   880 .84 0      .64 .41 7.3 42 5.9 3.1 79 280
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 100    100    1200   1900 1.7  .49   7.3  4.0  90   310 12   6.5 140 380
loop-new/count_by_1_true-unreach-call_true-termination.i -16 .16 .16 1.5 23 1.7  0      910    890    18000   2900 6.0 3.3 81 300
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 .23 .23 3.0 30 1.9  0      11    5.7  120   310 11   6.0 170 370
loop-new/count_by_2_true-unreach-call_true-termination.i -16 .15 .15 1.6 23 1.7  0      920    890    15000   3100 7.3 3.8 82 320
loop-new/count_by_k_true-unreach-call_true-termination.i -16 5.6  5.6  79   160 1.9  0      910    890    16000   2000 86   54   790 7000
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 110    110    1400   15000 1.7  0      900    890    17000   1500 960   790   13000 4800
loop-new/gauss_sum_true-unreach-call_true-termination.i -16 1.8  1.8  24   140 1.9  0      16    8.3  160   580 250   220   3400 7000
loop-new/half_true-unreach-call_true-termination.i -16 1.3  1.3  14   110 1.8  0      910    890    18000   3000 55   38   680 3100
loop-new/nested_true-unreach-call_true-termination.i 0 890    890    10000   15000 1.7  0      910    890    16000   2400 42   23   700 1500
loop-industry-pattern/aiob_1_true-unreach-call.c 2 .21 .21 2.5 25 1.7  0      29    23    450   590 10   5.5 130 310
loop-industry-pattern/aiob_2_true-unreach-call.c 2 .25 .25 2.2 25 1.7  0      32    26    550   590 11   5.7 120 320
loop-industry-pattern/aiob_3_true-unreach-call.c 2 .25 .25 2.3 25 1.7  0      27    21    560   580 10   5.6 140 300
loop-industry-pattern/aiob_4_true-unreach-call.c 2 .22 .22 2.6 25 1.7  0      26    20    380   550 10   5.5 140 300
loop-industry-pattern/mod3_true-unreach-call.c 0 900    900    13000   290 .84 0      .64 .40 7.5 39 6.2 3.4 60 290
loop-industry-pattern/nested_true-unreach-call.c 0 62    62    840   15000 .84 0      .54 .34 13   41 6.2 3.3 60 300
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 900    900    12000   1800 .84 0      .60 .40 8.2 40 6.1 3.2 85 310
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 900    900    12000   1800 .84 0      .62 .39 8.3 40 5.8 3.0 95 300
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 900    900    11000   1800 .84 0      .50 .31 10   39 6.6 3.5 120 310
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 900    900    11000   1700 .84 0      .66 .41 8.1 40 6.1 3.2 69 310
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 900    900    11000   1700 .84 0      .59 .38 7.2 39 6.8 3.5 60 320
loops/heavy_true-unreach-call.c 0 780    780    3100   15000 .84 0      .50 .32 8.5 39 5.7 3.1 52 310
loops/compact_false-unreach-call.c 0 900    900    11000   4400 .84 0      .52 .32 12   39 5.5 2.9 82 300
loops/heavy_false-unreach-call.c 0 320    320    3800   15000 .84 0      .66 .42 8.3 40 5.7 3.0 85 300
../../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 -295 27000 27000 300000 400000 320 3.0  156 1300 1000 26000 34000   156 1400 960 21000 69000   156 26000 25000 460000 220000   156 23000 19000 340000 220000  
    correct results 67 107 4500 4500 52000 59000 180 1.8  26 340 220 6300 13000   25 580 380 9100 30000   32 5500 5200 100000 70000   34 3800 3100 53000 31000  
        correct true 40 80 1500 1500 17000 38000 130 .33 4 0 0 0 0   6 0 0 0 0   32 5500 5200 100000 70000   34 3800 3100 53000 31000  
        correct false 27 27 3000 3000 35000 20000 47 1.4  22 340 220 6300 13000   19 580 380 9100 30000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 27 14 680 680 9000 14000 59 .48 5 870 730 18000 19000   6 700 530 11000 35000   0 8000 7700 140000 95000   0 13000 12000 200000 43000  
        correct-unconfirmed true 14 14 200 200 2500 9700 35 0    5 0 0 0 0   6 0 0 0 0   0 8000 7700 140000 95000   0 13000 12000 200000 43000  
        correct-unconfirmed false 13 0 470 470 6500 4600 24 .48 0 870 730 18000 19000   0 700 530 11000 35000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 26 -416 1200 1200 16000 10000 49 .75 0 0 0 0 0   0 0 0 0 0   14 11000 10000 190000 53000   13 4300 3600 68000 130000  
        incorrect true 0
        incorrect false 26 -416 1200 1200 16000 10000 49 .75 0 0 0 0 0   0 0 0 0 0   0 11000 10000 190000 53000   0 4300 3600 68000 130000  
score (156 tasks, max score: 261) -295
Run set sv-comp17.ReachSafety-Loops