Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; 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-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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) 0 wit inspect 16   3.5 120 730 .40   .84  unknown 20    11    190   690 timeout (false(unreach-call)) 93   51   1400 1100 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 0 wit inspect 36   7.0 230 1300 1.3    0     true 8.0  4.2  100   380 true 11   6.0 140 420 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 960   310   9100 4600 1.9    0     error (invalid witness file) .53 .34 4.8 40 error (invalid witness file) 6.1 3.2 84 300 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 10   2.3 76 490 .17   .020 false(unreach-call) 11    5.7  160   470 false(unreach-call) 28   15   600 570 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 14   3.1 100 610 .0041 0     - - true 20    10    190 640 true 95   52   1200 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 50   9.3 300 1700 .078  0     - - out of memory 470    450    8900 7000 true 81   44   1000 960
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.8 2.1 68 490 0      0     - - true 14    7.0  240 480 true 80   43   790 880
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   2.5 72 510 0      0     - - true 17    8.9  210 520 true 88   47   1600 990
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.7 1.5 42 280 .0041 0     - - true 8.1  4.3  92 290 true 21   11   390 590
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.9 1.9 56 430 0      0     - - true 7.9  4.2  170 320 true 24   13   480 590
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 28   5.0 170 1000 .20   0     false(unreach-call) 7.4  4.0  150   300 false(unreach-call) 12   6.1 210 470 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 29   5.2 190 950 .20   0     false(unreach-call) 7.0  3.7  110   300 false(unreach-call) 12   6.2 180 470 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 30   5.7 210 1000 .38   0     false(unreach-call) 7.2  3.9  93   300 false(unreach-call) 12   6.4 190 500 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 24   4.6 160 1000 .20   .020 false(unreach-call) 7.2  3.8  97   310 false(unreach-call) 13   6.8 220 500 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 7.1 1.7 49 380 .0082 0     false(unreach-call) 6.2  3.3  90   300 false(unreach-call) 10   5.4 160 370 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 100   28   830 2900 .52   0     false(unreach-call) 8.6  4.5  99   330 false(unreach-call) 16   8.2 270 570 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 84   21   680 2500 .55   0     false(unreach-call) 9.1  4.8  180   310 false(unreach-call) 14   7.4 250 550 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 50   11   380 1700 .28   0     false(unreach-call) 7.1  3.8  110   300 false(unreach-call) 12   6.5 220 530 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 9.7 2.1 62 490 .0082 .020 false(unreach-call) 6.5  3.5  100   290 false(unreach-call) 15   7.6 220 420 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 18   3.4 110 680 .049  .020 false(unreach-call) 7.4  3.9  160   310 false(unreach-call) 12   6.6 190 510 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 19   3.5 110 730 .049  .020 false(unreach-call) 8.0  4.2  140   320 false(unreach-call) 13   6.6 240 510 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 6.8 1.6 52 410 .0041 0     false(unreach-call) 5.4  2.9  64   290 false(unreach-call) 9.6 5.1 180 330 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 1 wit inspect 23   4.5 140 850 0      0     - - unknown 12    6.2  250 470 false(unreach-call) 13   6.9 220 380
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 1 wit inspect 20   3.9 130 770 0      0     - - unknown 15    7.6  230 460 false(unreach-call) 13   6.7 240 370
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 1 wit inspect 28   5.1 180 920 0      0     - - unknown 15    7.6  260 480 false(unreach-call) 13   6.6 240 380
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 1 wit inspect 24   4.6 140 930 0      0     - - unknown 14    7.3  190 470 false(unreach-call) 15   7.9 140 360
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 1 wit inspect 42   8.7 310 1600 0      0     - - timeout 910    890    12000 5400 false(unreach-call) 79   53   790 3200
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.3 34 280 .0041 0     - - true 9.7  5.2  93 310 true 11   5.7 200 360
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.2 1.1 28 270 .0041 0     - - true 5.1  2.8  90 280 true 9.4 5.0 180 320
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 1 wit inspect 22   4.2 140 830 0      0     - - timeout 910    890    19000 5100 false(unreach-call) 63   42   890 2800
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 2 wit inspect 150   44   1200 4500 .053  0     - - timeout 910    900    17000 5000 true 57   30   1000 1100
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 2 wit inspect 100   26   760 4000 .053  0     - - timeout 910    890    16000 5100 true 58   31   930 1100
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c segmentation fault 0 wit inspect 48   9.6 330 1700 0      .012 - - error (invalid witness file) .53 .34 11 39 error (invalid witness file) 6.4 3.4 110 310
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 2 wit inspect 190   57   1600 4600 .053  0     - - timeout 900    890    18000 4900 true 60   32   790 1100
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 1 wit inspect 43   9.0 290 1800 0      0     - - timeout 910    890    19000 5100 false(unreach-call) 67   46   1100 3200
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 960   310   4600 4600 .033  .041 error (invalid witness file) .54 .35 8.6 39 error (invalid witness file) 6.1 3.3 120 300 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 960   310   5200 5100 .033  0     error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.9 3.1 110 300 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 1.5 42 320 0      0     - - true 6.4  3.5  130 300 false(unreach-call) 9.8 5.3 120 330
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.1 1.5 39 390 0      0     - - true 8.2  4.4  92 300 false(unreach-call) 8.3 4.5 160 330
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.0 1.7 45 400 0      0     - - true 6.5  3.5  110 300 false(unreach-call) 8.9 4.7 160 320
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.2 1.5 42 360 0      0     - - true 8.9  4.8  90 310 false(unreach-call) 7.8 4.2 130 310
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.8 1.7 47 440 0      0     - - true 9.1  4.9  91 300 false(unreach-call) 7.9 4.3 130 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.4 1.6 49 370 0      0     - - true 9.1  4.9  99 310 false(unreach-call) 9.8 5.3 150 330
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 1.3 32 280 .0041 0     - - true 4.6  2.6  110 280 true 10   5.4 200 350
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.6 1.4 43 290 .0041 0     - - true 5.9  3.2  83 290 true 12   6.3 180 420
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 1.5 47 320 0      0     - - true 6.9  3.7  74 290 false(unreach-call) 8.3 4.5 140 320
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.7 1.4 36 330 0      0     - - true 5.7  3.1  98 300 false(unreach-call) 8.3 4.4 150 320
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 6.3 1.6 44 350 0      0     - - true 6.1  3.3  120 300 false(unreach-call) 7.6 4.1 140 320
ntdrivers/cdaudio_false-unreach-call.i.cil.c segmentation fault 0 wit inspect 690   210   5900 5500 0      0     error (invalid witness file) .52 .35 4.1 40 error (invalid witness file) 7.2 3.8 140 320 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c timeout 0 wit inspect 960   840   13000 3600 7.6    .51  unknown 64    51    660   1900 false(unreach-call) 27   14   510 610 - -
ntdrivers/floppy_false-unreach-call.i.cil.c timeout 0 wit inspect 960   370   9300 6800 14      0     error (invalid witness file) .53 .33 12   40 error (invalid witness file) 7.0 3.7 100 310 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 wit inspect 290   180   3400 4700 2.7    .029 false(unreach-call) 17    9.5  210   600 timeout 97   69   890 1100 - -
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 530   140   4500 6600 8.1    0     true 12    6.1  160   340 true 27   15   450 700 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 15   4.9 110 730 .0041 0     - - true 52    33    720 1100 true 160   96   2000 2400
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 77   18   570 3000 .090  0     - - out of memory 850    830    12000 7000 true 100   61   2400 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c true 1 wit inspect 590   320   6100 5800 .24   0     - - out of memory 270    240    5300 7000 out of memory 180   110   3200 7000
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 910   280   6300 7400 0      0     - - out of memory 540    520    9100 7000 out of memory 210   130   1700 7000
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 wit inspect 960   240   7300 9600 0      0     - - out of memory 600    470    12000 7000 error 25   13   290 360
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c out of memory 0 wit inspect 280   84   1900 15000 .63   0     error (invalid witness file) .57 .41 8.2 40 error (invalid witness file) 6.2 3.3 110 300 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c out of memory 0 wit inspect 190   58   1700 15000 .53   .041 error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.3 3.4 120 300 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c out of memory 0 wit inspect 230   70   1500 15000 .57   0     error (invalid witness file) .50 .34 4.6 39 error (invalid witness file) 6.4 3.3 93 300 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c out of memory 0 wit inspect 220   67   1700 15000 .57   0     error (invalid witness file) .49 .34 5.1 41 error (invalid witness file) 6.4 3.4 110 310 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c out of memory 0 wit inspect 240   75   1700 15000 .42   10     error (invalid witness file) .53 .34 10   39 error (invalid witness file) 6.0 3.2 100 300 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c out of memory 0 wit inspect 240   72   1900 15000 .41   .041 error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.3 3.3 130 300 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c out of memory 0 wit inspect 230   72   1700 15000 .42   10     error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.1 3.2 99 300 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c out of memory 0 wit inspect 230   72   1800 15000 .41   10     error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.4 3.4 120 290 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c out of memory 0 wit inspect 500   160   3500 15000 .59   0     error (invalid witness file) .48 .30 6.7 40 error (invalid witness file) 6.3 3.3 120 300 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c out of memory 0 wit inspect 390   120   2500 15000 .57   .041 error (invalid witness file) .52 .33 10   39 error (invalid witness file) 6.5 3.4 130 300 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 960   310   5100 4300 .95   0     error (invalid witness file) .50 .32 8.4 40 error (invalid witness file) 6.5 3.4 110 310 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c out of memory 0 wit inspect 390   120   2600 15000 .57   .020 error (invalid witness file) .50 .32 7.2 39 error (invalid witness file) 5.9 3.2 110 310 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 960   310   5700 10000 .87   0     error (invalid witness file) .54 .36 11   40 error (invalid witness file) 6.0 3.2 100 300 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c out of memory 0 wit inspect 340   110   2900 15000 .52   10     error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.2 3.3 130 300 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c out of memory 0 wit inspect 480   150   3000 15000 .53   0     error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.0 3.2 120 290 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c out of memory 0 wit inspect 380   120   3100 15000 .57   10     error (invalid witness file) .53 .33 8.9 43 error (invalid witness file) 6.6 3.5 140 310 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c out of memory 0 wit inspect 470   150   3000 15000 .54   9.9   error (invalid witness file) .56 .36 9.1 40 error (invalid witness file) 6.4 3.4 140 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 960   310   5600 4000 .99   0     error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.0 3.2 110 290 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c out of memory 0 wit inspect 510   160   3100 15000 .57   0     error (invalid witness file) .49 .34 9.1 39 error (invalid witness file) 6.6 3.4 130 310 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 2 wit inspect 33   6.5 200 1100 .18   8.8   - - true 260    240    3500 2100 timeout 960   880   18000 3100
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 2 wit inspect 35   6.7 220 1200 .18   0     - - true 210    200    4500 2200 timeout 960   890   15000 3900
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 2 wit inspect 34   6.4 220 1100 .18   0     - - true 200    190    4800 2100 timeout 960   910   25000 3800
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 2 wit inspect 34   6.7 230 1300 .18   0     - - true 220    200    4300 2100 timeout 960   870   17000 3300
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 77   19   530 2500 .10   0     - - timeout 910    890    14000 4800 timeout 960   810   16000 5400
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 24   4.4 150 770 .094  0     - - timeout 910    890    23000 4900 timeout 960   820   18000 5500
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c segmentation fault 0 wit inspect 170   49   1400 4500 0      .012 - - error (invalid witness file) .49 .31 11 43 error (invalid witness file) 5.7 3.1 110 290
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 1 wit inspect 130   35   1200 4100 .10   0     - - timeout 910    890    16000 4500 timeout 960   860   24000 5100
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 1 wit inspect 97   24   610 2700 .13   0     - - timeout 910    890    16000 4800 timeout 960   820   18000 5800
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 1 wit inspect 110   28   840 3500 .10   .020 - - timeout 910    890    18000 4700 timeout 960   870   18000 5200
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 1 wit inspect 79   19   620 2700 .11   0     - - timeout 910    890    18000 4800 timeout 960   820   12000 6300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 1 wit inspect 130   34   940 4000 .10   .82  - - timeout 910    890    23000 4900 timeout 960   810   21000 6400
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 1 wit inspect 110   28   810 4200 .057  0     - - timeout 910    890    25000 4800 out of memory 650   520   14000 7000
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 1 wit inspect 45   8.9 270 1700 .10   0     - - timeout 910    890    17000 4600 timeout 960   810   18000 6200
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 1 wit inspect 270   82   2300 4900 0      0     - - timeout 910    890    22000 4900 out of memory 690   580   9800 7000
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 1 wit inspect 52   10   320 1700 .15   .020 - - timeout 910    890    19000 4900 timeout 960   800   18000 6500
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 1 wit inspect 290   87   2200 5000 0      0     - - timeout 910    890    16000 4600 out of memory 760   620   14000 7000
../../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 89 20000 6900 150000 420000 53   72    94 230 140 3100 9100   94 580 330 9300 17000   94 20000 20000 400000 140000   94 16000 14000 300000 130000  
    correct results 41 69 1300 310 9400 44000 3.7 8.9  13 98 52 1500 4100   13 180 94 3100 6300   23 5100 4900 92000 45000   24 4800 4100 89000 31000  
        correct true 28 56 850 220 6300 30000 1.1 8.8  0 0 0 0 0   0 0 0 0 0   23 5100 4900 92000 45000   15 4800 4100 89000 31000  
        correct false 13 13 420 95 3100 14000 2.6 .10 13 98 52 1500 4100   13 180 94 3100 6300   0 0 0 0 0   9 0 0 0 0  
    correct-unconfimed results 23 20 2800 890 23000 60000 11   1.7  2 40 21 450 1400   2 130 72 2000 2200   0 14000 14000 280000 82000   7 11000 9400 210000 91000  
        correct-unconfirmed true 20 20 2200 740 18000 51000 1.3 .86 2 0 0 0 0   2 0 0 0 0   0 14000 14000 280000 82000   0 11000 9400 210000 91000  
        correct-unconfirmed false 3 0 590 150 4900 8600 9.8 .84 0 40 21 450 1400   0 130 72 2000 2200   0 0 0 0 0   7 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (94 tasks, max score: 146) 89
Run set sv-comp17.ReachSafety-ControlFlow