Tool CBMC
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.ControlFlow
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c 1.2  1.2  130 14   7.6 550 91 52   1000
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c .33 .34 36 13   7.2 540 82 48   860
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c .52 .53 49 15   7.7 570 92 53   1500
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c .24 .25 32 13   7.2 530 41 23   710
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 8.3  8.3  130
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 3.6  3.6  51
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 2.3  2.4  37
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 4.0  4.0  50
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 1.3  1.3  28
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 1.6  1.6  31
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 1.9  2.0  67 90   75   3700 21 11   470
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 2.0  2.0  67 90   75   3700 20 11   450
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 2.2  2.2  80 90   72   3700 17 9.2 430
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 2.0  2.0  70 90   72   3700 22 13   510
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c .16 .17 27 90   72   3800 18 9.7 370
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 12    12    290 90   72   3700 25 14   520
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 3.6  3.6  120 91   71   3700 24 13   520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 3.2  3.2  120 91   71   3800 22 12   380
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c .17 .18 27 90   72   3800 21 11   470
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 2.9  3.0  120 90   71   3800 21 11   490
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 2.8  2.8  110 91   71   3700 20 11   510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c .18 .19 27 8.4 4.7 400 17 9.5 350
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 850    850    1200
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 850    850    1200
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 850    850    1400
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 850    850    1200
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 850    850    1100
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 630    630    970
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 160    160    440
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 850    850    1100
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 850    850    1000
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 850    850    1000
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 850    850    1000
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 850    850    1000
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 850    850    1000
locks/test_locks_14_false-unreach-call.c .20 .21 25 91   75   3700 15 8.6 340
locks/test_locks_15_false-unreach-call.c .15 .16 25 90   78   3600 16 8.6 350
locks/test_locks_10_true-unreach-call.c 850    850    2900
locks/test_locks_11_true-unreach-call_false-termination.c 850    850    3500
locks/test_locks_12_true-unreach-call_false-termination.c 850    850    4000
locks/test_locks_13_true-unreach-call.c 850    850    5000
locks/test_locks_14_true-unreach-call.c 850    850    5300
locks/test_locks_15_true-unreach-call_false-termination.c 850    850    2000
locks/test_locks_5_true-unreach-call_false-termination.c 180    180    1000
locks/test_locks_6_true-unreach-call_false-termination.c 270    270    1400
locks/test_locks_7_true-unreach-call_false-termination.c 400    400    1800
locks/test_locks_8_true-unreach-call_false-termination.c 550    550    2300
locks/test_locks_9_true-unreach-call.c 780    780    2800
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 48 17000 17000 47000 48 1200   980   51000   48 590   330   10000  
    correct results 47 17000 17000 47000 5 1100   910   47000   15 570   320   9800  
        correct true 30 17000 17000 46000 0 0   0   0   0 0   0   0  
        correct false 17 34 34 1300 5 1100   910   47000   15 570   320   9800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 77
Run set sv-comp16.ControlFlow