Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; 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-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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 3.9 1.2  31 290 .0041 .020  4.9  2.7  79   290 9.9 5.4 180 350
loops/bubble_sort_false-unreach-call.i 0 440   410    5000 1900 7.8    8.8    18    9.2  230   540 20   11   320 500
loops/count_up_down_false-unreach-call_true-termination.i 1 6.1 1.6  41 410 .0041 0      3.7  2.1  72   270 7.4 4.0 160 310
loops/eureka_01_false-unreach-call.i 0 520   300    5200 4000 .35   0      97    88    1700   2300 13   6.8 220 320
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 12   2.8  78 710 .037  0      3.7  2.1  61   280 9.9 5.3 190 340
loops/insertion_sort_false-unreach-call_true-termination.i 0 55   12    390 2200 0      .012  .52 .34 12   41 5.9 3.1 120 300
loops/invert_string_false-unreach-call_true-termination.i 1 31   6.9  230 1700 .33   .0041 4.5  2.6  83   290 13   7.1 190 390
loops/linear_search_false-unreach-call.i 1 15   3.9  100 580 .0082 0      5.6  3.1  87   300 22   12   220 610
loops/ludcmp_false-unreach-call.i 0 960   920    12000 1900 .0082 0      97    83    1700   3300 46   37   680 7000
loops/matrix_false-unreach-call_true-termination.i 1 59   14    450 2200 .057  0      27    23    610   570 13   7.4 250 390
loops/n.c24_false-unreach-call.i 0 900   290    8100 5000 0      0      92    77    1800   2400 96   59   1000 2100
loops/nec11_false-unreach-call_false-termination.i 1 3.7 1.1  31 290 .0082 0      5.7  3.1  64   280 7.3 3.9 150 320
loops/nec20_false-unreach-call_true-termination.i 1 6.7 1.6  47 450 .0041 .0041 4.0  2.2  64   290 8.6 4.6 170 350
loops/s3_false-unreach-call.i 0 240   72    2000 15000 .63   6.1    .51 .35 9.4 40 6.3 3.3 120 300
loops/string_false-unreach-call_true-termination.i 1 7.1 1.7  56 360 .090  0      93    80    1100   2000 8.0 4.3 150 320
loops/sum01_bug02_false-unreach-call_true-termination.i 1 9.0 2.1  65 500 .0041 0      4.5  2.5  75   290 11   5.8 190 360
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 7.7 1.8  49 470 .0041 0      4.0  2.3  60   280 11   6.0 150 350
loops/sum01_false-unreach-call_true-termination.i 1 9.8 2.2  67 490 .0041 0      4.4  2.4  92   290 12   6.8 190 590
loops/sum03_false-unreach-call_true-termination.i 1 4.9 1.4  37 290 .016  0      6.7  3.7  150   310 29   17   420 640
loops/sum04_false-unreach-call_true-termination.i 1 4.0 1.3  29 290 .0082 8.8    5.5  3.1  74   290 13   7.4 190 390
loops/sum_array_false-unreach-call.i 1 32   6.3  180 1700 .23   .045  4.3  2.5  55   290 12   6.3 200 360
loops/terminator_01_false-unreach-call_true-termination.i 1 3.5 1.1  29 280 .0041 0      4.5  2.5  80   280 7.9 4.3 150 350
loops/terminator_02_false-unreach-call_true-termination.i 1 3.6 1.2  29 280 .0041 0      4.5  2.5  62   280 8.5 4.6 170 350
loops/terminator_03_false-unreach-call_true-termination.i 1 4.5 1.4  34 330 .029  .025  4.7  2.6  53   270 9.0 4.7 160 340
loops/trex01_false-unreach-call_true-termination.i 1 5.0 1.4  38 320 .016  0      3.7  2.1  60   270 7.0 3.7 140 310
loops/trex02_false-unreach-call_true-termination.i 1 3.5 1.1  30 280 .0041 0      4.7  2.6  95   280 7.7 4.1 140 340
loops/trex03_false-unreach-call_true-termination.i 1 4.5 1.3  31 330 .012  0      3.8  2.1  51   270 7.2 3.9 140 310
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 3.9 1.2  33 300 .0041 0      4.7  2.6  66   290 11   6.0 230 350
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 23   6.1  150 880 .0041 0      23    12    220   570 63   36   670 780
loops/vogal_false-unreach-call.i 0 98   28    880 2300 .012  0      92    82    1700   1500 97   74   1200 980
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 3.4 1.1  27 290 .0041 0      4.4  2.4  73   280 7.7 4.1 140 340
loops/array_true-unreach-call_true-termination.i 2 4.2 1.3  31 310 .0041 0      5.5  3.1  48   300 13   7.0 210 350
loops/bubble_sort_true-unreach-call.i 2 3.1 1.1  25 280 0      0      4.6  2.5  59   270 8.7 4.6 150 330
loops/count_up_down_true-unreach-call_true-termination.i 0 900   290    8200 8900 0      0      420    410    7500   7000 960   940   23000 810
loops/eureka_01_true-unreach-call.i 1 6.6 1.6  40 350 .0041 0      660    630    14000   7000 960   850   23000 4200
loops/eureka_05_true-unreach-call_true-termination.i 2 4.0 1.2  33 280 .0041 0      510    490    8900   5200 37   21   550 740
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 3.0 1.1  24 270 0      0      4.8  2.7  67   280 8.7 4.6 140 340
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 2.9 1.1  23 270 0      3.1    4.9  2.7  44   280 7.7 4.1 130 310
loops/insertion_sort_true-unreach-call_true-termination.i 0 910   300    6800 4200 0      0      900    890    21000   1400 7.6 4.1 150 320
loops/invert_string_true-unreach-call_true-termination.i 2 21   5.9  180 720 .045  .0041 28    21    620   610 8.0 4.3 130 310
loops/linear_sea.ch_true-unreach-call.i 0 900   440    10000 6900 0      0      750    740    15000   7000 960   930   21000 830
loops/lu.cmp_true-unreach-call.i 1 4.9 1.4  38 320 .0041 0      910    860    16000   5700 45   37   1300 7000
loops/matrix_true-unreach-call_true-termination.i 2 9.9 3.7  69 480 .0041 0      7.9  5.6  210   420 17   9.8 290 540
loops/n.c11_true-unreach-call_false-termination.i 2 2.9 1.0  23 270 .0041 0      260    260    5000   7000 10   5.6 130 380
loops/n.c40_true-unreach-call_true-termination.i 2 4.4 1.3  33 280 0      0      4.9  2.8  59   270 180   170   3500 710
loops/nec40_true-unreach-call_true-termination.i 2 4.1 1.3  30 280 0      0      5.3  2.9  56   280 180   170   3600 790
loops/string_true-unreach-call_true-termination.i 2 5.6 1.4  41 320 .0041 0      6.0  3.2  120   300 10   5.5 220 350
loops/sum01_true-unreach-call_true-termination.i 2 120   37    1000 3900 0      0      41    26    540   910 25   13   190 420
loops/sum03_true-unreach-call_false-termination.i 2 3.9 1.2  27 280 0      0      4.7  2.6  72   280 8.6 4.6 160 340
loops/sum04_true-unreach-call_true-termination.i 2 2.8 1.0  22 270 .0041 .79   5.9  3.3  61   280 11   6.2 200 410
loops/sum_array_true-unreach-call.i 0 210   63    1700 4400 0      0      .56 .35 10   41 5.6 3.0 98 290
loops/terminator_02_true-unreach-call_true-termination.i 2 3.4 1.1  31 280 .0041 0      5.6  3.1  53   280 8.2 4.5 160 340
loops/terminator_03_true-unreach-call_true-termination.i 2 3.8 1.1  28 300 .0041 .0041 5.1  2.8  69   270 8.6 4.6 170 340
loops/trex01_true-unreach-call_true-termination.i 2 5.9 1.5  44 320 0      0      6.2  3.4  85   290 450   370   11000 1800
loops/trex02_true-unreach-call_true-termination.i 2 3.5 1.2  26 280 .0041 .0041 5.7  3.1  62   280 9.4 5.1 150 340
loops/trex03_true-unreach-call_true-termination.i 2 4.1 1.2  28 280 .0041 0      4.9  2.7  100   290 8.3 4.5 170 350
loops/trex04_true-unreach-call_false-termination.i 2 3.8 1.2  27 280 .049  0      6.6  3.7  59   280 960   830   14000 2100
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 0 910   310    6900 9600 .0041 0      320    310    7700   7000 11   5.9 200 370
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 27   8.5  230 1200 .016  0      11    5.8  110   370 9.6 5.2 160 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 4.0 1.2  31 290 .0082 0      4.7  2.6  100   300 8.4 4.5 140 320
loops/vogal_true-unreach-call.i 0 61   14    460 1800 0      .012  .51 .33 11   39 5.8 3.1 110 310
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 2.9 1.0  22 280 .0041 0      4.9  2.7  47   270 7.4 3.9 140 330
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 2.7 .99 23 260 .0041 0      3.6  2.0  54   270 8.3 4.5 120 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 3.0 1.0  25 290 .0041 0      4.7  2.6  51   270 8.6 4.6 160 340
loop-acceleration/array_false-unreach-call1_true-termination.i 0 680   330    6300 7200 0      0      .47 .31 7.1 40 5.8 3.1 120 300
loop-acceleration/array_false-unreach-call2_true-termination.i 0 930   440    7300 14000 0      0      16    8.7  220   920 11   5.6 170 460
loop-acceleration/array_false-unreach-call3_true-termination.i 0 920   440    9600 4000 0      0      97    88    1100   3600 13   6.9 220 320
loop-acceleration/const_false-unreach-call1.i 0 920   370    8400 9300 0      0      93    84    1300   2600 15   7.9 220 320
loop-acceleration/diamond_false-unreach-call1.i 1 43   11    360 2000 .020  0      6.3  3.4  80   320 98   56   1200 6400
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 910   300    8000 7900 0      0      93    86    940   2000 97   67   880 1200
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 3.9 1.2  29 310 .0041 0      4.2  2.3  52   280 8.3 4.5 130 350
loop-acceleration/nested_false-unreach-call1.i 0 19   3.5  120 840 0      0      .48 .31 9.0 40 5.3 2.9 91 290
loop-acceleration/phases_false-unreach-call1.i 0 900   300    8600 5100 0      0      92    86    1400   1900 97   68   1800 1200
loop-acceleration/phases_false-unreach-call2.i 1 4.7 1.3  35 300 .0041 .85   3.5  2.0  26   270 7.3 3.9 140 320
loop-acceleration/simple_false-unreach-call1.i 0 90   26    650 2900 0      0      .51 .32 10   41 5.5 2.9 89 290
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 3.3 1.2  27 300 .0082 8.9    4.5  2.5  110   280 7.3 3.9 150 310
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 5.6 1.5  38 370 .0041 0      3.4  1.9  48   260 7.1 3.8 130 320
loop-acceleration/simple_false-unreach-call4.i 0 200   61    1900 3100 0      .012  .53 .33 10   39 6.6 3.4 140 320
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 3.7 1.2  28 280 .0082 0      5.5  3.1  52   290 13   6.8 240 370
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 3.6 1.2  27 280 .0082 .020  5.3  3.0  100   290 12   6.6 260 380
loop-acceleration/array_true-unreach-call1_true-termination.i 2 4.0 1.2  28 300 0      0      4.8  2.7  68   280 960   800   17000 4500
loop-acceleration/array_true-unreach-call2_true-termination.i 0 940   440    7100 14000 0      0      17    9.3  290   880 11   5.8 200 470
loop-acceleration/array_true-unreach-call3_true-termination.i 2 4.0 1.2  27 310 0      0      5.8  3.2  78   290 960   850   17000 2500
loop-acceleration/array_true-unreach-call4_true-termination.i 0 900   290    8000 5200 0      0      5.5  3.0  60   280 960   860   17000 3000
loop-acceleration/const_true-unreach-call1.i 2 3.2 1.1  28 270 0      0      3.9  2.2  77   280 960   810   16000 2400
loop-acceleration/diamond_true-unreach-call1_true-termination.i 2 34   8.5  280 1800 0      3.0    17    13    360   530 850   740   15000 1600
loop-acceleration/diamond_true-unreach-call2.i 2 9.1 2.0  62 720 0      3.1    7.7  4.4  160   330 41   28   570 660
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 44   11    320 1900 0      5.7    .63 .41 7.8 39 5.5 3.0 110 300
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 3.6 1.1  26 310 .0041 0      4.9  2.7  60   280 9.0 4.8 110 310
loop-acceleration/nested_true-unreach-call1.i 2 3.4 1.1  26 270 0      0      5.4  3.0  60   280 960   850   16000 4700
loop-acceleration/overflow_true-unreach-call1.i 0 900   290    7900 8700 0      0      410    400    9700   7000 960   810   18000 2400
loop-acceleration/phases_true-unreach-call1.i 0 900   300    7800 5000 0      0      450    440    9500   7000 960   830   17000 2000
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 4.7 1.4  36 310 0      0      5.9  3.4  80   330 9.3 5.1 190 340
loop-acceleration/simple_true-unreach-call1.i 0 910   300    7900 8600 0      0      460    440    10000   7000 960   820   19000 2000
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 3.3 1.1  26 280 .0041 0      3.9  2.2  63   280 7.4 4.0 140 310
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 900   290    8700 7300 0      0      880    870    21000   7000 960   920   19000 900
loop-acceleration/simple_true-unreach-call4.i 2 3.0 1.1  24 270 0      0      5.2  2.9  60   270 8.6 4.7 160 350
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 2.8 1.0  21 270 .0041 0      8.4  6.0  130   400 51   45   1400 430
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 2.8 1.0  24 270 .0041 0      4.8  2.7  56   270 10   5.6 180 380
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 9.5 2.4  74 530 .020  .020  4.1  2.3  70   290 7.8 4.1 160 320
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900   290    8200 5000 0      0      900    890    12000   2400 960   840   21000 3100
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 330   100    2900 5600 .0082 0      400    390    13000   7000 13   6.9 140 370
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 83   21    690 3000 0      .0041 .55 .35 11   40 7.3 3.8 140 330
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 2 66   16    440 3700 .025  0      900    890    17000   3200 13   7.4 220 500
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 910   290    6900 5600 0      0      900    890    16000   2400 8.4 4.5 140 320
loop-invgen/down_true-unreach-call_true-termination.i 0 910   300    9100 4200 0      3.1    900    890    25000   4800 960   800   15000 2100
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 930   320    9300 3900 0      0      900    890    15000   2700 9.7 5.2 92 340
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900   290    7400 5500 0      0      890    870    18000   7000 960   830   17000 1700
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 490   160    3600 4300 .078  .020  .56 .35 11   42 5.9 3.1 85 300
loop-invgen/id_build_true-unreach-call_true-termination.i 2 9.4 2.3  68 550 0      0      6.3  3.5  67   290 7.4 4.0 150 320
loop-invgen/large_const_true-unreach-call_true-termination.i 2 5.5 1.5  38 310 0      .79   6.9  3.8  75   300 8.1 4.4 120 330
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 23   4.3  160 870 0      .012  .53 .35 10   40 5.9 3.1 110 300
loop-invgen/nested6_true-unreach-call_true-termination.i 0 960   350    8800 4000 0      0      900    890    18000   4900 8.7 4.6 110 320
loop-invgen/nested9_true-unreach-call_true-termination.i 0 72   16    510 3400 0      .0041 .59 .37 13   42 6.1 3.3 100 300
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 880   280    6900 6500 0      0      .53 .34 12   41 5.7 3.0 130 300
loop-invgen/seq_true-unreach-call_true-termination.i 0 960   350    9300 3900 0      0      910    880    21000   6300 960   810   18000 1700
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 530   170    4600 3100 0      0      .59 .39 7.2 39 7.2 3.8 82 290
loop-invgen/up_true-unreach-call_true-termination.i 0 23   4.1  160 1100 0      .012  .62 .40 9.6 40 5.7 3.1 110 290
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 2 77   26    660 3300 0      0      20    12    410   810 15   7.7 190 330
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 960   350    8500 3200 0      0      900    900    22000   790 960   790   17000 1900
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 2.8 1.0  22 270 .0041 0      5.1  2.8  70   280 10   5.5 200 370
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 0 900   300    7500 9000 0      0      400    390    8100   7000 960   840   23000 2200
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 4.3 1.2  31 270 0      0      7.2  3.9  73   300 14   7.4 180 360
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 3.9 1.3  29 280 0      3.1    5.0  2.7  85   280 8.3 4.4 150 320
loop-lit/ddlm2013_true-unreach-call.i 0 930   320    9300 6200 0      0      400    390    6900   7000 960   850   15000 2300
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 4.1 1.2  30 280 .0041 .79   69    63    1400   770 110   71   1300 1400
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900   290    6100 4300 0      0      900    890    15000   3100 960   810   15000 2300
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 4.9 1.3  38 290 .0041 0      64    57    1000   1100 89   52   1200 1300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 2 860   360    7900 5200 .0041 0      130    98    2200   3200 13   7.2 220 370
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 0 53   14    430 2000 .0041 .012  .51 .33 11   41 6.9 3.7 88 300
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 4.8 1.3  32 300 .012  0      380    370    6400   7000 14   7.7 240 440
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 0 900   290    6800 8300 0      0      340    330    9600   7000 960   840   12000 2100
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 900   850    11000 3900 .11   0      8.2  4.6  86   310 960   890   20000 1200
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 5.5 1.4  36 310 .0041 0      3.9  2.2  84   270 7.5 4.0 180 320
loop-new/count_by_1_true-unreach-call_true-termination.i 2 3.0 1.1  25 270 0      .79   4.4  2.4  66   280 9.9 5.4 150 340
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 3.2 1.1  26 270 0      0      4.1  2.3  85   280 9.2 5.0 170 340
loop-new/count_by_2_true-unreach-call_true-termination.i 0 910   300    9200 5100 0      0      380    370    8500   7000 960   800   17000 3700
loop-new/count_by_k_true-unreach-call_true-termination.i 0 910   300    7700 5300 .0082 0      910    900    17000   5700 960   840   23000 1900
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 910   300    9000 3300 0      0      900    900    23000   1300 960   800   16000 4900
loop-new/gauss_sum_true-unreach-call_true-termination.i 2 84   25    640 4200 0      0      49    31    590   1400 20   10   300 410
loop-new/half_true-unreach-call_true-termination.i 0 900   290    8000 5500 0      0      870    860    12000   7000 960   810   19000 2600
loop-new/nested_true-unreach-call_true-termination.i 0 39   7.2  250 2600 0      0      .66 .41 7.7 39 5.6 3.0 110 290
loop-industry-pattern/aiob_1_true-unreach-call.c 2 35   8.5  280 1100 .12   .79   37    28    870   830 12   6.2 180 310
loop-industry-pattern/aiob_2_true-unreach-call.c 2 32   8.1  230 920 .12   0      38    30    950   850 12   6.4 170 310
loop-industry-pattern/aiob_3_true-unreach-call.c 2 36   8.4  260 1200 .12   0      44    35    630   830 11   5.7 200 310
loop-industry-pattern/aiob_4_true-unreach-call.c 2 33   8.9  230 950 .098  0      32    25    920   760 11   5.9 230 310
loop-industry-pattern/mod3_true-unreach-call.c 2 14   5.8  110 380 .0041 0      7.9  5.9  220   340 29   24   630 340
loop-industry-pattern/nested_true-unreach-call.c 0 39   8.6  270 2200 0      .012  .64 .41 8.7 41 6.0 3.2 110 300
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 9.3 2.2  66 450 0      0      4.4  2.4  96   270 10   5.6 180 310
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 8.7 2.1  67 460 0      0      5.5  2.9  100   330 11   5.9 210 310
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 8.5 2.0  66 450 0      0      4.8  2.6  95   300 13   6.6 220 330
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 9.3 2.2  58 500 0      0      6.8  3.6  69   310 11   5.7 140 300
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 8.9 2.0  57 470 0      0      4.8  2.6  73   270 11   5.8 170 310
loops/heavy_true-unreach-call.c 2 3.9 1.2  29 280 0      0      6.0  3.3  75   280 960   880   14000 6500
loops/compact_false-unreach-call.c 0 910   300    8600 4500 0      0      92    85    800   1100 97   89   950 4600
loops/heavy_false-unreach-call.c 0 910   300    9300 4400 0      0      5.1  2.8  100   300 97   71   970 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 151 40000 15000   360000 370000 11      59   156 1200 970 17000 34000   156 1200 790 17000 45000   156 22000 21000 450000 200000   156 30000 26000 550000 110000  
    correct results 91 149 2300 770   19000 66000 1.7    35   17 280 190 4100 12000   32 490 270 7600 19000   54 3300 3000 64000 54000   44 8200 7000 140000 47000  
        correct true 58 116 2000 690   17000 48000 .72   16   3 0 0 0 0   0 0 0 0 0   54 3300 3000 64000 54000   39 8200 7000 140000 47000  
        correct false 33 33 350 88   2500 19000 .97   19   14 280 190 4100 12000   32 490 270 7600 19000   0 0 0 0 0   5 0 0 0 0  
    correct-unconfimed results 4 2 630 330   6200 7000 .37   0   0 190 170 3400 3800   0 110 80 1500 1300   0 1600 1500 31000 13000   0 1000 890 24000 11000  
        correct-unconfirmed true 2 2 12 2.9 78 680 .0082 0   0 0 0 0 0   0 0 0 0 0   0 1600 1500 31000 13000   0 1000 890 24000 11000  
        correct-unconfirmed false 2 0 620 330   6100 6300 .36   0   0 190 170 3400 3800   0 110 80 1500 1300   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) 151
Run set sv-comp17.ReachSafety-Loops