Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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 1.0  1.0  13   150 .0041 0      false(unreach-call) 8.5  4.5  180 310 false(unreach-call) 14   7.4 260 520 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .27 .26 2.6 31 .0041 0      false(unreach-call) 8.0  4.2  170 310 false(unreach-call) 16   8.4 170 440 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 4.9 53 .0041 0      false(unreach-call) 8.5  4.5  110 320 false(unreach-call) 19   10   350 510 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .20 .19 2.0 25 .0041 0      false(unreach-call) 7.1  3.8  160 320 false(unreach-call) 12   6.2 210 430 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.1  2.1  21   150 .0082 0      - - exception 7.3  3.9  150   290 true 130   70   1500 1200
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 0 wit inspect 850    850    3100   6300 6.1    0      - - error (invalid witness file) .73 .46 7.0 40 error (invalid witness file) 6.1 3.2 120 290
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .45 .44 4.7 31 .0082 .16   - - exception 7.5  4.0  85   290 true 82   44   820 900
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .90 .89 9.6 53 .0082 0      - - exception 8.4  4.4  88   300 true 75   41   750 1100
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .25 .25 2.7 19 .0082 0      - - true 8.3  4.5  81   290 true 26   14   340 560
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .32 .31 3.1 21 .0082 0      - - true 9.4  4.9  120   320 true 24   13   410 580
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 1.4  1.4  16   84 .10   0      true 6.8  3.6  140 290 false(unreach-call) 12   6.3 220 460 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.5  1.4  15   87 .11   0      true 6.5  3.5  99 290 false(unreach-call) 14   7.4 220 460 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 1.7  1.7  19   100 .11   0      true 6.6  3.5  100 310 false(unreach-call) 12   6.6 240 470 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 1.4  1.4  16   87 .10   0      true 6.6  3.5  130 310 false(unreach-call) 14   7.4 150 470 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .16 .15 1.1 20 .0041 0      true 7.1  3.8  130 290 false(unreach-call) 13   7.0 140 380 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 11    11    120   330 .51   0      true 9.0  4.8  100 440 false(unreach-call) 16   8.3 290 570 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.5  2.5  26   140 .13   0      true 9.9  5.2  140 440 false(unreach-call) 18   9.6 160 540 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.3  2.3  30   140 .098  0      true 8.7  4.6  110 420 false(unreach-call) 13   6.6 210 470 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .16 .15 1.2 20 .0041 0      true 7.7  4.1  130 290 false(unreach-call) 18   9.2 200 420 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.2  2.2  24   140 .098  .0041 true 7.4  3.9  140 290 false(unreach-call) 13   6.8 180 490 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.1  2.0  25   120 .098  0      true 7.6  4.0  140 290 false(unreach-call) 12   6.5 230 510 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .18 .17 1.4 20 .0041 0      false(unreach-call) 5.9  3.2  110 290 false(unreach-call) 9.9 5.2 180 360 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 19    19    250   380 2.0    0      - - true 22    12    330   690 true 58   32   600 1700
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 20    20    230   390 1.9    0      - - true 27    14    340   700 true 74   40   1200 1400
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 23    23    230   450 1.9    0      - - true 26    14    290   730 true 67   36   1200 1700
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 19    19    290   390 1.9    0      - - true 24    13    240   680 true 64   35   520 1700
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    4400   1200 7.4    0      - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 7.9 4.1 110 310
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 850    850    4100   1100 12      0      - - error (invalid witness file) .71 .44 9.0 42 error (invalid witness file) 6.1 3.2 110 300
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 850    850    5400   2600 15      0      - - error (invalid witness file) .56 .36 10   40 error (invalid witness file) 6.6 3.5 120 300
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    3700   1200 7.5    .28   - - error (invalid witness file) .61 .39 8.4 41 error (invalid witness file) 7.4 3.8 150 330
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    4600   1200 7.2    0      - - error (invalid witness file) .54 .36 8.1 39 error (invalid witness file) 6.0 3.2 120 300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    3800   1200 7.6    0      - - error (invalid witness file) .65 .42 8.5 41 error (invalid witness file) 6.1 3.2 130 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    4200   1200 8.0    0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.2 3.2 120 300
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    3600   1200 7.7    0      - - error (invalid witness file) .75 .46 9.4 43 error (invalid witness file) 6.5 3.4 92 290
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c error (42) 0 wit inspect 850    850    3700   1200 7.6    0      - - error (invalid witness file) .60 .39 7.8 39 error (invalid witness file) 6.0 3.2 130 290
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .15 .14 1.5 21 .0041 0      true 4.4  2.4  86 280 false(unreach-call) 11   5.9 120 350 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .16 .16 1.6 19 .0041 0      true 4.5  2.5  75 280 false(unreach-call) 9.0 4.8 180 340 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    4800   3300 15      0      - - error (invalid witness file) .60 .37 8.2 39 error (invalid witness file) 5.8 3.1 110 290
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6300   4000 16      0      - - error (invalid witness file) .55 .36 12   44 error (invalid witness file) 6.7 3.5 110 290
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5800   4700 18      .48   - - error (invalid witness file) .73 .47 8.6 45 error (invalid witness file) 5.6 3.0 120 280
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5600   5500 19      11      - - error (invalid witness file) .53 .33 11   39 error (invalid witness file) 5.8 3.1 110 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6200   6100 21      0      - - error (invalid witness file) .46 .30 4.8 39 error (invalid witness file) 6.6 3.5 110 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    8300   6900 22      .0041 - - error (invalid witness file) .66 .42 7.9 40 error (invalid witness file) 5.5 2.9 84 280
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6000   5900 20      0      - - error (invalid witness file) .47 .30 9.5 39 error (invalid witness file) 5.6 3.0 120 290
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6900   8000 23      0      - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.9 3.1 110 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    8800   1800 11      0      - - error (invalid witness file) .59 .36 10   39 error (invalid witness file) 6.3 3.3 130 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    8300   2300 12      0      - - error (invalid witness file) .53 .34 10   40 error (invalid witness file) 6.0 3.1 120 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5200   2800 13      0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.4 3.4 110 310
ntdrivers/cdaudio_false-unreach-call.i.cil.c error (1) 0 wit inspect 2.2  2.2  23   210 .012  0      error (invalid witness file) .51 .33 13 39 error (invalid witness file) 7.0 3.7 140 320 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 1.2  1.2  14   120 .012  0      timeout 96    82    1600 2900 false(unreach-call) 37   20   630 540 - -
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 2.7  2.7  30   150 .012  0      exception 7.1  3.7  110 280 false(unreach-call) 55   32   1200 1200 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16    16    180   180 1.4    0      exception 4.5  2.4  76 210 timeout (true) 95   78   1700 870 - -
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 12    12    140   790 .012  .29   true 12    5.9  200 340 timeout 96   67   990 870 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c error (1) 0 wit inspect 2.1  2.1  24   200 .012  0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.4 3.9 130 320
ntdrivers/diskperf_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4000   4100 4.9    0      - - error (invalid witness file) .49 .32 9.6 40 error (invalid witness file) 6.9 3.6 140 300
ntdrivers/floppy2_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    7000   8400 120      0      - - error (invalid witness file) .56 .36 8.8 41 error (invalid witness file) 8.2 4.3 160 330
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (42) 0 wit inspect 850    850    6800   2900 90      .23   - - error (invalid witness file) .61 .39 12   46 error (invalid witness file) 7.2 3.8 110 300
ntdrivers/parport_true-unreach-call.i.cil.c error (1) 0 wit inspect 51    51    620   1500 .037  0      - - error (invalid witness file) .60 .38 10   42 error (invalid witness file) 7.3 3.8 160 330
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 12    12    170   470 .70   0      true 17    9.3  340 590 false(unreach-call) 53   36   1200 640 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 4.2  4.2  48   210 .19   0      true 36    22    340 1400 false(unreach-call) 38   23   610 580 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 4.2  4.2  50   210 .19   .0041 true 40    24    500 1000 false(unreach-call) 39   23   580 570 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 4.1  4.1  47   210 .19   0      true 36    22    300 1200 false(unreach-call) 43   26   500 580 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  69   270 .16   0      true 33    19    740 1100 false(unreach-call) 45   24   510 550 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  63   250 .16   .16   true 32    18    390 940 false(unreach-call) 39   21   440 540 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  60   250 .16   0      true 33    19    560 1000 false(unreach-call) 41   22   410 540 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.0  5.0  57   250 .16   0      true 33    19    640 980 false(unreach-call) 30   17   660 520 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  67   260 .27   0      true 29    17    750 1000 false(unreach-call) 59   38   970 830 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  63   250 .26   .16   true 34    19    460 900 false(unreach-call) 46   28   820 620 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16    16    190   510 .79   0      true 32    18    270 790 timeout 96   78   1700 820 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  61   250 .26   0      true 35    20    770 790 false(unreach-call) 48   29   1000 630 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 15    15    220   510 .76   0      true 34    19    450 880 timeout 97   82   1300 910 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.3  5.3  68   250 .23   0      true 35    20    710 810 false(unreach-call) 86   68   1500 710 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.1  59   250 .26   0      true 34    20    440 920 false(unreach-call) 55   36   1100 720 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  62   250 .26   0      true 33    19    670 790 false(unreach-call) 54   34   850 610 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  63   250 .26   0      true 33    19    440 770 false(unreach-call) 58   36   940 830 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16    16    220   510 .79   .0041 true 32    18    580 880 timeout 96   77   1400 860 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  60   250 .27   0      true 31    18    640 740 false(unreach-call) 63   40   1000 820 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 33    33    410   650 2.8    0      - - exception 6.7  3.5  110   280 timeout 960   880   18000 3600
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 32    32    350   600 2.6    0      - - exception 7.2  3.9  130   290 timeout 960   880   22000 4500
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 31    31    360   600 2.5    0      - - exception 8.3  4.5  94   280 timeout 960   900   20000 4100
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 32    32    340   600 2.6    0      - - exception 6.8  3.6  120   290 timeout 960   880   21000 3400
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    5400   1700 7.5    0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.3 3.3 140 310
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    3200   1700 7.5    0      - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 5.7 3.0 89 290
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4300   1700 10      0      - - error (invalid witness file) .64 .42 7.8 40 error (invalid witness file) 6.7 3.5 130 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4100   1700 8.7    0      - - error (invalid witness file) .60 .38 13   44 error (invalid witness file) 6.2 3.3 110 290
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4000   1700 8.5    0      - - error (invalid witness file) .53 .32 9.9 40 error (invalid witness file) 6.0 3.2 140 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    6200   1700 8.7    0      - - error (invalid witness file) .62 .38 7.3 39 error (invalid witness file) 6.2 3.3 120 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4300   1700 9.0    0      - - error (invalid witness file) .70 .45 8.7 43 error (invalid witness file) 6.1 3.3 130 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4300   1700 8.6    0      - - error (invalid witness file) .59 .36 8.7 40 error (invalid witness file) 7.5 3.9 77 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4100   1700 8.8    0      - - error (invalid witness file) .53 .32 11   39 error (invalid witness file) 6.2 3.3 130 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    6400   1700 8.6    .0041 - - error (invalid witness file) .64 .41 7.3 40 error (invalid witness file) 6.8 3.6 130 320
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    5500   1700 9.1    0      - - error (invalid witness file) .67 .42 8.9 41 error (invalid witness file) 6.1 3.2 120 290
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4300   1700 8.9    0      - - error (invalid witness file) .49 .32 8.5 41 error (invalid witness file) 6.6 3.4 130 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (42) 0 wit inspect 850    850    4700   1700 9.5    0      - - error (invalid witness file) .66 .42 7.2 40 error (invalid witness file) 5.6 3.1 120 290
../../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 58 32000 32000 200000 120000 630   12    94 870 530 14000 27000   94 1600 1100 26000 25000   94 190 110 2500 7000   94 4700 4000 93000 38000  
    correct results 45 54 200 200 2500 7900 13   .50 34 750 460 13000 24000   36 1100 680 19000 20000   6 140 75 1700 4300   9 600 320 7400 11000  
        correct true 9 18 85 85 1000 1900 7.8 .16 29 0 0 0 0   0 0 0 0 0   6 140 75 1700 4300   9 600 320 7400 11000  
        correct false 36 36 120 120 1400 6000 5.4 .34 5 750 460 13000 24000   36 1100 680 19000 20000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 9 4 200 200 2400 4900 14   .29 4 110 64 1600 3100   0 480 380 7100 4300   0 29 15 450 1100   0 3800 3500 81000 16000  
        correct-unconfirmed true 4 4 130 130 1500 2400 11   0    4 0 0 0 0   0 0 0 0 0   0 29 15 450 1100   0 3800 3500 81000 16000  
        correct-unconfirmed false 5 0 75 75 960 2500 3.7 .29 0 110 64 1600 3100   0 480 380 7100 4300   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) 58
Run set sv-comp17.ReachSafety-ControlFlow