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