Tool ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 CPAchecker 1.7-svn 27742
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS Linux 4.15.0-42-generic Linux 4.15.0-58-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Run set uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Loops utaipan.sv-comp19_prop-reachsafety.ReachSafety-Loops veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops kInduction-kipdr.ReachSafety-Loops kInduction-dfkipdr.ReachSafety-Loops
Options --full-output --full-output -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction-kipdrInvariants -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction-kipdrdfInvariants -setprop cpa.invariants.useMod2Template=true
../programs/benchmarks/ status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage status cputime (s) walltime (s) memUsage
loops/array_false-unreach-call_true-termination.i 7.81 2.80 364392448 69.8 7.11 2.78 335081472 60.8 3.01 1.23 149184512 29.3 4.88 2.56 188350464 5.66 2.97 215855104
loops/bubble_sort_false-unreach-call.i 12.3  3.80 448061440 87.3 11.5  3.57 434569216 86.1 475    461    2164862976 3790   906    456    4326375424 904    454    4631867392
loops/count_up_down_false-unreach-call_true-termination.i 7.48 2.59 371195904 59.6 6.84 2.56 340815872 59.0 9.07 3.59 267280384 73.3 4.22 2.28 157237248 6.08 3.21 183029760
loops/eureka_01_false-unreach-call_true-termination.i 778    742    1923280896 10200   681    625    2284457984 8290   44.5  25.7  677478400 436   905    453    4928905216 904    453    5839478784
loops/for_bounded_loop1_false-unreach-call_true-termination.i 8.23 2.96 352215040 73.9 9.87 3.33 373202944 74.4 13.7  5.05 273289216 99.5 5.18 2.75 204009472 6.28 3.31 253988864
loops/insertion_sort_false-unreach-call_true-termination.i 356    310    1149542400 4170   900    834    1375944704 9760   434    409    4165496832 4000   6.99 3.65 239767552 75.9  38.2  1346576384
loops/invert_string_false-unreach-call_true-termination.i 16.8  7.41 524447744 146   20.2  8.27 574246912 186   28.5  13.3  294199296 208   10.6  5.49 289415168 11.6  6.01 587268096
loops/linear_search_false-unreach-call.i 900    858    709435392 11100   901    879    842792960 12700   17.8  6.53 276803584 135   15.0  7.71 347635712 15.5  7.94 685727744
loops/ludcmp_false-unreach-call.i 39.6  25.8  862752768 344   44.0  26.1  912191488 357   30.6  17.9  1493413888 324   238    120    14999998464 266    134    14999998464
loops/matrix_false-unreach-call_true-termination.i 9.43 3.16 372797440 77.9 10.2  3.78 383152128 79.3 508    480    9144442880 3580   7.23 3.77 251817984 11.4  5.89 380399616
loops/n.c24_false-unreach-call.i 901    779    3794640896 10300   901    769    4599808000 12000   901    878    3033464832 10100   902    453    2977046528 902    452    3953127424
loops/nec11_false-unreach-call_false-termination.i 7.98 2.71 366018560 60.4 7.52 2.67 337661952 60.2 12.9  4.71 264101888 104   4.24 2.29 160800768 4.81 2.56 186462208
loops/nec20_false-unreach-call_true-termination.i 8.58 2.81 377085952 68.2 7.85 2.74 371376128 68.2 19.0  7.20 286695424 138   4.80 2.57 191229952 6.34 3.35 213651456
loops/s3_false-unreach-call.i 13.6  4.26 343076864 99.4 44.3  13.9  742850560 377   92.0  66.7  867495936 998   50.0  25.2  700493824 66.1  33.3  1060552704
loops/string_false-unreach-call_true-termination.i 20.7  8.09 570228736 178   24.9  11.4  599498752 212   31.6  11.1  300892160 228   64.9  39.2  1506467840 84.1  42.4  2015133696
loops/sum01_bug02_false-unreach-call_true-termination.i 12.4  4.42 490463232 101   13.4  4.99 520835072 130   15.5  5.93 292569088 136   6.50 3.41 231092224 7.19 3.77 247517184
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 10.8  4.01 467501056 91.4 10.7  4.27 496185344 96.1 14.6  5.74 285618176 119   5.98 3.12 211197952 7.82 4.10 229523456
loops/sum01_false-unreach-call_true-termination.i 12.4  4.36 555548672 99.2 13.0  5.05 504274944 106   15.6  5.98 296931328 137   6.69 3.51 244858880 8.76 4.58 261009408
loops/sum03_false-unreach-call_true-termination.i 225    214    557219840 3140   163    153    521383936 2020   14.8  5.65 312262656 126   8.03 4.19 239542272 7.88 4.11 306274304
loops/sum04_false-unreach-call_true-termination.i 9.48 3.27 367296512 74.6 9.97 3.44 411553792 82.8 15.6  5.77 296759296 112   5.52 2.92 214540288 7.04 3.70 228667392
loops/sum_array_false-unreach-call.i 9.28 2.92 381100032 71.6 9.50 3.42 378015744 70.9 2.97 1.33 144781312 27.0 7.87 4.14 283840512 10.7  5.65 458608640
loops/terminator_01_false-unreach-call_true-termination.i 7.78 3.08 354267136 64.2 8.54 3.39 355893248 62.9 8.68 3.52 267722752 78.0 4.46 2.40 170348544 5.35 2.82 187265024
loops/terminator_02_false-unreach-call_true-termination.i 7.83 2.69 369639424 70.8 7.76 3.02 332341248 57.9 13.5  5.09 276738048 120   4.69 2.49 166719488 6.16 3.24 203735040
loops/terminator_03_false-unreach-call_true-termination.i 8.24 2.82 353406976 59.4 7.37 2.64 342835200 67.0 9.01 3.55 271675392 74.2 4.27 2.30 171413504 4.95 2.61 188321792
loops/trex01_false-unreach-call_true-termination.i 8.02 2.73 353669120 66.1 7.99 2.76 363319296 60.4 14.4  5.32 270548992 112   4.75 2.53 170160128 5.17 2.76 194490368
loops/trex02_false-unreach-call_true-termination.i 8.12 3.14 368496640 62.7 7.64 3.02 349016064 64.0 13.2  4.84 270438400 96.4 4.22 2.28 171036672 5.85 3.11 195399680
loops/trex03_false-unreach-call_true-termination.i 8.04 3.10 377573376 66.2 7.94 2.71 366645248 61.6 14.1  5.11 270266368 118   4.55 2.43 166617088 6.06 3.23 188583936
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 9.54 3.37 372830208 75.5 10.2  3.37 435073024 86.6 16.5  5.88 297783296 123   4.66 2.48 166006784 5.00 2.65 182407168
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 14.8  5.54 485830656 122   17.2  5.66 632688640 148   29.1  16.7  284282880 273   14.8  7.62 450633728 20.4  10.4  793362432
loops/vogal_false-unreach-call.i 900    858    993341440 10600   900    868    1026551808 11600   62.2  46.1  374079488 675   49.9  26.3  975699968 77.6  39.1  1492488192
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 6.95 2.57 347701248 65.1 8.01 2.74 371138560 62.3 13.7  4.93 300142592 103   4.22 2.25 162508800 5.31 2.82 178978816
loops/array_true-unreach-call_true-termination.i 9.58 3.92 421613568 76.3 10.8  3.90 484519936 101   3.13 1.36 146894848 26.7 5.54 2.92 195346432 5.81 3.05 204066816
loops/bubble_sort_true-unreach-call_true-termination.i 8.50 2.69 366858240 63.1 8.11 3.06 345559040 55.6 17.3  7.68 431992832 142   4.09 2.19 149757952 5.20 2.77 167141376
loops/count_up_down_true-unreach-call_true-termination.i 11.2  3.77 445214720 90.0 10.3  3.98 459309056 89.4 14.9  7.05 453414912 118   906    456    5787004928 906    456    6388199424
loops/eureka_01_true-unreach-call.i 901    860    4383518720 10800   900    853    6861750272 11600   135    83.4  1091571712 1510   904    453    3410120704 905    453    4813615104
loops/eureka_05_true-unreach-call_true-termination.i 900    856    1274081280 11300   900    838    1670717440 12000   114    68.7  931643392 1030   903    717    4870574080 904    453    3520335872
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 8.43 2.80 361582592 59.8 7.30 2.67 333582336 59.1 12.9  6.43 464801792 111   4.62 2.47 169775104 4.23 2.26 165355520
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 8.26 2.67 364294144 64.6 8.16 2.74 376197120 70.5 12.8  6.40 460390400 107   4.84 2.61 168894464 4.21 2.27 172081152
loops/insertion_sort_true-unreach-call_true-termination.i 900    831    2752880640 9460   900    819    1223872512 9620   786    759    6304948224 7380   6.48 3.41 236851200 902    452    1948749824
loops/invert_string_true-unreach-call_true-termination.i 288    260    1154482176 3480   901    744    967974912 9920   101    65.4  773144576 937   36.3  18.4  519729152 33.7  17.1  659357696
loops/linear_sea.ch_true-unreach-call.i 900    866    766726144 10700   901    880    686444544 13500   128    68.1  1273708544 1430   908    455    5806919680 903    453    3625664512
loops/lu.cmp_true-unreach-call.i 11.2  4.11 482570240 96.4 48.7  29.6  962793472 484   64.5  39.0  3560984576 701   254    128    14999998464 11.9  6.18 406536192
loops/matrix_true-unreach-call_true-termination.i 11.3  4.37 506499072 102   900    882    1792077824 13700   28.5  11.2  512503808 231   5.80 3.07 199708672 6.39 3.37 234344448
loops/n.c11_true-unreach-call_false-termination.i 11.0  3.66 441876480 86.6 11.1  3.94 500846592 105   27.5  10.7  510230528 204   5.15 2.74 196026368 5.15 2.73 188063744
loops/n.c40_true-unreach-call_true-termination.i 27.5  18.0  346230784 312   11.6  3.54 418906112 98.2 30.7  13.5  528666624 266   4.49 2.39 169205760 5.44 2.87 195817472
loops/nec40_true-unreach-call_true-termination.i 30.1  20.3  370577408 315   12.0  3.75 441688064 93.6 31.6  14.7  508186624 274   5.42 2.87 178065408 5.00 2.64 198443008
loops/string_true-unreach-call_true-termination.i 10.3  3.65 442404864 79.3 11.8  3.90 509628416 89.3 17.8  6.17 200183808 135   7.51 3.93 236834816 7.77 4.08 307277824
loops/sum01_true-unreach-call_true-termination.i 10.1  3.56 469286912 77.1 11.4  4.03 503975936 94.7 16.3  7.53 533598208 126   906    455    5721006080 163    81.9  1754812416
loops/sum03_true-unreach-call_false-termination.i 8.28 2.83 359284736 62.5 8.50 2.93 365674496 60.3 12.6  6.68 440643584 118   5.08 2.70 182001664 6.15 3.25 201543680
loops/sum04_true-unreach-call_true-termination.i 11.1  3.75 495104000 98.9 11.6  4.59 540524544 100   17.4  7.79 577966080 144   6.53 3.44 219357184 5.61 2.97 196382720
loops/sum_array_true-unreach-call.i 900    859    2098118656 12300   901    838    1231941632 10200   22.6  11.9  197603328 202   906    454    2602086400 906    454    4053262336
loops/terminator_02_true-unreach-call_true-termination.i 9.13 2.94 376729600 69.4 8.58 3.31 369651712 70.5 14.5  6.94 470044672 121   5.11 2.74 181862400 6.61 3.46 202350592
loops/terminator_03_true-unreach-call_true-termination.i 8.87 3.23 372920320 66.0 7.72 2.84 335761408 57.2 13.4  6.70 446615552 122   4.24 2.29 176812032 4.53 2.40 169795584
loops/trex01_true-unreach-call_true-termination.i 8.60 2.90 376123392 68.0 7.89 2.78 356401152 69.9 13.3  6.60 440668160 103   64.0  32.3  1833865216 7.24 3.79 207626240
loops/trex02_true-unreach-call_true-termination.i 7.49 3.10 339021824 72.1 7.76 3.08 336429056 66.4 13.1  6.61 454356992 114   4.76 2.54 174833664 4.64 2.47 169766912
loops/trex03_true-unreach-call_true-termination.i 8.32 3.14 372924416 59.3 8.16 3.14 364941312 74.8 14.1  6.97 472539136 121   4.66 2.45 179458048 6.10 3.21 230166528
loops/trex04_true-unreach-call_false-termination.i 7.75 2.74 343998464 57.0 7.79 2.79 348966912 59.5 12.9  6.64 456294400 108   4.77 2.57 181334016 5.80 3.06 175890432
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 10.3  3.49 413528064 80.7 10.2  3.60 456699904 76.3 18.5  8.02 467693568 166   905    454    2598305792 904    454    2803388416
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 8.96 3.17 353742848 72.6 8.98 3.00 380346368 76.5 46.8  31.4  481017856 478   7.44 3.88 292306944 11.9  6.13 374845440
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 7.99 2.73 358338560 65.7 8.37 2.82 371417088 65.0 17.9  7.76 465526784 154   4.67 2.49 177434624 5.06 2.69 175550464
loops/vogal_true-unreach-call.i 901    862    937992192 11300   901    840    1229488128 12900   130    58.3  952455168 1220   68.4  34.4  1091694592 102    51.2  1600000000
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 8.01 2.74 370495488 64.9 7.16 3.07 353071104 56.4 12.8  6.40 460648448 94.4 4.29 2.29 166637568 4.90 2.62 164040704
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 7.88 2.73 360017920 68.4 8.54 2.78 371478528 67.2 12.0  6.31 420872192 113   4.45 2.37 172519424 4.33 2.33 166400000
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 8.15 3.11 374337536 63.5 7.63 2.81 354050048 64.6 12.3  6.41 441409536 114   4.54 2.43 167870464 4.43 2.34 167178240
loop-acceleration/array_false-unreach-call1_true-termination.i 901    869    907264000 10800   901    845    1005522944 11100   241    219    1935589376 3410   905    453    3875434496 903    452    2906062848
loop-acceleration/array_false-unreach-call2_true-termination.i 900    872    729780224 10300   900    865    931815424 10200   4.63 1.66 187727872 35.1 905    453    3968561152 905    453    2635198464
loop-acceleration/array_false-unreach-call3_true-termination.i 900    864    1023807488 10800   900    846    1180688384 10900   465    440    1960067072 6400   905    453    4704747520 903    452    3208765440
loop-acceleration/const_false-unreach-call1.i 901    878    588062720 11900   901    881    650506240 12400   217    203    2460811264 3070   908    457    6432206848 905    456    5497778176
loop-acceleration/diamond_false-unreach-call1.i 901    874    612196352 12100   900    865    859828224 13100   48.1  33.4  585146368 580   27.3  13.8  562958336 43.3  21.9  1053609984
loop-acceleration/functions_false-unreach-call1_true-termination.i 900    873    620859392 10400   901    862    662208512 12100   41.0  25.8  282750976 387   907    456    6130708480 920    470    5664083968
loop-acceleration/multivar_false-unreach-call1_true-termination.i 6.77 2.80 329605120 52.2 7.37 2.52 342065152 60.3 8.97 3.59 267030528 75.6 4.27 2.29 163254272 4.50 2.39 183103488
loop-acceleration/nested_false-unreach-call1.i 901    881    855109632 10800   901    883    877821952 11200   219    202    3063672832 2930   902    452    2946355200 902    452    1885560832
loop-acceleration/phases_false-unreach-call1.i 901    883    573251584 11100   901    871    743383040 11400   372    357    9598021632 5020   906    455    3563532288 902    453    3237232640
loop-acceleration/phases_false-unreach-call2_false-termination.i 8.25 3.09 368705536 61.9 7.94 3.04 368656384 64.4 8.66 3.38 269275136 80.2 4.39 2.34 162877440 5.08 2.71 199622656
loop-acceleration/simple_false-unreach-call1.i 901    883    578711552 13800   901    879    821579776 12900   216    203    2068459520 2530   907    455    6275756032 905    454    4954419200
loop-acceleration/simple_false-unreach-call2_true-termination.i 7.78 2.68 346685440 60.2 7.97 2.99 359264256 59.4 9.26 3.60 305205248 75.9 4.34 2.30 162267136 4.87 2.58 178409472
loop-acceleration/simple_false-unreach-call3_true-termination.i 7.45 2.60 335499264 51.3 7.11 2.57 339226624 63.4 13.5  5.00 271003648 97.7 5.35 2.85 157802496 5.00 2.63 186671104
loop-acceleration/simple_false-unreach-call4.i 901    880    720240640 12700   900    871    685387776 11200   216    203    2084651008 3190   907    455    6919057408 905    454    4775211008
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 9.15 3.41 381005824 79.1 10.5  3.68 441421824 88.3 13.7  5.11 284041216 107   6.62 3.49 208535552 5.68 3.02 213250048
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 10.1  3.41 397029376 79.4 10.7  3.79 495955968 89.0 9.11 3.59 280330240 76.8 5.30 2.80 204840960 6.73 3.55 235376640
loop-acceleration/array_true-unreach-call1_true-termination.i 11.9  5.67 395673600 100   13.1  5.86 476016640 112   38.1  23.5  1210257408 413   4.86 2.59 185339904 5.44 2.90 208150528
loop-acceleration/array_true-unreach-call2_true-termination.i 901    873    927195136 10200   900    865    737062912 10500   4.20 1.57 189722624 30.4 905    454    3398778880 903    452    3701387264
loop-acceleration/array_true-unreach-call3_true-termination.i 9.37 3.44 409280512 68.7 10.1  3.56 437882880 83.5 15.1  4.93 197693440 104   4.81 2.57 185434112 5.42 2.89 170115072
loop-acceleration/array_true-unreach-call4_true-termination.i 900    866    771260416 12200   901    849    1061117952 10300   15.3  4.93 196218880 104   907    454    4679352320 904    453    3898966016
loop-acceleration/const_true-unreach-call1.i 9.53 3.21 379375616 67.0 8.52 2.90 367288320 62.5 14.0  6.99 462323712 133   4.21 2.27 163880960 4.88 2.61 195432448
loop-acceleration/diamond_true-unreach-call1_true-termination.i 901    877    756756480 11800   900    868    689500160 10900   73.9  42.5  797454336 718   29.2  14.8  653328384 44.6  22.6  936755200
loop-acceleration/diamond_true-unreach-call2.i 284    269    760512512 3700   279    259    695996416 3430   51.3  31.1  846602240 509   7.89 4.11 275771392 11.9  6.19 458801152
loop-acceleration/functions_true-unreach-call1_true-termination.i 901    871    771690496 10400   900    867    838012928 10900   121    65.4  1261559808 1390   11.1  5.72 282509312 27.0  13.7  1012273152
loop-acceleration/multivar_true-unreach-call1_true-termination.i 8.41 2.83 374009856 62.3 7.08 2.71 343953408 64.7 12.5  6.69 433000448 103   5.40 2.88 199979008 4.41 2.35 168194048
loop-acceleration/nested_true-unreach-call1.i 46.8  27.4  905871360 548   68.0  51.2  853229568 952   42.6  33.8  549322752 451   7.57 3.99 234921984 5.01 2.66 168787968
loop-acceleration/overflow_true-unreach-call1.i 901    882    572731392 11800   8.87 3.41 369819648 67.4 116    65.4  1266790400 1090   6.89 3.62 235982848 6.07 3.21 200916992
loop-acceleration/phases_true-unreach-call1.i 901    883    578965504 12000   901    864    852676608 11200   275    220    9789263872 3460   7.15 3.75 236720128 902    452    2126303232
loop-acceleration/phases_true-unreach-call2_false-termination.i 10.6  4.97 384233472 106   11.6  5.82 382922752 114   14.0  6.87 454316032 114   902    451    388108288 4.16 2.24 166965248
loop-acceleration/simple_true-unreach-call1.i 901    883    564252672 13100   9.06 3.44 376770560 72.8 117    65.5  1324388352 1230   5.56 2.91 211021824 5.78 3.04 190115840
loop-acceleration/simple_true-unreach-call2_true-termination.i 7.67 2.69 370290688 72.4 8.14 2.77 361058304 72.2 12.5  6.23 463110144 110   5.39 2.87 166977536 5.35 2.82 166760448
loop-acceleration/simple_true-unreach-call3_true-termination.i 10.4  4.84 385544192 95.0 9.70 4.84 371310592 101   118    65.5  1150091264 1340   7.56 3.96 224407552 4.95 2.61 200806400
loop-acceleration/simple_true-unreach-call4.i 8.74 2.92 373895168 67.4 8.79 3.40 353009664 70.3 14.6  6.62 466427904 124   4.48 2.42 168673280 4.20 2.25 168026112
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 15.2  8.20 478498816 146   144    136    494481408 1840   28.6  15.9  598114304 241   10.2  5.31 303955968 5.43 2.88 200835072
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 8.45 3.46 361594880 66.4 10.0  3.68 468234240 86.6 14.2  6.69 474333184 127   4.80 2.57 172777472 4.32 2.28 167477248
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 8.33 2.87 367898624 61.7 8.39 2.81 373178368 60.9 305    291    6586818560 3620   5.76 3.05 214138880 7.21 3.77 225939456
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 900    879    621518848 11600   901    882    862486528 13500   16.0  5.33 194555904 110   905    453    5115297792 904    453    3867615232
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 900    872    880119808 11600   900    871    1001635840 12200   15.8  5.25 196231168 117   905    454    1360949248 902    452    2055696384
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 900    872    668733440 10700   900    868    686161920 10800   15.5  5.18 193990656 102   905    454    5723009024 904    453    4598112256
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 53.7  46.3  481329152 741   230    220    558497792 3390   17.3  6.58 196730880 140   902    452    1918377984 902    452    1734496256
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 7.72 3.12 348057600 58.9 7.91 2.74 369172480 64.7 13.6  6.69 452288512 113   4.99 2.63 168615936 5.62 3.01 200581120
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 8.60 3.30 349491200 67.8 8.75 2.89 370327552 64.0 13.5  6.75 440950784 116   4.87 2.61 179994624 6.57 3.49 204800000
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c 25.9  16.2  600424448 287   73.8  61.6  578580480 871   49.4  41.8  14999998464 611   903    452    1835773952 902    452    1502212096
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c 25.7  16.9  558936064 311   29.5  21.0  505036800 325   48.9  41.7  14999998464 602   903    452    1847250944 902    452    1844477952
loop-invgen/id_trans_false-unreach-call_true-termination.i 8.56 3.03 352841728 76.1 7.99 3.02 341954560 64.9 13.5  5.02 271212544 103   4.47 2.40 167313408 5.74 3.02 195682304
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 9.87 3.40 408068096 93.3 10.8  3.71 468594688 96.8 16.5  7.69 480759808 143   903    452    1991700480 902    452    1934319616
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 9.91 3.36 417337344 80.2 10.2  3.71 467824640 86.1 16.1  7.39 502546432 139   904    453    3724120064 904    454    3902799872
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 12.4  4.53 489648128 108   13.2  4.63 562499584 126   19.2  8.92 663965696 178   903    452    2005377024 929    478    1987207168
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 12.4  4.26 548708352 97.4 12.4  4.34 576675840 108   901    887    1213177856 11300   903    452    2369327104 903    452    2430369792
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 11.5  3.90 522670080 105   10.9  3.98 540012544 106   901    887    1884344320 10100   6.84 3.63 237559808 10.5  5.44 271540224
loop-invgen/down_true-unreach-call_true-termination.i 901    713    1834225664 10600   900    714    1693552640 10600   150    66.2  1511993344 1430   915    459    11620765696 905    455    8403460096
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 901    731    2891374592 11100   900    726    2456018944 10700   11.6  4.10 198299648 85.5 916    460    10477498368 903    454    12037087232
loop-invgen/half_2_true-unreach-call_true-termination.i 901    754    957759488 7240   900    750    950968320 10100   140    66.4  1230422016 1200   911    456    5769441280 907    454    5900554240
loop-invgen/heapsort_true-unreach-call_true-termination.i 35.7  16.6  801550336 324   35.5  14.2  836980736 299   151    73.6  1025802240 1460   903    452    1633275904 902    452    2437668864
loop-invgen/id_build_true-unreach-call_true-termination.i 8.77 3.37 374013952 70.7 8.17 3.33 347656192 69.8 13.9  6.73 479076352 127   5.44 2.87 200478720 8.48 4.44 246480896
loop-invgen/large_const_true-unreach-call_true-termination.i 10.1  3.95 438669312 77.4 12.3  4.09 517210112 100   21.5  9.05 518164480 177   5.99 3.17 203825152 7.06 3.68 232153088
loop-invgen/nest-if3_true-unreach-call_true-termination.i 8.31 2.83 370225152 69.5 7.72 3.12 341692416 69.3 13.6  6.73 451502080 109   902    452    1632182272 902    452    1989599232
loop-invgen/nested6_true-unreach-call_true-termination.i 11.3  3.86 508846080 82.8 11.5  4.24 501403648 90.1 901    886    2554277888 7910   903    452    2777194496 902    452    2969440256
loop-invgen/nested9_true-unreach-call_true-termination.i 12.5  4.29 561446912 97.6 12.7  4.39 515764224 107   18.8  8.39 624222208 166   917    463    13979410432 903    453    5611655168
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 18.8  6.73 661110784 170   19.2  7.10 717017088 188   825    800    1771728896 8920   905    453    3589111808 905    455    3985670144
loop-invgen/seq_true-unreach-call_true-termination.i 901    808    896606208 11900   900    799    1156247552 14000   150    67.7  1060929536 1500   922    463    9807163392 905    455    11797471232
loop-invgen/string_concat-noarr_true-unreach-call_false-termination.i 901    778    1059065856 12500   901    755    1042087936 15100   149    67.3  1404440576 1440   913    457    11812614144 905    455    7421394944
loop-invgen/up_true-unreach-call_true-termination.i 901    724    1705590784 11000   900    714    1643028480 10500   152    66.1  1529344000 1410   916    460    11492941824 905    455    8120373248
loop-invgen/SpamAssassin-loop_true-unreach-call.i.v+cfa-reducer.c 15.9  5.23 574791680 137   15.7  5.75 579604480 136   901    886    673374208 8040   904    452    2119237632 903    453    1623973888
loop-invgen/apache-escape-absolute_true-unreach-call.i.v+cfa-reducer.c 19.4  6.19 661757952 155   19.7  6.53 670887936 170   901    885    1039466496 11000   906    453    3005853696 903    453    2933182464
loop-invgen/apache-get-tag_true-unreach-call.i.p+lhb-reducer.c 17.4  6.39 552701952 153   18.8  6.19 670154752 147   901    882    817225728 9320   9.36 4.95 310128640 12.6  6.50 490016768
loop-invgen/apache-get-tag_true-unreach-call.i.p+nlh-reducer.c 29.8  11.4  833286144 259   29.9  10.9  818585600 313   901    877    1218912256 10100   39.0  19.9  751833088 49.2  24.8  1763045376
loop-invgen/apache-get-tag_true-unreach-call.i.p+sep-reducer.c 38.7  12.3  1017012224 325   39.1  12.2  1078341632 351   901    874    6727045120 12700   30.1  15.3  1247756288 37.0  18.8  1355702272
loop-invgen/apache-get-tag_true-unreach-call.i.v+lhb-reducer.c 16.6  5.32 595648512 148   16.8  5.28 527900672 149   901    886    866619392 10000   8.96 4.89 252018688 11.0  5.72 354672640
loop-invgen/apache-get-tag_true-unreach-call.i.v+nlh-reducer.c 15.6  5.43 571273216 131   15.9  5.36 563212288 139   901    885    837566464 11000   7.90 4.26 257339392 9.59 5.01 316600320
loop-invgen/id_build_true-unreach-call.i.p+nlh-reducer.c 15.3  4.63 591790080 118   15.6  4.67 571031552 122   901    879    1197359104 8700   903    452    2632278016 902    452    2193960960
loop-invgen/id_build_true-unreach-call.i.p+sep-reducer.c 15.5  4.72 570970112 123   15.1  4.58 511651840 123   901    879    1630748672 8970   903    452    2387943424 902    452    2307616768
loop-invgen/id_build_true-unreach-call.i.v+lhb-reducer.c 9.15 2.96 378802176 66.9 9.13 3.32 357404672 62.3 901    887    738381824 7910   901    451    2495254528 902    452    2185166848
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 8.31 2.96 365506560 59.9 9.90 3.32 390520832 77.6 6.07 2.33 200675328 48.1 907    456    6247759872 203    102    1754972160
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 10.4  4.01 483229696 86.9 11.5  4.08 480485376 96.7 19.1  10.7  572870656 166   902    452    1029881856 901    451    1439309824
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 9.73 3.43 378445824 74.8 9.23 3.44 408387584 72.9 14.9  7.21 457785344 150   4.77 2.57 199041024 4.96 2.65 185831424
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 9.88 3.22 413626368 89.4 10.8  3.68 461332480 90.1 15.6  7.44 464867328 124   907    456    5871001600 904    454    4594335744
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 8.28 3.03 353034240 66.6 8.91 3.11 376254464 76.4 6.52 2.50 223928320 49.7 5.84 3.13 180637696 5.01 2.66 187043840
loop-lit/css2003_true-unreach-call_true-termination.c.i 8.94 2.92 361361408 68.7 8.81 2.80 365854720 77.8 6.29 2.49 199942144 50.8 4.81 2.55 178184192 6.05 3.15 224018432
loop-lit/ddlm2013_true-unreach-call.i 11.6  3.79 472412160 90.1 14.6  6.49 503889920 135   768    747    1516699648 9030   6.69 3.55 214036480 906    456    7169269760
loop-lit/gj2007_true-unreach-call_true-termination.c.i 71.1  34.2  1121878016 692   122    67.9  1107017728 1220   81.1  38.6  1514983424 881   110    55.2  1097805824 9.11 4.73 349208576
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 8.82 3.64 358580224 63.6 10.3  3.90 436621312 81.3 19.8  8.65 459554816 147   903    452    1865781248 902    452    2271289344
loop-lit/gr2006_true-unreach-call_true-termination.c.i 118    74.4  1270231040 1470   109    66.6  968597504 1270   105    46.6  1713201152 990   93.1  46.8  1138397184 32.6  16.5  826875904
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 7.81 3.23 334970880 62.8 8.98 3.37 374575104 66.9 376    362    1080385536 4170   904    453    2184716288 902    452    2031898624
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 8.55 3.12 350375936 72.3 9.65 3.28 395497472 80.7 15.0  7.18 477798400 119   906    455    5948792832 904    454    4512985088
loop-lit/jm2006_true-unreach-call_true-termination.c.i 10.4  4.06 495984640 83.5 11.8  4.18 548540416 107   15.2  7.16 448479232 118   907    456    6742016000 909    458    6270341120
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 10.1  4.22 471027712 93.3 10.9  4.57 490434560 84.3 15.3  7.37 442781696 107   907    456    6296125440 907    457    6050877440
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 900    866    879685632 12100   900    871    858714112 12800   147    83.3  1270267904 1360   909    455    6161797120 906    454    6090002432
loop-lit/gcnr2008_false-unreach-call_false-termination.i 8.14 2.71 376545280 66.0 6.88 2.96 329891840 60.8 14.3  5.43 273383424 103   4.88 2.59 160141312 5.78 3.04 199118848
loop-lit/gj2007_true-unreach-call.c.i.p+lhb-reducer.c 78.3  39.9  1131700224 774   112    67.7  1108148224 1280   85.6  41.1  1358229504 792   96.2  48.3  1023012864 9.16 4.78 283156480
loop-lit/gj2007_true-unreach-call.c.i.p+nlh-reducer.c 96.9  49.2  1078378496 962   115    59.6  1102589952 1400   89.3  41.4  1121337344 794   19.3  9.87 426512384 8.09 4.22 259407872
loop-lit/gsv2008_true-unreach-call.c.i.p+cfa-reducer.c 8.85 3.06 358748160 66.0 7.96 2.90 359505920 65.5 442    425    1187110912 4550   903    452    1839210496 667    334    1961119744
loop-lit/gsv2008_true-unreach-call.c.i.v+cfa-reducer.c 8.27 2.86 374288384 64.5 7.88 2.86 343146496 67.9 448    431    1066844160 4720   903    452    1793785856 764    383    1972469760
loop-lit/gsv2008_true-unreach-call.c.i.v+lhb-reducer.c 9.29 3.39 369344512 67.4 9.05 3.41 372969472 68.7 845    830    940523520 7520   903    452    2322247680 902    452    2153168896
loop-lit/jm2006_true-unreach-call.c.i.v+cfa-reducer.c 9.49 3.35 399237120 90.9 11.1  3.73 467677184 87.6 740    726    713408512 7370   907    456    6671650816 905    454    6157135872
loop-new/count_by_1_true-unreach-call_true-termination.i 8.96 3.42 386183168 69.4 9.67 3.42 400371712 74.3 13.8  6.63 455192576 111   4.33 2.29 168300544 4.41 2.35 167354368
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 9.40 3.15 383778816 82.3 10.5  3.45 384290816 79.6 18.1  8.12 445054976 152   4.61 2.48 170553344 4.17 2.24 166178816
loop-new/count_by_2_true-unreach-call_true-termination.i 901    717    1352425472 13300   901    717    1129000960 12600   139    65.4  1284046848 1380   908    456    7000072192 4.82 2.57 188776448
loop-new/count_by_k_true-unreach-call_true-termination.i 901    788    964091904 9760   901    776    958488576 9630   123    65.3  1111494656 1520   903    452    1545592832 903    453    2757021696
loop-new/count_by_nondet_true-unreach-call_true-termination.i 900    714    2660139008 11200   900    712    1496043520 11900   901    887    1216987136 9830   903    452    2259279872 902    452    1775910912
loop-new/gauss_sum_true-unreach-call_true-termination.i 900    772    798048256 13600   16.1  10.0  435646464 162   33.5  26.6  199536640 375   904    453    3068346368 101    50.7  1421914112
loop-new/half_true-unreach-call_true-termination.i 13.1  4.83 559931392 111   21.7  12.7  508805120 218   592    571    1155223552 6670   904    453    3346030592 904    454    3902119936
loop-new/nested_true-unreach-call_true-termination.i 164    119    4687917056 2020   186    139    4751077376 2070   901    888    715464704 8100   904    452    2649935872 902    452    2569515008
loop-new/gauss_sum_true-unreach-call.i.p+cfa-reducer.c 901    817    706846720 10500   21.3  14.4  504852480 222   398    296    1792888832 4390   903    453    3082854400 225    113    1853599744
loop-new/gauss_sum_true-unreach-call.i.p+lhb-reducer.c 901    795    944988160 8960   20.5  13.7  472084480 250   404    305    1569005568 4470   903    453    3069456384 202    101    1642332160
loop-new/gauss_sum_true-unreach-call.i.v+cfa-reducer.c 901    821    714018816 10200   15.4  8.44 493404160 151   350    277    1373319168 4160   904    453    3141214208 213    107    1799544832
loop-industry-pattern/aiob_1_true-unreach-call.c 10.9  3.74 327233536 87.9 11.2  4.15 330801152 99.1 89.4  48.6  1147912192 704   37.1  18.7  577134592 47.6  24.1  1029484544
loop-industry-pattern/aiob_2_true-unreach-call.c 11.3  3.87 324497408 91.7 11.3  3.75 335077376 85.4 87.6  47.7  1293918208 632   35.2  17.8  644579328 45.2  22.8  914804736
loop-industry-pattern/aiob_3_true-unreach-call.c 11.2  3.77 329691136 95.4 11.6  3.87 333271040 92.2 89.1  47.9  1262125056 637   37.7  19.1  552308736 49.0  24.7  1116327936
loop-industry-pattern/aiob_4_true-unreach-call.c 10.9  3.73 330932224 86.6 10.8  4.13 329576448 81.1 85.0  46.9  1264054272 700   34.1  17.3  596914176 58.4  29.4  944627712
loop-industry-pattern/aiob_4_true-unreach-call.c.v+cfa-reducer.c 908    141    13518364672 4430   19.4  6.63 652558336 172   98.7  50.4  1287245824 912   36.4  18.4  624078848 57.0  28.8  1225674752
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lh-reducer.c 16.1  4.87 576282624 143   18.3  6.14 536358912 163   95.2  48.7  1150824448 684   40.4  21.1  638509056 57.0  28.7  1232801792
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lhb-reducer.c 24.3  9.68 571801600 210   35.2  14.9  842383360 312   112    53.4  1321938944 842   41.9  21.6  674193408 53.6  27.0  1539178496
loop-industry-pattern/aiob_4_true-unreach-call.c.v+nlh-reducer.c 36.5  19.2  840118272 333   31.3  14.8  717467648 273   70.7  31.3  1670688768 699   6.48 3.41 195997696 7.63 4.01 278372352
loop-industry-pattern/mod3_true-unreach-call.c 9.20 3.41 366903296 70.0 9.29 3.91 347111424 83.7 29.2  21.3  449269760 300   15.1  7.72 240939008 11.8  6.08 279838720
loop-industry-pattern/mod3_true-unreach-call.c.v+cfa-reducer.c 7.64 2.92 337506304 57.6 7.74 2.87 347348992 63.6 773    763    741011456 8010   11.9  6.23 227201024 13.0  6.69 270229504
loop-industry-pattern/mod3_true-unreach-call.c.v+lhb-reducer.c 8.81 2.99 378605568 68.9 9.19 3.09 370978816 71.6 901    891    716398592 11300   902    452    2186735616 902    452    2351730688
loop-industry-pattern/mod3_true-unreach-call.c.v+sep-reducer.c 10.1  4.00 388513792 87.4 9.03 3.90 347295744 84.2 901    890    626409472 8620   903    452    2172411904 902    452    2292551680
loop-industry-pattern/nested_true-unreach-call.c 901    798    5811875840 11100   32.7  12.3  894160896 288   74.8  33.9  1551556608 684   903    452    3797164032 903    452    3127734272
loop-industry-pattern/ofuf_1_true-unreach-call.c 11.5  3.54 434192384 102   11.8  3.55 451686400 102   29.5  13.1  469647360 281   7.99 4.17 252002304 8.27 4.33 296673280
loop-industry-pattern/ofuf_2_true-unreach-call.c 11.4  3.83 436953088 87.1 11.7  3.63 454070272 92.6 27.4  11.1  499421184 240   7.64 4.00 246177792 7.78 4.08 280723456
loop-industry-pattern/ofuf_3_true-unreach-call.c 10.2  3.38 392515584 82.4 12.1  3.71 447377408 94.6 26.8  10.9  497770496 224   7.13 3.75 250933248 7.79 4.09 293498880
loop-industry-pattern/ofuf_4_true-unreach-call.c 11.2  3.48 425345024 89.1 12.2  3.69 467537920 102   27.3  11.1  495038464 244   7.72 4.03 248455168 7.86 4.10 278405120
loop-industry-pattern/ofuf_5_true-unreach-call.c 10.7  3.46 427274240 90.2 12.2  3.80 459108352 93.4 28.1  11.3  508465152 245   8.98 4.67 240570368 8.78 4.59 276828160
loops/heavy_true-unreach-call.c 33.4  8.81 2857668608 230   901    767    9218666496 6980   114    37.3  6588473344 717   903    453    5300572160 4.67 2.51 181972992
loops/compact_false-unreach-call.c 901    871    1377067008 11700   901    865    4476596224 7120   15.3  4.93 193777664 103   905    453    4878594048 905    453    5071355904
loops/heavy_false-unreach-call.c 902    705    6163136512 10900   901    766    9612910592 8310   219    205    5528576000 2570   903    452    5638438912 903    452    8279117824
loops-crafted-1/Mono1_false-unreach-call1.c 901    883    583094272 12900   901    864    665079808 11300   371    357    10540642304 5830   904    453    3190292480 902    452    1945620480
loops-crafted-1/Mono3_false-unreach-call1.c 901    882    680128512 10100   900    841    697585664 10400   641    622    11136397312 7510   906    456    6314094592 907    457    6270398464
loops-crafted-1/Mono4_false-unreach-call1.c 901    722    1402933248 12700   901    721    1253081088 14000   616    597    9227378688 7570   903    452    2541674496 903    452    2477555712
loops-crafted-1/Mono5_false-unreach-call1.c 901    880    734539776 11300   901    806    745480192 11100   375    357    9613455360 4950   903    452    2167664640 903    453    2960789504
loops-crafted-1/Mono6_false-unreach-call1.c 901    880    611131392 13800   901    812    922800128 9360   376    357    9688690688 4810   907    456    5712556032 904    454    3627823104
loops-crafted-1/nested3_false-unreach-call.c 901    881    585117696 11800   901    878    637853696 12500   217    202    2546950144 2580   903    452    3938463744 902    452    6153895936
loops-crafted-1/nested5_false-unreach-call.c 901    884    583974912 12100   901    880    787275776 10100   216    202    2016780288 2670   903    452    7033860096 903    452    11462303744
loops-crafted-1/Mono1_true-unreach-call1.c 901    882    581513216 11200   900    865    668221440 11300   274    220    10551713792 3120   904    452    2991415296 902    453    2296348672
loops-crafted-1/nested3_true-unreach-call.c 901    844    1020817408 10400   900    837    1310945280 10400   52.4  36.0  684269568 517   902    452    3283501056 5.22 2.77 177369088
loops-crafted-1/nested5_true-unreach-call.c 25.8  19.5  431742976 307   18.4  11.2  498339840 210   28.1  20.3  476917760 283   5.06 2.67 183062528 6.01 3.17 184496128
loop-invariants/bin-suffix-5_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 14.1  5.30 358744064 106   13.2  5.40 341192704 99.6 12.6  6.56 436551680 104   5.59 2.95 191176704 5.78 3.09 227045376
loop-invariants/const_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 8.66 2.86 378712064 62.0 8.18 2.78 374779904 58.8 13.2  6.49 465199104 123   4.84 2.55 190672896 5.37 2.85 171810816
loop-invariants/eq1_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 7.82 2.71 345120768 69.3 8.34 2.80 368672768 63.6 13.9  7.00 469114880 118   6.13 3.25 227528704 5.21 2.77 173649920
loop-invariants/eq2_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 8.08 2.91 340291584 60.6 7.58 2.87 336576512 54.0 13.6  6.75 465625088 131   5.22 2.79 188936192 6.62 3.52 247832576
loop-invariants/even_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 7.38 2.74 345518080 66.3 8.63 3.24 361435136 64.0 139    65.5  1360805888 1430   5.21 2.77 187944960 5.84 3.11 203776000
loop-invariants/mod4_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 8.42 2.87 376909824 71.1 7.73 2.80 352546816 61.9 141    65.5  1358127104 1610   5.17 2.76 190087168 5.65 3.00 227065856
loop-invariants/odd_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c 9.57 4.77 364707840 94.9 10.7  4.95 395063296 104   139    65.4  1355874304 1490   5.49 2.91 180396032 5.54 2.96 201453568
../programs/benchmarks/ status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage cpuenergy (J) status cputime (s) walltime (s) memUsage status cputime (s) walltime (s) memUsage
total 208 54700   49000   162990620672 672000 208 50900   45700   163322802176 631000 208 37800 33400 306606460928 405000 208 79100 39900 435192549376 208 73300 36800 389011296256
    correct results 144 4080   2760   75703824384 44700 150 3980   2580   77301624832 42700 182 17700 13700 238761373696 191000 114 1600 830 36758511616 126 4240 2150 60678520832
        correct true 109 2410   1390   59426197504 24700 116 2810   1680   61494747136 29800 125 10200 6940 120378040320 104000 78 1220 624 26400706560 89 3660 1850 45142458368
        correct false 35 1670   1380   16277626880 20000 34 1160   897   15806877696 13000 57 7430 6730 118383333376 86700 36 385 206 10357805056 37 579 296 15536062464
    incorrect results 1 39.6 25.8 862752768 344 1 44.0 26.1 912191488 357 0 0 0
        incorrect true 1 39.6 25.8 862752768 344 1 44.0 26.1 912191488 357 0 0 0
        incorrect false 0 0 0 0 0
score (208 tasks, max score: 357) 221 234 307 192 215
Run set uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Loops utaipan.sv-comp19_prop-reachsafety.ReachSafety-Loops veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops pdr-inv.kInduction-kipdr.ReachSafety-Loops pdr-inv.kInduction-dfkipdr.ReachSafety-Loops