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