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-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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 .49  .49  6.1  50 .84 0   7.7  4.1  95   300 11   5.8 160 420
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .80  .79  1.9  28 .84 0   7.8  4.1  120   310 9.7 5.2 160 340
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .34  .34  4.0  32 .84 0   7.7  4.1  110   310 10   5.4 150 370
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .19  .19  1.7  27 .84 0   6.6  3.5  110   310 9.6 5.1 150 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.1   1.1   12    140 .84 0   18    9.4  220   660 92   51   720 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .91  .91  12    74 .84 0   360    350    4500   7000 71   39   560 970
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .33  .33  3.9  42 .84 0   12    6.5  140   480 67   36   580 940
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .53  .53  5.9  64 .84 0   15    7.6  170   520 79   42   640 980
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .17  .17  2.0  26 .84 0   7.4  4.0  130   320 22   11   260 570
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .96  .95  1.9  38 .84 0   9.3  4.9  83   360 21   11   260 600
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 1 3.8   3.8   53    230 .84 0   6.7  3.6  81   320 9.5 5.1 160 330
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 3.8   3.8   45    230 .84 0   6.7  3.6  110   300 8.6 4.6 120 330
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 1 4.6   4.6   67    280 .84 0   7.0  3.7  78   300 8.4 4.6 160 330
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 1 3.9   3.9   46    230 .84 0   7.4  3.9  160   310 9.2 4.9 160 330
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 1 .12  .12  1.2  26 .84 0   5.2  2.8  56   280 8.1 4.4 160 320
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 1 7.4   7.3   84    380 .84 0   8.3  4.4  150   320 8.9 4.8 150 330
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 1 6.0   6.0   83    300 .84 0   10    5.3  230   430 9.1 4.9 180 330
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 1 1.8   1.8   23    120 .84 0   7.2  3.8  130   300 9.1 4.9 150 320
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 1 .20  .20  2.6  26 .94 0   6.0  3.2  97   290 8.8 4.7 120 310
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 1 1.6   1.6   18    110 .84 0   6.5  3.5  110   290 8.7 4.6 120 320
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 1 1.5   1.5   19    100 .84 0   6.8  3.6  110   300 8.6 4.6 130 320
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 1 .11  .11  1.3  26 .84 0   5.0  2.7  89   290 9.7 5.2 170 340
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 2 46     46     570    1900 .84 0   18    10    280   640 52   28   920 1500
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 45     45     610    1900 .84 0   19    11    260   650 64   34   580 1500
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 2 52     52     730    2300 .84 0   24    13    240   690 56   30   540 1700
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 2 46     46     710    1900 .84 0   16    9.2  270   640 62   33   810 1400
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 0 770     770     9400    15000 .84 0   .57 .35 13   43 6.1 3.3 93 300
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 900     900     11000    14000 .84 0   .53 .34 14   40 5.7 3.0 120 300
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 420     410     5300    15000 .84 0   .52 .34 11   41 5.9 3.1 120 300
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 0 870     870     11000    15000 .84 0   .52 .33 11   39 6.2 3.3 130 300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 0 850     850     11000    15000 .84 0   .50 .33 10   39 5.6 2.9 88 300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 0 850     850     12000    15000 .84 0   .47 .31 6.4 41 5.9 3.1 130 290
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 0 900     900     10000    14000 .84 0   .51 .33 11   39 6.0 3.2 110 300
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 0 890     890     9900    15000 .84 0   .49 .32 10   41 6.2 3.3 110 300
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 0 900     900     10000    15000 .84 0   .58 .38 4.8 41 6.3 3.4 130 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 .092 .093 .97 24 .84 0   4.9  2.6  73   280 7.5 4.0 130 320
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 .091 .090 1.1  24 .84 0   5.2  2.8  84   290 7.8 4.1 140 310
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16  .15  1.3  24 .84 0   6.4  3.4  110   310 21   11   260 790
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16  .16  1.6  24 .84 0   8.1  4.4  90   310 26   14   350 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15  .15  2.1  24 .84 0   7.3  3.9  120   320 34   19   520 2300
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16  .16  1.8  25 .84 0   7.0  3.7  88   310 38   23   340 3600
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .18  .18  2.2  26 .99 0   9.4  5.0  100   320 84   53   930 6400
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .21  .21  1.9  28 .84 0   8.7  4.6  95   320 87   55   730 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12  .12  1.1  23 .84 0   4.9  2.7  95   290 9.7 5.3 150 350
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .10  .10  1.3  24 .84 0   4.9  2.7  95   290 11   6.1 160 380
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14  .14  1.3  23 .84 0   6.5  3.5  110   300 13   6.7 240 410
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  1.5  24 .84 0   6.4  3.5  94   290 15   7.9 240 560
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15  .15  1.4  24 .84 0   6.3  3.4  100   310 19   9.7 220 600
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 1.6   1.6   21    280 .84 0   .51 .33 8.3 41 7.0 3.7 130 310
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 .94  .94  12    91 .84 0   97    82    1400   3100 13   7.3 180 480
ntdrivers/floppy_false-unreach-call.i.cil.c 0 900     900     13000    240 .84 0   .50 .34 11   40 6.9 3.6 120 300
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 1 150     150     2000    2200 .84 0   12    6.7  150   480 12   6.6 170 410
ntdrivers/parport_false-unreach-call.i.cil.c 0 37     37     85    430 .84 0   97    70    1700   4200 22   13   260 600
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 2.4   2.4   30    310 .84 0   .49 .32 11   42 7.1 3.8 130 310
ntdrivers/diskperf_true-unreach-call.i.cil.c 2 3.0   3.0   36    160 .84 0   660    650    6600   7000 110   62   840 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c 0 900     900     12000    450 .84 0   .50 .33 12   40 8.0 4.2 150 310
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 900     900     12000    240 .84 0   .54 .34 13   41 6.6 3.5 130 300
ntdrivers/parport_true-unreach-call.i.cil.c 2 75     75     730    1400 .84 0   380    310    6500   7000 190   130   1900 4100
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 900     900     8300    3900 .84 0   .49 .32 9.9 39 6.9 3.6 130 310
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 850     850     8000    3200 .84 0   11    6.1  170   470 10   5.4 180 340
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 810     810     8000    3100 .84 0   11    5.9  100   470 9.8 5.2 110 350
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 890     890     8100    3200 .84 0   11    6.0  230   470 9.9 5.3 130 350
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 1 250     250     2500    1600 .84 0   9.0  4.8  100   380 11   5.8 170 380
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 1 190     190     1600    1600 .84 0   9.3  5.0  150   380 10   5.5 180 360
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 1 190     190     1600    1500 .84 0   9.2  4.9  130   390 9.9 5.4 150 360
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 1 180     180     1400    1500 .84 0   9.2  4.9  100   390 9.9 5.4 150 360
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 1 830     830     8000    3700 .84 0   11    5.7  170   450 10   5.5 140 360
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 1 670     670     6100    3400 .84 0   11    5.7  190   450 11   5.8 180 390
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 900     900     8000    3900 .84 0   .49 .32 8.0 39 6.2 3.3 140 300
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 1 620     620     6900    3400 .84 0   10    5.6  100   460 11   5.9 180 380
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 900     900     9000    3800 .84 0   .53 .35 4.8 40 6.4 3.4 130 300
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 1 440     440     4200    2400 .84 0   10    5.4  92   450 10   5.5 170 360
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 1 700     700     5900    3600 .84 0   10    5.4  180   450 10   5.6 160 350
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 1 590     590     5700    3400 .84 0   10    5.4  160   460 10   5.4 170 350
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 1 750     750     5700    3700 .84 0   10    5.5  150   450 10   5.6 160 350
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900     900     7800    4000 .84 0   .49 .32 12   39 6.4 3.4 130 300
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 1 780     780     6900    3600 .84 0   10    5.5  140   450 10   5.5 150 360
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 900     900     9700    3600 .84 0   .53 .35 4.6 41 6.3 3.3 130 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 900     900     10000    3500 .84 0   .53 .36 7.0 41 6.7 3.5 110 310
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 900     900     9100    3200 .88 0   .54 .33 14   40 6.6 3.5 92 320
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 900     900     8300    3500 .84 0   .55 .35 14   43 6.3 3.3 89 300
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900     900     11000    4700 .84 0   .51 .34 12   39 6.4 3.4 130 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900     900     7700    4700 .84 0   .50 .35 7.3 40 6.7 3.6 120 300
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900     900     9000    4700 .84 0   .49 .32 6.0 42 5.9 3.2 110 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900     900     8100    4400 .84 0   .53 .33 13   40 7.0 3.7 86 300
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900     900     8700    4400 .84 0   .51 .33 9.3 39 6.1 3.3 130 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900     900     7300    4500 .84 0   .51 .33 12   40 6.6 3.5 130 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900     900     9500    4100 .84 0   .47 .29 6.2 39 6.5 3.4 130 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900     900     7600    4600 .84 0   .51 .34 8.6 41 6.5 3.4 120 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900     900     9600    4400 .84 0   .50 .33 13   40 5.7 3.1 110 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900     900     8200    3700 .84 0   .53 .34 12   41 5.9 3.2 120 290
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900     900     8000    3900 .84 0   .53 .34 9.0 40 6.2 3.3 110 290
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900     900     8100    4600 .84 0   .51 .33 10   42 6.2 3.3 120 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900     900     7600    3900 .84 0   .52 .33 12   41 6.2 3.3 120 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 80 38000 38000 390000 280000 79   0   94 480 310 7500 20000   94 400 220 6500 15000   94 1600 1400 21000 30000   94 1400 820 16000 49000  
    correct results 57 80 9200 9200 87000 58000 48   0   34 290 150 4300 13000   34 330 180 5300 12000   20 1600 1400 20000 29000   22 1200 720 13000 40000  
        correct true 23 46 270 270 3400 10000 19   0   0 0 0 0 0   33 0 0 0 0   20 1600 1400 20000 29000   22 1200 720 13000 40000  
        correct false 34 34 8900 8900 83000 47000 29   0   34 290 150 4300 13000   1 330 180 5300 12000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 2 0 38 38 96 520 1.7 0   0 190 150 3200 7300   2 35 20 440 1100   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 2 0 38 38 96 520 1.7 0   0 190 150 3200 7300   0 35 20 440 1100   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) 80
Run set sv-comp17.ReachSafety-ControlFlow