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