Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.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 .48  .48  6.0  49 .84 0   false(unreach-call) 7.7  4.1  160   310 true 12   6.4 230 420 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .23  .23  2.5  28 .84 0   false(unreach-call) 7.3  3.9  110   300 true 11   5.7 180 360 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .31  .31  3.7  32 .84 0   false(unreach-call) 7.8  4.2  160   310 true 9.8 5.3 150 380 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .20  .20  1.7  27 .84 0   false(unreach-call) 7.2  3.9  120   370 true 9.2 5.0 160 320 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1   1.1   11    140 .84 0   - - true 18    9.6  250   550 true 97   53   660 1000
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c out of memory 0 wit inspect 370     370     5400    15000 .84 0   - - error (invalid witness file) .50 .33 9.8 40 error (invalid witness file) 5.9 3.1 100 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .36  .36  3.9  42 .84 0   - - true 12    6.3  170   480 true 70   38   570 960
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .56  .56  6.7  64 .84 0   - - true 15    7.6  190   530 true 78   42   610 1000
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .17  .17  1.8  26 .84 0   - - true 6.9  3.7  100   290 true 21   11   250 540
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .25  .25  3.1  38 .84 0   - - true 9.1  4.8  170   350 true 21   11   230 590
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.4   2.4   29    140 .84 0   false(unreach-call) 7.2  3.8  160   300 true 8.7 4.7 190 330 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.5   2.5   32    140 .84 0   false(unreach-call) 7.1  3.8  130   300 true 8.7 4.6 160 330 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 3.0   3.0   39    160 .84 0   false(unreach-call) 7.3  3.9  110   310 true 9.4 5.0 180 330 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 2.5   2.5   29    140 .84 0   false(unreach-call) 7.2  3.8  120   310 true 9.4 5.0 180 330 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .095 .095 1.1  26 .84 0   false(unreach-call) 5.5  3.0  95   290 true 8.5 4.6 140 310 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 4.7   4.7   60    220 .84 0   false(unreach-call) 7.9  4.2  150   310 true 9.7 5.2 140 330 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 3.7   3.7   48    180 .84 0   false(unreach-call) 10    5.2  200   430 true 9.1 4.9 180 320 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 1.1   1.1   14    74 .84 0   false(unreach-call) 7.1  3.8  120   300 true 9.1 4.9 190 330 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .21  .21  2.7  26 .84 0   false(unreach-call) 6.2  3.3  100   290 true 9.1 4.8 160 320 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .99  .99  12    72 .84 0   false(unreach-call) 6.7  3.6  100   290 true 10   5.4 120 320 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .96  .96  13    67 .84 0   false(unreach-call) 6.9  3.7  100   300 true 8.8 4.7 140 320 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .12  .12  1.1  26 .84 0   false(unreach-call) 5.4  2.9  95   290 false(unreach-call) 10   5.5 150 330 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 31     31     420    1200 .84 0   - - true 16    8.9  130   570 true 52   28   440 1500
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 31     31     350    1200 .84 0   - - true 17    9.6  220   640 true 56   30   510 1400
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 35     35     480    1500 .84 0   - - true 21    11    190   680 true 67   36   540 1500
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 30     30     380    1200 .84 0   - - true 17    9.4  200   640 true 61   32   550 1300
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 0 wit inspect 900     900     11000    13000 .84 0   - - error (invalid witness file) .59 .37 7.9 40 error (invalid witness file) 6.3 3.3 110 310
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     900     3100    3500 .84 0   - - error (invalid witness file) .50 .32 8.7 39 error (invalid witness file) 6.5 3.4 130 300
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c out of memory 0 wit inspect 480     480     5300    15000 .84 0   - - error (invalid witness file) .52 .33 9.1 41 error (invalid witness file) 5.7 3.1 83 300
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 0 wit inspect 900     900     12000    12000 .84 0   - - error (invalid witness file) .61 .40 6.2 41 error (invalid witness file) 6.0 3.2 120 300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 0 wit inspect 900     900     9400    12000 .84 0   - - error (invalid witness file) .69 .45 7.5 42 error (invalid witness file) 5.4 2.9 110 290
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 0 wit inspect 900     900     11000    12000 .84 0   - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 5.9 3.1 97 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 0 wit inspect 900     900     10000    10000 .84 0   - - error (invalid witness file) .48 .32 8.4 39 error (invalid witness file) 6.5 3.4 130 300
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 0 wit inspect 900     900     12000    11000 .84 0   - - error (invalid witness file) .71 .44 7.3 39 error (invalid witness file) 6.3 3.4 120 300
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 0 wit inspect 900     900     11000    11000 .84 0   - - error (invalid witness file) .49 .32 5.8 40 error (invalid witness file) 6.3 3.3 120 290
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .12  .12  .98 24 .84 0   false(unreach-call) 5.2  2.8  98   290 true 7.7 4.1 150 320 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .091 .092 1.1  24 .84 0   false(unreach-call) 5.9  3.2  93   280 true 7.9 4.2 160 310 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 330     330     3800    15000 .84 0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.6 3.0 84 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 340     340     4000    15000 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.8 3.6 130 320
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 350     350     4300    15000 .84 0   - - error (invalid witness file) .51 .34 7.7 39 error (invalid witness file) 5.8 3.1 130 290
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 350     350     5200    15000 .84 0   - - error (invalid witness file) .48 .31 5.5 41 error (invalid witness file) 6.0 3.2 110 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 350     350     4200    15000 .84 0   - - error (invalid witness file) .71 .45 9.1 44 error (invalid witness file) 6.1 3.2 130 290
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 360     360     4000    15000 .84 0   - - error (invalid witness file) .49 .33 6.7 39 error (invalid witness file) 6.1 3.2 130 290
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 290     290     4300    15000 .84 0   - - error (invalid witness file) .47 .30 5.8 39 error (invalid witness file) 5.8 3.2 110 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 290     290     3600    15000 .86 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.9 3.1 99 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 310     310     3900    15000 .84 0   - - error (invalid witness file) .47 .32 4.4 39 error (invalid witness file) 5.7 3.0 71 290
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 310     310     3900    15000 .84 0   - - error (invalid witness file) .51 .32 8.9 39 error (invalid witness file) 5.9 3.1 110 290
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c out of memory 0 wit inspect 320     320     3800    15000 .84 0   - - error (invalid witness file) .57 .37 7.8 40 error (invalid witness file) 5.8 3.1 120 310
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     11000    2500 .84 0   error (invalid witness file) .51 .34 12   39 error (invalid witness file) 7.3 3.8 140 310 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect .97  .97  12    91 .84 0   timeout 97    82    1100   3300 true 14   7.3 220 450 - -
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 5.5   5.5   65    360 .84 0   true 38    24    440   1300 true 24   13   290 590 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 96     96     1200    1200 .84 0   false(unreach-call) 12    6.9  210   480 true 13   7.2 230 440 - -
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 11     11     120    430 .84 0   timeout 97    68    930   4300 true 23   13   310 600 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect 37     37     510    560 .84 0   - - error (invalid witness file) .49 .32 13   41 error (invalid witness file) 7.8 4.1 160 310
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     10000    10000 .84 0   - - error (invalid witness file) .54 .34 14   44 error (invalid witness file) 6.6 3.5 130 300
ntdrivers/floppy2_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     9300    3200 .84 0   - - error (invalid witness file) .55 .35 13   42 error (invalid witness file) 7.8 4.1 140 320
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 900     900     7300    3700 .84 0   - - error (invalid witness file) .48 .31 9.1 40 error (invalid witness file) 6.6 3.5 140 300
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8400    4200 .84 0   - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.6 3.5 120 300
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8000    3800 .84 0   error (invalid witness file) .52 .34 6.0 39 error (invalid witness file) 5.7 3.0 110 280 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 750     750     8000    3100 .84 0   false(unreach-call) 11    6.1  140   480 true 11   5.9 220 360 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 740     740     7900    3100 .84 0   false(unreach-call) 11    6.1  170   470 true 11   5.7 190 360 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 760     760     7400    3100 .84 0   false(unreach-call) 13    6.9  210   470 true 9.9 5.3 170 350 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 240     240     2400    1500 .84 0   false(unreach-call) 9.3  5.0  130   390 true 12   6.3 140 360 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 300     300     2800    1500 .84 0   false(unreach-call) 9.6  5.1  190   380 true 10   5.6 210 360 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 200     200     2400    1500 .84 0   false(unreach-call) 10    5.6  150   400 true 11   6.1 220 360 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 170     170     1500    1500 .84 0   false(unreach-call) 9.4  5.0  160   380 true 10   5.6 180 360 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 870     870     8700    3500 .99 0   false(unreach-call) 10    5.5  140   460 true 11   6.0 200 380 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 700     700     5800    3300 .84 0   false(unreach-call) 10    5.5  150   460 true 10   5.5 180 350 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     9500    4600 .84 0   error (invalid witness file) .61 .38 7.4 39 error (invalid witness file) 5.7 3.1 120 290 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     1900    2000 .84 0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.9 3.2 98 290 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7900    3800 .84 0   error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 120 300 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 410     410     3300    2300 .84 0   false(unreach-call) 10    5.6  140   460 true 11   6.1 210 380 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 660     660     5700    3500 .84 0   false(unreach-call) 13    6.8  89   460 true 9.9 5.4 180 360 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 610     610     6100    3300 .84 0   false(unreach-call) 11    6.1  130   450 true 11   5.6 210 360 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 690     690     6700    3600 .84 0   false(unreach-call) 11    5.7  210   460 true 11   5.8 180 370 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7900    3500 .84 0   error (invalid witness file) .53 .35 12   42 error (invalid witness file) 5.9 3.2 100 300 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 700     700     5500    3500 .84 0   false(unreach-call) 11    5.7  200   460 true 12   6.6 170 370 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8500    3400 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.9 3.2 110 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     2400    1600 .99 0   - - error (invalid witness file) .50 .32 9.5 40 error (invalid witness file) 6.1 3.2 120 290
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     11000    3300 .84 0   - - error (invalid witness file) .55 .37 5.7 43 error (invalid witness file) 5.8 3.1 110 280
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8400    3100 .84 0   - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 6.1 3.3 120 300
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7700    4500 .84 0   - - error (invalid witness file) .61 .41 6.5 40 error (invalid witness file) 6.6 3.5 140 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8000    4500 .84 0   - - error (invalid witness file) .48 .33 11   40 error (invalid witness file) 6.4 3.4 110 300
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7500    4500 .84 0   - - error (invalid witness file) .48 .31 6.4 41 error (invalid witness file) 6.4 3.4 130 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7900    3500 .84 0   - - error (invalid witness file) .51 .35 13   39 error (invalid witness file) 5.9 3.2 120 290
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7500    4300 .84 0   - - error (invalid witness file) .54 .34 9.0 42 error (invalid witness file) 7.0 3.7 140 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8600    4200 .84 0   - - error (invalid witness file) .48 .30 8.3 39 error (invalid witness file) 6.6 3.5 120 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8900    3800 .84 0   - - error (invalid witness file) .47 .31 7.0 40 error (invalid witness file) 6.3 3.3 130 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7400    4000 .84 0   - - error (invalid witness file) .52 .34 11   43 error (invalid witness file) 7.3 3.8 120 310
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     8200    4000 .84 0   - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.2 3.2 110 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     9400    4300 .84 0   - - error (invalid witness file) .51 .32 8.3 40 error (invalid witness file) 5.9 3.2 110 300
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     11000    4600 .84 0   - - error (invalid witness file) .55 .35 5.8 40 error (invalid witness file) 6.2 3.3 110 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     9400    4200 .84 0   - - error (invalid witness file) .53 .34 13   40 error (invalid witness file) 6.2 3.3 120 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900     900     7400    4600 .84 0   - - error (invalid witness file) .51 .33 7.4 39 error (invalid witness file) 6.6 3.5 130 310
../../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 51 44000 44000 440000 430000 79   0   94 520 330 7200 21000   94 430 230 7400 15000   94 160 86 2000 6500   94 790 420 9500 23000  
    correct results 42 51 8100 8100 77000 47000 35   0   33 290 150 4700 12000   33 330 180 5900 12000   9 130 71 1600 4700   9 520 280 4400 9800  
        correct true 9 18 130 130 1700 5500 7.6 0   0 0 0 0 0   32 0 0 0 0   9 130 71 1600 4700   9 520 280 4400 9800  
        correct false 33 33 7900 7900 76000 41000 28   0   33 290 150 4700 12000   1 330 180 5900 12000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 0 18 18 200 880 2.5 0   1 230 180 2500 8900   3 60 34 810 1600   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 3 0 18 18 200 880 2.5 0   0 230 180 2500 8900   0 60 34 810 1600   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) 51
Run set sv-comp17.ReachSafety-ControlFlow