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