Tool ULTIMATE Automizer f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 55   15   440 1100 2.6 0   false(unreach-call) 8.4  4.4  96   310 false(unreach-call) 14   7.6 200 550 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 31   8.0 260 920 2.7 0   error (invalid witness file) 5.2  2.8  62   220 false(unreach-call) 14   7.4 240 480 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 46   12   330 1000 2.7 0   error (invalid witness file) 5.8  3.1  61   220 false(unreach-call) 13   7.1 180 520 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 17   4.3 130 530 2.6 0   error (invalid witness file) 4.0  2.2  45   260 false(unreach-call) 12   6.5 180 460 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 95   41   820 2000 3.3 0   - - true 19    10    380   660 true 97   53   940 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 63   24   610 1400 2.9 0   - - out of memory 370    360    10000   7000 true 69   38   670 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 65   27   680 1600 2.9 0   - - true 15    8.0  180   470 true 67   36   560 910
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 70   27   680 1600 3.1 0   - - true 16    8.4  300   520 true 74   40   800 1000
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 18   5.2 150 540 2.7 0   - - true 8.4  4.4  110   290 true 22   12   230 560
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 16   4.7 130 670 2.8 0   - - true 9.2  4.8  150   360 true 21   11   310 580
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 14   3.7 110 510 2.8 0   true 9.2  4.8  120   340 false(unreach-call) 12   6.2 140 470 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   3.9 110 570 2.8 0   true 6.6  3.5  74   290 false(unreach-call) 12   6.2 190 460 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 14   3.9 110 530 2.8 0   true 7.9  4.1  120   310 false(unreach-call) 12   6.5 180 520 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 14   3.8 99 530 2.8 0   true 8.1  4.3  120   320 false(unreach-call) 12   6.2 260 470 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 11   3.0 88 510 2.6 0   true 7.8  4.1  120   290 false(unreach-call) 10   5.6 170 390 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 34   9.0 290 1200 2.9 0   true 13    6.5  88   410 false(unreach-call) 15   8.0 230 580 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 26   6.9 230 870 2.8 0   true 11    5.8  99   470 false(unreach-call) 15   7.6 240 560 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 20   5.2 150 730 2.7 0   true 13    6.7  160   450 false(unreach-call) 14   7.2 210 530 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 18   4.8 150 750 2.7 0   true 7.4  3.9  90   290 false(unreach-call) 12   6.2 180 450 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 15   4.1 120 650 2.8 0   true 9.0  4.7  140   320 false(unreach-call) 12   6.5 160 500 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 16   4.3 130 640 2.8 0   true 8.3  4.4  86   310 false(unreach-call) 13   6.6 210 510 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 6.7 2.1 52 330 2.6 0   false(unreach-call) 7.0  3.7  64   290 false(unreach-call) 9.7 5.1 140 360 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 49   17   450 2600 2.7 0   - - true 16    9.1  260   540 true 51   28   450 1600
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 46   14   380 2300 2.7 0   - - true 16    8.8  280   540 true 61   33   850 1700
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 47   14   370 1900 2.7 0   - - true 18    9.8  180   560 true 55   30   440 1700
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 48   14   440 2100 2.7 0   - - true 18    9.9  240   540 true 62   33   530 1400
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 2 wit inspect 46   16   400 2100 2.7 0   - - out of memory 780    760    20000   7000 true 51   28   530 1800
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.6 2.5 73 440 2.6 0   - - true 10    5.5  130   320 true 23   13   350 550
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.2 56 330 2.5 0   - - true 5.2  2.8  96   290 true 11   6.0 200 360
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 2 wit inspect 49   17   490 1900 2.7 0   - - timeout 910    890    19000   5100 true 52   28   510 1400
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 2 wit inspect 41   15   400 1800 2.7 0   - - timeout 910    890    18000   5100 true 53   29   480 1100
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 2 wit inspect 42   14   370 1600 2.7 0   - - timeout 910    890    22000   5100 true 49   26   670 1100
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 2 wit inspect 61   25   570 2400 2.7 0   - - timeout 910    890    14000   4700 true 58   31   470 1500
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 2 wit inspect 54   20   470 2200 2.7 0   - - timeout 910    890    20000   4800 true 57   30   530 1100
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 2 wit inspect 43   17   410 1700 2.7 0   - - timeout 910    890    18000   5100 true 57   30   720 1200
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.9 2.2 56 340 2.6 0   true 4.8  2.6  48   270 false(unreach-call) 10   5.3 150 360 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 7.1 2.2 55 350 2.6 0   true 4.3  2.4  47   280 false(unreach-call) 11   5.8 170 350 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 19   5.4 150 930 2.6 0   - - true 7.5  4.0  80   300 true 22   12   300 840
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 27   8.8 210 1500 2.6 0   - - true 7.4  4.0  110   300 true 27   14   370 1200
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 36   15   300 2900 2.6 0   - - true 7.8  4.2  91   300 true 31   18   460 2000
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 61   28   450 5200 2.6 0   - - true 7.7  4.1  120   300 true 41   25   570 3900
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 140   59   940 6400 2.6 0   - - true 6.8  3.7  120   310 true 82   52   810 6500
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 320   130   2400 8600 2.6 0   - - true 7.4  4.0  130   300 out of memory 95   59   770 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.6 2.3 68 380 2.6 0   - - true 5.3  2.9  68   290 true 11   5.9 200 360
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 2.5 67 440 2.6 0   - - true 6.7  3.6  74   290 true 12   6.3 220 410
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.7 2.7 74 520 2.6 0   - - true 6.6  3.6  83   290 true 14   7.5 220 490
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 11   3.2 91 540 2.6 0   - - true 6.1  3.3  71   290 true 16   8.2 160 630
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 15   4.0 120 780 2.6 0   - - true 6.8  3.7  100   290 true 19   9.9 250 620
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   770   11000 5400 2.3 0   error (invalid witness file) .50 .32 9.2 40 error (invalid witness file) 7.2 3.7 130 310 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 19   4.7 140 610 2.6 0   exception 5.3  2.8  58   230 false(unreach-call) 16   8.7 260 520 - -
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 140   97   1100 4700 2.6 0   exception 7.6  4.0  110   290 timeout 97   74   890 3800 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c timeout 0 wit inspect 900   850   8300 1700 2.3 0   error (invalid witness file) .45 .30 7.4 39 error (invalid witness file) 6.8 3.6 140 320 - -
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 wit inspect 97   45   880 1200 2.5 0   error (invalid witness file) .49 .33 3.7 39 error (invalid witness file) 6.7 3.5 140 300 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 150   76   1700 3500 3.6 0   - - true 53    33    620   1100 true 150   92   1500 2300
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 100   44   1000 2300 3.0 0   - - out of memory 590    570    13000   7000 true 110   63   1400 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c true 1 wit inspect 350   210   2900 8200 9.2 0   - - out of memory 410    380    11000   7000 out of memory 210   140   1900 7000
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c true 1 wit inspect 280   150   2900 8500 3.5 0   - - out of memory 550    530    10000   7000 out of memory 160   110   2400 7000
ntdrivers/parport_true-unreach-call.i.cil.c true 2 wit inspect 220   140   2400 4800 5.1 0   - - out of memory 500    410    8800   7000 true 210   150   2800 4800
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c timeout 0 wit inspect 900   850   12000 2400 2.5 0   error (invalid witness file) .54 .35 8.0 40 error (invalid witness file) 6.5 3.5 130 300 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 97   66   940 820 2.6 0   true 7.8  4.1  110   290 false(unreach-call) 37   21   630 580 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 93   64   850 800 2.6 0   true 6.3  3.4  68   300 false(unreach-call) 33   19   360 570 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 140   110   1700 830 2.6 0   true 7.3  3.9  92   290 false(unreach-call) 33   19   310 570 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 29   10   220 550 2.6 0   error (invalid witness file) 5.5  2.9  42   220 false(unreach-call) 30   17   420 540 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 27   9.2 230 520 2.7 0   true 8.4  4.5  150   300 false(unreach-call) 33   18   500 550 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 27   9.2 220 530 2.7 0   true 8.0  4.3  88   300 false(unreach-call) 31   17   360 530 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 27   9.3 200 520 2.7 0   true 9.1  4.9  170   300 false(unreach-call) 31   17   290 530 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   12000 4900 2.3 0   error (invalid witness file) .63 .40 8.4 40 error (invalid witness file) 6.6 3.5 120 300 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   12000 5000 2.5 0   error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.5 3.4 110 300 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 900   770   11000 3800 2.3 0   error (invalid witness file) .55 .35 7.8 40 error (invalid witness file) 5.9 3.1 100 290 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   10000 4900 2.5 0   error (invalid witness file) .50 .32 9.2 40 error (invalid witness file) 6.6 3.5 130 300 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 900   770   12000 3900 2.3 0   error (invalid witness file) .53 .34 12   42 error (invalid witness file) 7.1 3.7 110 330 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 59   37   510 720 2.7 0   true 11    5.8  90   300 false(unreach-call) 54   40   450 670 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   12000 4800 2.3 0   error (invalid witness file) .52 .35 12   40 error (invalid witness file) 5.8 3.1 89 290 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 5200 2.5 0   error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.7 3.5 130 320 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   14000 4500 2.3 0   error (invalid witness file) .61 .39 9.8 41 error (invalid witness file) 6.2 3.3 130 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900   770   14000 3800 2.3 0   error (invalid witness file) .62 .40 4.9 40 error (invalid witness file) 6.4 3.4 110 300 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   11000 5000 2.3 0   error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.3 3.4 130 300 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   820   11000 2500 2.5 0   - - error (invalid witness file) .56 .36 9.3 39 error (invalid witness file) 6.0 3.2 100 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   820   12000 2300 2.5 0   - - error (invalid witness file) .53 .35 9.4 40 error (invalid witness file) 6.3 3.3 110 310
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900   840   12000 2400 2.3 0   - - error (invalid witness file) .69 .42 8.1 40 error (invalid witness file) 6.4 3.3 120 300
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c timeout 0 wit inspect 900   840   12000 2700 2.5 0   - - error (invalid witness file) .66 .42 7.1 39 error (invalid witness file) 6.0 3.2 120 290
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   10000 5400 2.3 0   - - error (invalid witness file) .52 .34 8.7 39 error (invalid witness file) 6.1 3.2 97 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   10000 4100 2.3 0   - - error (invalid witness file) .56 .36 9.2 39 error (invalid witness file) 6.0 3.2 72 310
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900   780   12000 5500 2.3 0   - - error (invalid witness file) .57 .36 8.0 39 error (invalid witness file) 6.0 3.2 110 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   10000 5200 2.3 0   - - error (invalid witness file) .61 .38 6.6 39 error (invalid witness file) 6.2 3.3 110 300
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 5300 2.3 0   - - error (invalid witness file) .58 .38 8.1 39 error (invalid witness file) 6.3 3.3 120 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   12000 4900 2.3 0   - - error (invalid witness file) .53 .33 8.5 40 error (invalid witness file) 6.7 3.5 100 310
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   13000 4900 2.3 0   - - error (invalid witness file) .62 .39 8.3 39 error (invalid witness file) 6.5 3.5 130 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 4800 2.3 0   - - error (invalid witness file) .55 .36 11   39 error (invalid witness file) 6.2 3.3 91 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900   780   12000 5100 2.3 0   - - error (invalid witness file) .64 .42 8.0 41 error (invalid witness file) 6.4 3.3 120 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 4800 2.3 0   - - error (invalid witness file) .69 .43 7.0 39 error (invalid witness file) 6.3 3.3 120 290
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   14000 5300 2.3 0   - - error (invalid witness file) .66 .42 6.6 39 error (invalid witness file) 6.0 3.2 89 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900   780   11000 5200 2.3 0   - - error (invalid witness file) .55 .35 6.1 41 error (invalid witness file) 6.1 3.2 120 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 5200 2.3 0   - - error (invalid witness file) .64 .41 8.1 40 error (invalid witness file) 6.2 3.3 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 94 95 31000 26000 380000 240000 250   0   94 220   120   2800 9000   94 710 420 9600 22000   94 8900 8500 190000 82000   94 2300 1400 26000 73000  
    correct results 60 93 2900 1300 26000 88000 170   0   22 210   110   2500 8200   27 520 290 7000 14000   23 8000 7600 170000 67000   32 1800 1100 20000 54000  
        correct true 33 66 2000 850 18000 70000 93   0   20 0   0   0 0   0 0 0 0 0   23 8000 7600 170000 67000   32 1800 1100 20000 54000  
        correct false 27 27 880 420 7900 18000 72   0   2 210   110   2500 8200   27 520 290 7000 14000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 2 770 450 6900 21000 15   0   0 7.6 4.0 110 290   0 97 74 890 3800   0 960 910 22000 14000   0 380 240 4400 14000  
        correct-unconfirmed true 2 2 620 360 5800 17000 13   0   0 0   0   0 0   0 0 0 0 0   0 960 910 22000 14000   0 380 240 4400 14000  
        correct-unconfirmed false 1 0 140 97 1100 4700 2.6 0   0 7.6 4.0 110 290   0 97 74 890 3800   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (94 tasks, max score: 146) 95
Run set sv-comp17.ReachSafety-ControlFlow