Tool CPAchecker 1.6.1-svn 23987
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 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.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 12   3.2 94 540 .029 0      true 21    12    220   760 false(unreach-call) 15   8.1 220 510 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 16   4.5 130 740 .041 0      true 11    5.8  140   450 false(unreach-call) 19   10   300 520 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 19   5.3 150 720 .041 0      true 13    7.4  140   560 false(unreach-call) 20   10   310 530 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 0 wit inspect 9.7 2.8 74 510 .029 0      true 9.6  5.2  200   440 true 12   6.5 200 410 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 25   8.1 190 1400 0     0      - - true 21    11    240   660 true 95   52   1400 1200
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 19   5.0 140 730 0     0      - - out of memory 390    380    10000   7000 true 77   42   1400 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 15   4.1 110 720 0     0      - - true 12    6.5  140   480 true 74   40   1200 930
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c witness invalid (true) 0 wit inspect 18   4.8 130 760 0     0      - - error (invalid witness file) .68 .41 8.2 41 error (invalid witness file) 6.4 3.4 120 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.6 2.0 47 360 0     0      - - true 8.0  4.3  77   290 true 22   12   410 540
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.0 2.4 60 450 0     0      - - true 8.8  4.6  140   330 true 23   12   430 570
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 9.5 2.7 77 480 .037 0      true 7.1  3.8  160   290 false(unreach-call) 12   6.3 260 450 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.5 2.7 79 480 .037 0      true 6.9  3.6  120   290 false(unreach-call) 12   6.5 230 480 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 10   3.0 82 480 .041 0      true 6.8  3.6  82   290 false(unreach-call) 11   5.9 170 480 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 8.9 2.6 79 470 .041 0      true 6.9  3.7  93   300 false(unreach-call) 12   6.2 170 470 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 54   14   340 2300 .020 0      false(unreach-call) 5.8  3.1  120   290 false(unreach-call) 10   5.5 180 370 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 0 wit inspect 46   13   330 2200 .049 0      true 10    5.4  98   430 true 15   7.7 190 550 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 0 wit inspect 70   22   520 3400 .049 0      true 8.9  4.7  100   390 true 13   6.9 200 540 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 0 wit inspect 27   6.8 200 1000 .033 .0041 true 8.7  4.6  190   370 true 13   6.7 200 470 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 68   22   490 3400 .025 2.8    true 10    5.5  190   430 false(unreach-call) 12   6.5 210 420 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 6.5 2.0 57 350 .037 0      true 7.3  3.9  110   300 false(unreach-call) 12   6.5 220 480 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 6.6 2.1 58 330 .037 0      true 7.3  3.9  86   320 false(unreach-call) 12   6.5 250 480 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 4.3 1.6 35 290 .016 0      false(unreach-call) 5.2  2.8  100   290 false(unreach-call) 9.6 5.1 140 330 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 33   8.3 220 1300 0     0      - - true 15    8.7  220   550 true 51   28   640 1700
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 36   8.6 260 1500 0     0      - - true 16    9.2  220   540 true 56   30   660 1600
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 35   8.6 240 1500 0     0      - - true 20    11    210   550 true 51   28   570 1400
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 39   9.3 270 1500 0     .0041 - - true 14    8.1  220   540 true 68   36   780 1500
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 2 wit inspect 60   15   420 2300 0     0      - - out of memory 730    720    13000   7000 true 64   34   700 2000
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.6 35 290 0     0      - - true 9.7  5.2  120   300 true 11   6.1 230 360
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.4 1.3 26 290 0     0      - - true 4.8  2.7  110   280 true 11   5.6 130 320
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 2 wit inspect 26   6.6 190 1100 0     0      - - timeout 910    890    15000   4800 true 67   36   760 1300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 2 wit inspect 44   13   330 2000 0     0      - - timeout 910    890    17000   5000 true 54   29   640 1300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 2 wit inspect 25   6.3 210 980 0     0      - - timeout 910    890    16000   4900 true 45   24   500 1000
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 2 wit inspect 320   98   2000 8000 0     0      - - timeout 910    890    27000   5000 true 60   32   810 1700
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 2 wit inspect 43   11   300 1900 0     0      - - timeout 910    890    14000   4600 true 51   28   730 1100
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 2 wit inspect 69   22   480 3200 0     0      - - timeout 910    890    24000   5300 true 62   33   530 1200
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 0 wit inspect 4.3 1.6 41 300 .020 0      true 4.6  2.5  58   280 true 11   5.8 180 350 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 0 wit inspect 4.3 1.6 34 300 .020 .025  true 4.8  2.7  96   280 true 11   5.6 200 360 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 1.3 26 270 0     0      - - true 6.4  3.5  93   290 true 22   11   370 810
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 1.3 26 270 0     0      - - true 7.6  4.1  76   300 true 26   14   370 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.2 1.3 28 270 0     0      - - true 6.3  3.4  120   290 true 37   21   740 2500
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 1.3 27 270 0     0      - - true 7.5  4.1  100   300 true 50   30   660 3700
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.1 1.3 27 270 0     0      - - true 6.7  3.6  110   300 true 75   48   1000 6200
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 1.3 27 270 0     0      - - true 7.3  4.0  140   300 out of memory 120   76   2500 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 2.8 1.2 24 270 0     0      - - true 5.3  2.9  91   290 true 12   6.5 130 360
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 2.8 1.2 26 270 0     0      - - true 6.0  3.3  74   290 true 11   5.9 160 370
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 2.9 1.2 26 270 0     0      - - true 5.9  3.3  89   290 true 14   7.2 240 420
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 2.9 1.3 28 270 0     0      - - true 6.7  3.7  77   290 true 20   11   140 560
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 1.3 26 270 0     0      - - true 7.5  4.1  79   290 true 20   11   240 600
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   620   8900 8000 0     0      error (invalid witness file) .54 .35 5.5 41 error (invalid witness file) 7.0 3.7 150 320 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16   4.1 130 650 .16  0      timeout 96    82    1300   3300 true 14   7.3 230 470 - -
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 25   6.4 210 940 .14  0      true 44    30    1000   1600 true 24   13   420 590 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 12   3.3 98 500 .13  0      true 14    7.6  250   440 true 12   6.5 160 430 - -
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 29   7.8 210 960 .16  0      timeout 97    69    1200   4100 timeout 97   65   1400 990 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 37   9.8 270 1600 0     0      - - true 48    30    640   1100 true 150   94   1900 2300
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 21   5.5 160 920 0     0      - - timeout 910    890    19000   6700 true 100   62   1700 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c true 1 wit inspect 59   17   460 2300 0     .0041 - - out of memory 300    280    5800   7000 false(unreach-call) 130   76   2100 4400
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c true 1 wit inspect 24   6.1 200 890 0     0      - - out of memory 450    430    11000   7000 out of memory 160   100   2800 7000
ntdrivers/parport_true-unreach-call.i.cil.c true 2 wit inspect 44   12   320 1700 0     0      - - out of memory 560    460    9000   7000 true 200   140   2400 4300
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10   2.9 79 490 .10  0      true 7.5  4.0  84   300 true 10   5.4 170 330 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 9.8 2.9 88 480 .10  0      true 8.1  4.3  180   300 true 12   6.2 200 360 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10   2.9 75 500 .11  0      true 8.6  4.6  110   310 true 13   7.0 120 350 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 11   3.1 86 500 .11  0      true 8.5  4.5  160   310 true 9.8 5.2 170 340 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.4 2.4 60 390 .074 0      false(unreach-call) 11    6.4  88   500 true 11   5.9 200 380 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.2 2.3 61 390 .074 0      false(unreach-call) 13    7.5  120   520 true 12   6.4 150 360 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.7 2.4 60 390 .074 0      false(unreach-call) 11    6.2  92   500 true 10   5.6 240 350 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.3 2.3 60 390 .074 0      false(unreach-call) 11    6.3  150   500 true 10   5.5 210 340 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6 2.2 51 350 .061 .0041 false(unreach-call) 8.8  4.8  160   340 true 10   5.5 190 360 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 8.8 2.8 64 470 .082 0      false(unreach-call) 13    7.4  100   530 true 10   5.5 180 350 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.3 2.1 53 340 .061 0      false(unreach-call) 8.2  4.4  110   330 true 10   5.5 180 350 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 8.5 2.7 67 360 .082 8.1    false(unreach-call) 14    7.6  140   530 true 11   6.0 200 360 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6 2.1 54 340 .061 .0082 false(unreach-call) 9.1  4.9  100   340 true 10   5.4 170 360 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 8.7 2.7 71 470 .082 0      timeout 94    76    1800   2000 true 11   5.7 220 360 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6 2.2 53 340 .061 0      false(unreach-call) 8.8  4.8  150   330 true 9.5 5.2 170 350 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 8.4 2.5 65 480 .082 0      false(unreach-call) 14    7.9  260   530 true 10   5.4 160 360 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.4 2.1 49 350 .061 0      false(unreach-call) 10    5.5  100   330 true 10   5.6 150 350 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.4 2.2 53 350 .061 0      false(unreach-call) 8.3  4.4  75   340 true 10   5.6 200 370 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6 2.1 53 340 .061 0      false(unreach-call) 9.0  4.9  150   340 true 11   5.7 180 360 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 11   3.1 83 500 .11  2.3    - - true 8.6  4.6  110   310 true 10   5.6 120 350
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 10   2.9 88 490 .11  0      - - true 8.2  4.3  150   310 true 9.9 5.3 190 350
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 11   3.1 77 490 .11  0      - - true 10    5.3  97   300 true 12   6.3 160 350
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 11   3.2 86 490 .11  .025  - - true 10    5.4  92   300 true 11   5.6 170 350
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.6 3.0 78 490 .090 0      - - false(unreach-call) 18    10    250   580 true 10   5.5 190 350
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 8.0 2.4 62 430 .082 0      - - false(unreach-call) 17    9.5  170   530 true 11   6.0 230 370
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 18   5.3 140 740 .21  0      - - true 120    100    2200   2700 true 11   5.7 220 380
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.6 2.8 82 490 .090 0      - - false(unreach-call) 19    11    260   560 true 10   5.6 190 350
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 12   3.5 93 540 .13  0      - - false(unreach-call) 28    17    350   720 true 12   6.6 150 380
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.9 3.0 80 500 .090 0      - - false(unreach-call) 17    9.6  300   580 true 11   5.7 160 360
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 10   3.1 89 510 .11  0      - - false(unreach-call) 30    18    360   980 true 11   5.7 200 360
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.5 2.8 72 480 .090 0      - - false(unreach-call) 15    8.6  230   580 true 9.8 5.3 180 350
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 12   3.4 93 550 .14  0      - - true 110    89    2000   2400 true 13   6.7 210 370
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.1 2.7 81 480 .090 0      - - false(unreach-call) 18    10    220   580 true 10   5.6 220 350
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 14   4.0 110 590 .16  0      - - true 100    84    2400   2300 true 12   6.4 170 370
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 14   3.9 110 560 .16  0      - - false(unreach-call) 35    21    440   920 true 11   5.8 200 360
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 15   4.3 120 690 .18  0      - - true 130    110    2100   2600 true 11   6.1 180 370
../../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 -180 2800 1200 23000 87000 4.7 13      94 690 450 10000 25000   94 590 330 9600 18000   94 9700 9200 200000 98000   94 2300 1300 33000 70000  
    correct results 58 90 1300 370 9100 53000 1.4 11      26 260 140 3400 11000   26 300 160 5200 11000   22 8300 7900 170000 66000   31 1800 1000 25000 52000  
        correct true 32 64 940 270 6600 37000 0   .0041 10 0 0 0 0   14 0 0 0 0   22 8300 7900 170000 66000   31 1800 1000 25000 52000  
        correct false 26 26 330 98 2500 16000 1.4 11      16 260 140 3400 11000   12 300 160 5200 11000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 17 2 380 110 2900 16000 1.3 .033  12 420 310 6800 15000   14 280 160 4300 6900   0 760 710 17000 14000   1 290 180 4900 11000  
        correct-unconfirmed true 2 2 83 23 660 3200 0   .0041 12 0 0 0 0   14 0 0 0 0   0 760 710 17000 14000   0 290 180 4900 11000  
        correct-unconfirmed false 15 0 290 85 2200 13000 1.3 .029  0 420 310 6800 15000   0 280 160 4300 6900   0 0 0 0 0   1 0 0 0 0  
    incorrect results 17 -272 190 56 1500 9000 2.1 2.3    0 0 0 0 0   0 0 0 0 0   17 700 520 12000 17000   17 190 100 3100 6100  
        incorrect true 0
        incorrect false 17 -272 190 56 1500 9000 2.1 2.3    0 0 0 0 0   0 0 0 0 0   9 700 520 12000 17000   0 190 100 3100 6100  
score (94 tasks, max score: 146) -180
Run set sv-comp17.ReachSafety-ControlFlow