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