Tool ULTIMATE Kojak f7c3ed31
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 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.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 7.2 1.9 58 380 2.5 0   4.7  2.6  43   280 7.4 4.0 150 320
loops/bubble_sort_false-unreach-call.i 0 8.4 2.7 67 310 2.6 0   .49 .31 7.3 40 5.8 3.1 120 300
loops/count_up_down_false-unreach-call_true-termination.i 1 5.5 1.8 47 320 2.5 0   4.0  2.3  65   270 7.2 3.9 130 320
loops/eureka_01_false-unreach-call.i 1 140   120   1700 970 2.5 0   4.8  2.6  75   280 28   19   360 690
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 7.3 2.2 54 360 2.5 0   3.9  2.2  67   280 7.4 3.9 110 320
loops/insertion_sort_false-unreach-call_true-termination.i 1 42   24   500 650 2.5 0   98    83    1300   3300 13   6.7 210 370
loops/invert_string_false-unreach-call_true-termination.i 1 12   3.6 92 500 2.5 0   5.5  3.0  68   290 8.7 4.6 160 350
loops/linear_search_false-unreach-call.i 0 900   850   9200 4600 2.3 0   .51 .34 7.0 40 6.0 3.1 93 300
loops/ludcmp_false-unreach-call.i 0 63   42   630 12000 2.5 0   .50 .31 11   39 5.9 3.1 95 290
loops/matrix_false-unreach-call_true-termination.i 1 8.2 2.5 70 370 2.5 0   7.6  5.1  73   460 7.3 4.0 82 340
loops/n.c24_false-unreach-call.i 0 900   720   14000 3700 2.3 0   .52 .35 11   39 7.0 3.8 75 290
loops/nec11_false-unreach-call_false-termination.i 1 5.5 1.8 45 340 2.5 0   3.5  2.0  55   280 7.6 4.0 130 320
loops/nec20_false-unreach-call_true-termination.i 1 5.8 2.0 48 320 2.5 0   13    6.9  110   440 7.4 3.9 120 340
loops/s3_false-unreach-call.i 0 680   620   8500 2000 2.5 0   .52 .33 8.8 42 6.3 3.3 120 300
loops/string_false-unreach-call_true-termination.i 1 16   5.0 110 470 2.6 0   6.0  3.3  43   290 17   9.2 230 380
loops/sum01_bug02_false-unreach-call_true-termination.i 1 10   3.0 80 490 2.5 0   98    85    1500   2300 9.3 5.0 140 350
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 8.3 2.4 66 380 2.5 0   98    85    1100   2200 8.8 4.8 100 350
loops/sum01_false-unreach-call_true-termination.i 1 11   3.2 91 490 2.5 0   98    86    1100   2900 9.8 5.3 180 420
loops/sum03_false-unreach-call_true-termination.i 1 22   10   190 530 2.6 0   3.9  2.2  52   280 23   13   330 1100
loops/sum04_false-unreach-call_true-termination.i 1 7.7 2.3 60 350 2.5 0   5.0  2.8  42   280 8.9 4.8 170 340
loops/sum_array_false-unreach-call.i 1 7.6 2.2 56 330 2.5 0   4.5  2.6  75   300 8.1 4.4 140 350
loops/terminator_01_false-unreach-call_true-termination.i 1 5.7 1.9 45 320 2.5 0   3.6  2.0  45   270 7.1 3.8 140 320
loops/terminator_02_false-unreach-call_true-termination.i 1 5.5 1.9 43 320 2.5 0   3.7  2.1  56   270 7.8 4.2 100 330
loops/terminator_03_false-unreach-call_true-termination.i 1 6.1 1.9 44 330 2.5 0   3.9  2.2  69   280 7.3 3.9 150 320
loops/trex01_false-unreach-call_true-termination.i 1 6.0 1.8 51 320 2.5 0   4.9  2.7  41   280 7.6 4.1 150 310
loops/trex02_false-unreach-call_true-termination.i 1 5.5 1.9 43 320 2.5 0   3.7  2.1  57   270 7.6 4.1 160 320
loops/trex03_false-unreach-call_true-termination.i 1 6.3 2.0 52 320 2.5 0   3.7  2.1  62   270 7.5 4.0 150 320
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 1 7.2 2.1 54 330 2.5 0   3.4  1.9  55   270 7.9 4.2 150 330
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 1 9.7 2.9 75 490 2.5 0   4.3  2.3  49   280 20   11   350 550
loops/vogal_false-unreach-call.i 1 32   10   270 790 2.6 0   6.0  3.3  86   320 97   72   990 1400
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 6.1 1.9 43 330 2.5 0   3.6  2.0  65   270 7.5 4.0 130 320
loops/array_true-unreach-call_true-termination.i 2 6.0 2.0 47 320 2.5 0   4.3  2.4  74   280 12   6.6 180 370
loops/bubble_sort_true-unreach-call.i 2 6.7 2.0 57 350 2.6 0   4.5  2.5  75   270 6.3 3.4 86 310
loops/count_up_down_true-unreach-call_true-termination.i 2 49   43   560 380 2.5 0   350    340    8100   7000 69   59   1200 520
loops/eureka_01_true-unreach-call.i 0 230   170   3300 1600 2.5 0   .65 .41 8.7 40 7.2 3.8 82 300
loops/eureka_05_true-unreach-call_true-termination.i 1 59   38   660 1000 2.5 0   36    26    730   840 11   5.7 170 380
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 6.6 2.0 53 330 2.5 0   5.1  2.8  58   270 7.7 4.2 150 320
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 6.2 1.9 45 330 2.5 0   4.3  2.4  66   280 8.2 4.4 160 330
loops/insertion_sort_true-unreach-call_true-termination.i 0 900   810   12000 1200 2.3 0   .62 .40 7.8 39 6.1 3.2 110 300
loops/invert_string_true-unreach-call_true-termination.i 2 81   59   940 680 2.5 0   24    18    530   660 300   270   3300 4500
loops/linear_sea.ch_true-unreach-call.i 0 900   860   11000 1100 2.5 0   .53 .34 14   41 6.1 3.2 110 300
loops/lu.cmp_true-unreach-call.i 0 63   41   570 12000 2.5 0   .49 .30 9.2 40 5.4 2.9 88 290
loops/matrix_true-unreach-call_true-termination.i 2 9.1 2.8 74 430 2.5 0   8.8  6.4  210   430 16   9.4 260 500
loops/n.c11_true-unreach-call_false-termination.i 2 7.7 2.4 64 350 2.5 0   5.5  3.0  60   290 12   6.4 230 360
loops/n.c40_true-unreach-call_true-termination.i 2 170   160   2200 640 2.5 0   4.2  2.3  90   270 180   170   2900 730
loops/nec40_true-unreach-call_true-termination.i 2 170   160   1900 680 2.5 0   4.9  2.7  70   280 200   190   2900 820
loops/string_true-unreach-call_true-termination.i 2 8.3 2.3 66 390 2.5 0   7.4  4.0  100   320 10   5.5 160 350
loops/sum01_true-unreach-call_true-termination.i 1 7.0 2.1 54 340 2.5 0   900    890    16000   3200 7.8 4.1 120 330
loops/sum03_true-unreach-call_false-termination.i 2 6.6 1.9 47 340 2.5 0   4.8  2.7  68   280 9.0 4.7 170 340
loops/sum04_true-unreach-call_true-termination.i 2 8.6 2.7 60 480 2.5 0   4.7  2.6  74   280 16   9.0 240 530
loops/sum_array_true-unreach-call.i 0 900   850   10000 650 2.3 0   .55 .35 9.5 40 6.4 3.4 120 310
loops/terminator_02_true-unreach-call_true-termination.i 2 6.6 2.0 46 340 2.5 0   4.6  2.5  61   280 7.2 3.9 140 310
loops/terminator_03_true-unreach-call_true-termination.i 2 6.1 1.9 46 340 2.5 0   4.7  2.6  67   280 7.7 4.2 140 310
loops/trex01_true-unreach-call_true-termination.i 2 5.8 1.9 51 320 2.5 0   410    380    13000   7000 8.0 4.3 160 330
loops/trex02_true-unreach-call_true-termination.i 2 6.2 1.8 52 350 2.5 0   5.3  2.9  56   280 7.8 4.2 150 320
loops/trex03_true-unreach-call_true-termination.i 2 5.9 2.0 50 320 2.5 0   5.1  2.8  68   280 7.4 4.0 130 320
loops/trex04_true-unreach-call_false-termination.i 2 6.2 1.9 48 330 2.5 0   5.5  3.0  68   280 7.6 4.0 69 330
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 2 7.3 2.4 66 380 2.5 0   530    520    9100   7000 10   5.6 200 360
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 2 6.6 2.1 48 330 2.6 0   12    6.4  140   430 9.4 5.1 170 350
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 6.1 1.9 45 320 2.5 0   5.5  3.1  62   280 10   5.3 120 330
loops/vogal_true-unreach-call.i 0 900   820   11000 2400 2.3 0   .48 .31 9.6 39 6.2 3.4 86 290
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 5.8 1.9 51 330 2.5 0   4.5  2.5  66   270 8.3 4.5 140 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 5.6 1.8 44 330 2.5 0   4.5  2.5  57   270 7.4 4.0 140 310
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 5.6 1.8 46 320 2.5 0   4.0  2.2  84   270 7.6 4.1 110 320
loop-acceleration/array_false-unreach-call1_true-termination.i 0 900   720   12000 3800 2.3 0   .52 .32 9.3 40 7.3 3.9 88 300
loop-acceleration/array_false-unreach-call2_true-termination.i 0 900   720   14000 3700 2.3 0   .56 .38 11   40 5.8 3.1 93 310
loop-acceleration/array_false-unreach-call3_true-termination.i 0 900   720   13000 2400 2.3 0   .56 .36 12   44 6.2 3.3 130 300
loop-acceleration/const_false-unreach-call1.i 0 900   810   12000 880 2.3 0   .53 .33 11   41 5.7 3.0 97 300
loop-acceleration/diamond_false-unreach-call1.i 1 850   800   12000 820 2.6 0   6.9  3.7  71   300 98   56   640 6400
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 900   790   11000 1900 2.3 0   .54 .36 13   41 6.1 3.2 130 300
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 6.6 1.9 47 340 2.5 0   3.5  2.0  32   270 7.5 4.0 150 310
loop-acceleration/nested_false-unreach-call1.i 0 900   830   12000 1500 2.3 0   .52 .33 9.2 39 6.2 3.3 110 300
loop-acceleration/phases_false-unreach-call1.i 0 900   880   12000 2300 2.3 0   .54 .33 12   40 6.1 3.2 110 300
loop-acceleration/phases_false-unreach-call2.i 1 5.5 1.8 48 320 2.5 0   3.6  2.0  45   270 7.4 4.0 140 320
loop-acceleration/simple_false-unreach-call1.i 0 900   800   13000 980 2.3 0   .57 .37 12   42 5.5 2.9 64 300
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 5.5 1.8 47 320 2.5 0   4.6  2.6  42   270 7.1 3.8 120 320
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 5.6 1.8 45 310 2.5 0   3.6  2.0  75   270 7.7 4.1 130 320
loop-acceleration/simple_false-unreach-call4.i 0 900   810   11000 960 2.3 0   .50 .34 6.4 40 6.0 3.2 130 300
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 7.0 2.2 49 360 2.5 0   4.4  2.5  70   270 11   6.2 180 360
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 7.4 2.3 50 350 2.5 0   3.8  2.1  44   270 12   6.4 190 350
loop-acceleration/array_true-unreach-call1_true-termination.i 0 900   730   13000 2900 2.3 0   .50 .32 9.6 41 5.8 3.1 89 300
loop-acceleration/array_true-unreach-call2_true-termination.i 0 900   720   12000 3100 2.3 0   .68 .45 9.2 41 6.1 3.2 100 300
loop-acceleration/array_true-unreach-call3_true-termination.i 0 900   720   15000 4400 2.3 0   .59 .38 9.5 40 5.9 3.1 94 300
loop-acceleration/array_true-unreach-call4_true-termination.i 0 900   720   12000 3400 2.3 0   .52 .32 11   40 6.1 3.2 120 300
loop-acceleration/const_true-unreach-call1.i 0 900   800   12000 870 2.3 0   .51 .34 11   40 5.8 3.0 95 290
loop-acceleration/diamond_true-unreach-call1_true-termination.i 0 900   840   12000 680 2.3 0   .52 .32 11   40 5.9 3.1 100 300
loop-acceleration/diamond_true-unreach-call2.i 1 13   4.5 120 470 2.5 0   4.7  2.6  65   280 47   40   650 520
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 900   790   12000 1800 2.3 0   .54 .34 12   40 6.0 3.2 85 300
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 5.8 1.9 46 320 2.5 0   380    370    8200   7000 7.9 4.3 150 320
loop-acceleration/nested_true-unreach-call1.i 0 900   830   13000 1500 2.3 0   .51 .32 11   41 5.7 3.0 99 300
loop-acceleration/overflow_true-unreach-call1.i 0 900   810   14000 1100 2.3 0   .47 .31 9.1 39 5.2 2.8 80 290
loop-acceleration/phases_true-unreach-call1.i 0 900   880   12000 2400 2.3 0   .48 .31 8.3 40 5.5 2.9 63 300
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 6.8 2.2 58 320 2.5 0   900    900    25000   430 10   6.0 160 350
loop-acceleration/simple_true-unreach-call1.i 0 900   800   13000 1000 2.3 0   .53 .34 13   39 5.3 2.9 95 290
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 5.4 1.7 46 330 2.5 0   4.8  2.6  59   280 7.8 4.2 160 320
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 900   800   12000 1200 2.3 0   .50 .33 11   39 7.1 3.8 86 300
loop-acceleration/simple_true-unreach-call4.i 0 900   810   13000 1100 2.3 0   .58 .38 8.5 40 5.9 3.1 120 300
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 0 900   890   12000 500 2.3 0   .66 .41 7.9 40 5.8 3.1 120 300
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 8.1 2.4 56 390 2.5 0   4.9  2.7  59   300 16   8.7 280 430
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 7.2 2.2 56 340 2.5 0   4.1  2.3  64   280 7.2 3.9 140 310
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 2 9.3 2.8 75 460 2.5 0   900    890    15000   2700 11   5.9 180 370
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 7.7 2.4 56 430 2.5 0   420    410    12000   7000 9.9 5.5 170 360
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 2 21   7.4 180 710 2.6 0   900    890    12000   2000 15   8.6 230 520
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 2 18   5.4 130 550 2.6 0   900    890    15000   3100 15   8.3 220 490
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 2 11   3.4 97 490 2.6 0   900    890    15000   2100 16   8.7 170 480
loop-invgen/down_true-unreach-call_true-termination.i 0 900   740   13000 3600 2.3 0   .67 .42 7.0 40 6.2 3.3 110 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900   750   12000 4200 2.3 0   .62 .40 7.8 41 5.9 3.1 120 290
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900   820   15000 760 2.3 0   .61 .39 8.5 40 5.2 2.8 57 290
loop-invgen/heapsort_true-unreach-call_true-termination.i 2 67   38   840 1000 2.5 0   900    890    16000   1700 120   87   1200 1400
loop-invgen/id_build_true-unreach-call_true-termination.i 2 7.4 2.3 63 380 2.5 0   4.8  2.7  86   290 8.8 4.8 150 350
loop-invgen/large_const_true-unreach-call_true-termination.i 2 8.4 2.5 62 440 2.5 0   5.2  3.0  83   290 13   7.2 250 420
loop-invgen/nest-if3_true-unreach-call_true-termination.i 2 9.5 3.0 80 480 2.5 0   900    890    15000   1400 10   5.6 180 370
loop-invgen/nested6_true-unreach-call_true-termination.i 2 9.5 2.9 80 470 2.5 0   900    880    24000   5100 12   6.8 170 410
loop-invgen/nested9_true-unreach-call_true-termination.i 2 16   6.3 150 510 2.5 0   900    890    15000   5200 15   8.2 250 530
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 2 20   7.3 180 550 2.5 0   450    440    6400   7000 22   12   480 580
loop-invgen/seq_true-unreach-call_true-termination.i 0 900   750   11000 2500 2.3 0   .63 .42 8.1 39 6.1 3.2 120 300
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 900   740   14000 3300 2.3 0   .63 .41 7.6 39 5.8 3.1 44 310
loop-invgen/up_true-unreach-call_true-termination.i 0 900   750   13000 2700 2.3 0   .66 .41 6.6 40 6.2 3.3 120 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 0 900   790   12000 1100 2.3 0   .68 .44 7.6 41 6.9 3.6 110 320
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 2 6.8 2.1 58 330 2.5 0   900    900    22000   860 13   7.3 230 380
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 7.3 2.3 64 380 2.5 0   5.3  3.0  60   290 14   7.4 190 370
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 2 6.9 2.1 57 330 2.5 0   340    340    7300   7000 10   5.6 190 370
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 8.1 2.1 65 370 2.5 0   4.7  2.6  110   280 10   5.5 150 350
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 6.3 2.0 46 330 2.5 0   4.4  2.5  96   280 7.7 4.2 160 330
loop-lit/ddlm2013_true-unreach-call.i 0 900   820   11000 1200 2.3 0   .49 .31 12   39 5.5 3.0 110 290
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 140   100   1800 1300 2.5 0   8.2  4.4  86   310 350   290   4900 4700
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 2 7.2 2.3 63 370 2.5 0   900    900    17000   2900 10   5.8 160 350
loop-lit/gr2006_true-unreach-call_true-termination.c.i 2 750   640   13000 1400 2.5 0   8.5  4.5  140   340 960   810   11000 4700
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 2 7.3 2.3 58 360 2.5 0   900    900    19000   1300 8.7 4.8 150 340
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 2 6.6 2.0 46 330 2.5 0   390    390    6200   7000 8.3 4.5 160 330
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 6.7 2.0 48 330 2.5 0   380    370    6500   7000 8.3 4.5 150 340
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 2 6.5 2.1 50 320 2.5 0   340    330    6200   7000 8.8 4.8 150 350
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 900   830   13000 830 2.3 0   .69 .43 6.2 41 5.7 3.0 100 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 6.1 1.9 46 320 2.5 0   4.1  2.3  67   270 8.0 4.2 140 340
loop-new/count_by_1_true-unreach-call_true-termination.i 0 900   730   13000 3200 2.3 0   .53 .34 10   42 5.2 2.8 87 290
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 6.4 2.1 56 330 2.5 0   4.0  2.2  61   270 9.4 5.1 180 360
loop-new/count_by_2_true-unreach-call_true-termination.i 0 900   730   12000 3000 2.3 0   .56 .37 9.1 42 6.5 3.4 120 300
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900   780   15000 3500 2.3 0   .66 .42 8.9 41 6.2 3.3 120 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900   730   14000 4800 2.3 0   .65 .42 8.0 40 6.1 3.2 87 310
loop-new/gauss_sum_true-unreach-call_true-termination.i 0 900   830   13000 800 2.3 0   .58 .37 9.1 39 6.0 3.2 120 300
loop-new/half_true-unreach-call_true-termination.i 0 900   820   12000 830 2.3 0   .54 .35 13   42 6.1 3.2 120 300
loop-new/nested_true-unreach-call_true-termination.i 1 120   91   1600 1400 2.5 0   900    890    17000   1900 960   830   12000 4500
loop-industry-pattern/aiob_1_true-unreach-call.c 0 8.6 2.8 70 310 2.6 0   .54 .35 6.7 39 5.9 3.2 110 300
loop-industry-pattern/aiob_2_true-unreach-call.c 0 8.4 2.7 69 310 2.6 0   .60 .38 12   44 5.8 3.1 120 300
loop-industry-pattern/aiob_3_true-unreach-call.c 0 7.9 2.6 59 310 2.6 0   .63 .41 8.4 40 6.1 3.2 120 300
loop-industry-pattern/aiob_4_true-unreach-call.c 0 8.1 2.7 67 300 2.6 0   .48 .32 10   39 6.5 3.4 95 330
loop-industry-pattern/mod3_true-unreach-call.c 0 900   890   12000 510 2.3 0   .48 .31 9.2 41 5.9 3.1 110 300
loop-industry-pattern/nested_true-unreach-call.c 0 900   720   14000 3100 2.3 0   .57 .36 11   44 6.1 3.2 130 300
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 8.3 2.7 59 300 2.6 0   .48 .32 11   40 6.8 3.6 100 310
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 8.2 2.8 66 300 2.6 0   .56 .36 13   44 6.1 3.2 120 290
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 8.7 2.7 67 320 2.6 0   .52 .35 8.9 39 5.7 3.0 90 290
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 8.8 2.7 60 320 2.6 0   .56 .36 11   44 6.5 3.5 95 300
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 8.2 2.7 70 310 2.6 0   .55 .35 11   40 6.0 3.2 120 300
loops/heavy_true-unreach-call.c 0 900   770   7000 7300 2.3 0   .56 .36 9.0 40 5.3 2.9 110 290
loops/compact_false-unreach-call.c 0 900   880   9700 5200 2.3 0   .54 .35 6.7 42 5.8 3.1 130 300
loops/heavy_false-unreach-call.c 0 900   770   7400 7300 2.3 0   .50 .32 11   39 6.6 3.5 140 310
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 156 147 49000 42000 650000 190000 390 0   156 550 430 7000 20000   156 620 360 8800 25000   156 17000 17000 330000 120000   156 4000 3200 54000 55000  
    correct results 89 143 3100 2400 40000 39000 230 0   31 540 420 6900 20000   33 520 310 7000 20000   31 15000 15000 300000 110000   53 2700 2100 36000 35000  
        correct true 54 108 1800 1300 24000 24000 140 0   7 0 0 0 0   0 0 0 0 0   31 15000 15000 300000 110000   53 2700 2100 36000 35000  
        correct false 35 35 1300 1000 16000 15000 89 0   24 540 420 6900 20000   33 520 310 7000 20000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 4 200 140 2400 3200 10 0   0 0 0 0 0   0 0 0 0 0   0 1800 1800 34000 6200   3 1000 880 13000 5700  
        correct-unconfirmed true 4 4 200 140 2400 3200 10 0   0 0 0 0 0   0 0 0 0 0   0 1800 1800 34000 6200   0 1000 880 13000 5700  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (156 tasks, max score: 261) 147
Run set sv-comp17.ReachSafety-Loops