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 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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 1 1.0  1.0  11   56 1.7  .094  10    5.4  110   300 12   6.3 150 440
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .44 .44 5.3 38 1.7  .094  7.4  4.0  120   300 10   5.4 120 340
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .69 .69 8.5 48 1.7  0      10    5.4  100   310 10   5.5 120 380
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .32 .32 4.2 27 1.7  .094  8.5  4.6  95   330 9.2 4.9 140 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.6  1.6  19   140 2.7  0      18    9.6  270   670 96   53   1200 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.4  1.4  17   140 2.3  0      460    440    8700   7000 73   40   490 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .57 .57 6.1 57 1.9  0      16    8.2  160   480 91   49   920 900
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .86 .86 9.3 77 2.0  0      15    7.7  220   520 84   45   970 1000
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .28 .28 3.0 25 1.8  0      7.5  3.9  100   280 23   12   320 560
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .36 .36 4.7 36 1.9  0      11    5.7  110   370 21   11   300 580
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 0 290    290    3700   15000 1.7  0      6.9  3.7  91   300 11   5.9 120 320
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 0 280    280    3100   15000 1.7  0      7.5  4.0  130   310 9.2 4.9 180 330
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 0 260    260    3800   15000 1.7  0      7.2  3.8  120   300 8.7 4.6 150 330
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 0 270    270    3000   15000 1.7  0      9.1  4.9  100   300 8.1 4.4 140 320
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 0 340    340    3500   15000 1.7  0      7.4  4.0  77   290 8.8 4.7 110 330
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 0 460    460    5100   15000 1.7  0      8.3  4.4  140   310 8.6 4.7 130 320
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 0 600    600    6000   15000 1.7  .0041 7.8  4.1  140   300 9.2 4.9 180 310
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 0 470    470    4900   15000 1.7  0      25    15    640   790 8.0 4.3 110 310
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 0 430    430    4900   15000 1.7  0      7.3  3.9  91   290 9.8 5.2 190 330
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 0 410    410    5500   15000 1.7  0      9.0  4.9  82   300 7.6 4.2 92 320
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 0 400    400    4800   15000 1.7  0      6.8  3.6  130   290 8.6 4.6 150 320
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 0 490    480    4900   15000 1.7  0      6.3  3.4  88   280 9.2 4.9 150 340
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 0 300    300    4300   15000 1.7  0      43    24    510   2500 59   32   400 2300
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 290    290    4200   15000 1.7  0      50    27    910   2800 69   37   440 2500
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 0 270    270    3200   15000 1.7  0      59    33    1100   3200 73   40   730 2700
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 0 280    280    3400   15000 1.7  0      49    27    380   2700 74   40   940 2500
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 0 430    430    6000   15000 1.7  0      670    640    11000   7000 67   36   420 2900
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 300    300    3300   3800 16    0      20    11    220   900 16   8.3 260 700
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 53    53    710   1800 8.3  0      13    6.8  130   600 13   6.7 220 510
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 0 410    410    4300   15000 1.7  0      850    820    15000   7000 72   39   740 2600
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 0 390    390    5300   15000 1.7  0      920    890    12000   6700 76   41   900 2400
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 0 410    410    4700   15000 1.7  0      920    890    13000   6700 64   34   860 2500
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 0 490    490    5300   15000 1.7  0      920    880    12000   6800 83   45   860 3000
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 0 420    420    4900   15000 1.7  0      920    880    14000   6700 71   39   730 2500
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 0 440    440    4900   15000 1.7  0      920    880    12000   6700 64   34   480 2500
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 0 110    110    1100   15000 1.7  0      5.6  3.1  77   280 7.3 3.9 97 310
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 120    110    1400   15000 1.7  0      5.8  3.2  75   280 8.2 4.4 69 320
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 88    88    950   15000 1.7  0      12    6.6  140   400 23   12   210 830
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 92    91    1000   15000 1.7  0      11    6.0  190   470 32   17   580 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 97    97    1300   15000 1.7  0      12    6.3  160   480 35   19   560 2200
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 100    100    1100   15000 1.7  0      15    8.1  140   500 44   26   430 3600
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 110    110    1300   15000 1.7  0      14    7.2  140   530 96   59   1100 6200
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 110    110    1200   15000 1.7  0      16    8.6  140   610 120   77   1200 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 140    140    1600   8700 9.3  0      14    7.6  100   720 13   6.8 150 560
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 210    210    2100   12000 11    0      17    8.8  150   790 19   9.8 220 680
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 77    77    920   15000 1.7  0      12    6.2  110   360 15   7.7 110 500
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 80    80    910   15000 1.7  0      12    6.3  110   370 19   9.7 170 610
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 83    83    870   15000 1.7  0      10    5.3  140   400 24   13   200 670
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 380    380    3100   15000 .84 0      .54 .34 11   40 7.3 3.8 110 310
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 120    120    1100   4500 1.7  .094  97    82    2600   2900 17   9.2 180 470
ntdrivers/floppy_false-unreach-call.i.cil.c 0 900    900    11000   260 .84 0      .66 .41 7.0 40 6.9 3.6 130 310
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 1 4.7  4.7  59   680 1.7  0      13    7.4  220   490 13   6.8 180 440
ntdrivers/parport_false-unreach-call.i.cil.c 0 900    900    7400   10000 .84 0      .53 .34 11   40 7.0 3.7 110 300
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 140    140    1500   15000 .84 0      .50 .32 7.5 40 8.2 4.3 80 310
ntdrivers/diskperf_true-unreach-call.i.cil.c 2 120    120    950   4500 5.8  0      880    860    14000   7000 120   69   1100 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c 0 900    900    10000   1100 .84 0      .60 .39 9.9 42 7.7 4.1 120 310
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 900    900    14000   260 .84 0      .61 .40 8.4 41 8.1 4.3 100 320
ntdrivers/parport_true-unreach-call.i.cil.c 0 900    900    9200   10000 .84 0      .63 .40 7.9 39 6.1 3.3 74 290
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 390    390    4500   15000 1.7  0      16    8.4  160   470 12   6.6 150 370
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 450    450    5400   15000 1.8  0      11    6.1  220   470 9.9 5.3 150 350
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 440    440    5000   15000 1.7  0      12    6.3  270   470 12   6.1 98 360
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 440    440    5200   15000 1.8  0      15    7.8  130   470 10   5.6 180 360
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 700    700    6800   15000 1.7  0      96    72    2300   3200 10   5.6 150 350
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 430    430    4100   15000 .84 0      .51 .33 9.7 41 6.1 3.2 65 300
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 420    420    5300   15000 .84 0      .51 .32 9.9 40 6.2 3.3 69 300
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 430    430    4800   15000 .84 0      .65 .42 8.0 42 6.2 3.3 110 290
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 540    540    5200   15000 .84 0      .53 .34 11   40 6.4 3.4 110 300
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 450    450    4500   15000 .84 0      .50 .33 12   39 6.2 3.2 89 300
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 470    470    4500   15000 .84 0      .60 .39 8.5 40 5.8 3.1 92 300
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 450    450    4500   15000 .84 .41   .62 .40 6.9 44 6.7 3.5 130 310
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 460    460    4500   15000 .84 0      .55 .34 9.0 42 6.0 3.2 86 300
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 470    470    4700   15000 .84 0      .47 .30 9.0 40 5.6 3.0 110 290
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 490    490    4500   15000 .84 0      .55 .36 10   39 6.3 3.3 95 300
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 470    470    4600   15000 .84 0      .64 .41 6.5 40 6.0 3.2 110 300
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 490    490    5100   15000 .84 0      .49 .32 11   40 5.7 3.0 87 300
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 480    480    4600   15000 .84 0      .51 .33 11   40 6.4 3.3 90 300
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 520    520    4900   15000 .84 0      .63 .41 7.6 39 6.2 3.2 79 310
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 400    400    5100   15000 1.7  0      240    220    4200   2800 960   880   17000 3800
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 450    450    4800   15000 1.8  0      220    200    3400   2700 960   890   21000 3700
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 450    450    4800   15000 1.7  0      210    190    2700   2700 960   900   16000 4000
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 460    460    5300   15000 1.7  0      240    220    3700   2700 960   880   14000 3700
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 780    780    8900   15000 1.7  0      910    890    16000   5900 960   820   11000 5400
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 430    430    4900   15000 .84 0      .60 .38 7.1 40 6.2 3.3 56 310
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 560    560    5100   15000 .84 0      .50 .31 11   41 5.5 3.0 91 290
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 450    450    5400   15000 .84 0      .51 .33 7.2 43 7.3 3.8 88 290
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 470    470    5100   15000 .84 0      .66 .43 6.2 39 6.8 3.6 130 310
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 460    460    4000   15000 .84 0      .71 .44 8.1 40 5.7 3.0 73 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 450    450    3700   15000 .84 0      .56 .36 8.7 39 5.7 3.0 50 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 450    450    4800   15000 .84 0      .66 .42 7.2 40 5.9 3.2 100 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 510    510    4600   15000 .84 0      .69 .44 7.9 41 6.4 3.4 91 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 460    460    4400   15000 .84 0      .51 .33 8.2 40 6.4 3.4 110 310
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 500    500    5400   15000 .84 0      .53 .33 11   40 7.8 4.1 100 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 490    490    4400   15000 .84 0      .71 .44 9.1 44 5.9 3.2 54 310
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 550    550    5400   15000 .84 .0082 .61 .39 7.7 40 7.8 4.1 120 340
../../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 27 33000   33000   360000 1100000 180   .80  94 430 280 8400 15000   94 350 190   5200 14000   94 9700 9200 150000 100000   94 6700 5400 99000 86000  
    correct results 16 27 830   830   8900 32000 72   .28  5 49 27 650 1700   5 54 29   710 1900   9 1500 1400 24000 19000   11 560 310 6200 9200  
        correct true 11 22 820   820   8800 31000 63   0     0 0 0 0 0   5 0 0   0 0   9 1500 1400 24000 19000   11 560 310 6200 9200  
        correct false 5 5 7.1 7.1 88 850 8.5 .28  5 49 27 650 1700   0 54 29   710 1900   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 0 120   120   1100 4500 1.7 .094 0 97 82 2600 2900   1 17 9.2 180 470   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 1 0 120   120   1100 4500 1.7 .094 0 97 82 2600 2900   0 17 9.2 180 470   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) 27
Run set sv-comp17.ReachSafety-ControlFlow