Tool DepthK ESBMC+DepthK version 2.1
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-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]]
Run set sv-comp16.ControlFlow
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.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 false(reach) 10    7.7  200 wit false(reach) 23   13   850 true 15 8.1 390
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 5.8  3.8  180 wit false(reach) 18   10   620 true 15 11   340
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 8.1  5.8  190 wit false(reach) 23   13   640 true 16 8.8 360
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c witness timeout 6.2  4.4  180 wit timeout 90   77   2300 true 15 8.7 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 2.1  2.1  75 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 1.6  1.6  39 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true .92 .95 34 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 1.1  1.2  46 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true .76 .79 28 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 1.1  1.1  33 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 62    61    290 wit false(reach) 13   7.3 490 true 11 6.4 330
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 62    60    300 wit false(reach) 13   6.9 490 true 14 8.7 350
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 77    75    330 wit false(reach) 14   7.5 510 true 11 6.6 350
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 62    60    290 wit false(reach) 13   7.1 500 true 13 7.9 320
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 4.1  2.4  180 wit false(reach) 14   7.7 530 true 12 7.6 340
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c witness timeout 85    83    340 wit timeout 90   72   1300 true 15 8.7 350
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 120    120    360 wit timeout 91   70   1300 true 15 8.9 340
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c witness timeout 97    95    340 wit timeout 90   72   1200 true 14 8.0 320
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 5.8  3.9  180 wit false(reach) 16   8.2 560 true 12 6.5 330
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 84    82    350 wit false(reach) 12   6.4 460 true 13 7.3 340
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c witness timeout 65    63    300 wit timeout 90   71   1300 true 14 7.8 340
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 4.7  2.7  180 wit false(reach) 10   5.6 420 true 13 7.5 330
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 5.2  5.3  270 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 7.1  7.1  280 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 6.2  6.2  320 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 5.6  5.6  270 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 5.6  5.6  260 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true .82 .85 32 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .58 .61 26 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 5.7  5.7  280 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 6.0  6.0  280 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 6.5  6.5  280 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 7.5  7.5  290 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 5.8  5.9  290 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 6.1  6.1  280 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 3.6  2.0  170 wit false(reach) 9.7 5.3 400 true 11 8.0 320
locks/test_locks_15_false-unreach-call.c false(reach) 3.7  2.1  170 wit false(reach) 9.6 5.4 410 true 12 8.1 340
locks/test_locks_10_true-unreach-call.c true 1.1  1.1  59 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 1.1  1.1  67 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 1.2  1.2  77 wit - -
locks/test_locks_13_true-unreach-call.c true 1.4  1.5  86 wit - -
locks/test_locks_14_true-unreach-call.c true 1.4  1.4  96 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 1.7  1.8  110 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true .65 .68 29 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true .68 .72 34 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true .85 .88 39 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true .83 .86 45 wit - -
locks/test_locks_9_true-unreach-call.c true .86 .88 52 wit - -
../../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 860 820 8600 48 640   460   14000   48 240   150   6100  
    correct results 43 480 460 7100 13 190   100   6900   13 170   100   4500  
        correct true 30 88 89 4100 0 0   0   0   13 0   0   0  
        correct false 13 390 370 3000 13 190   100   6900   0 170   100   4500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 73
Run set sv-comp16.ControlFlow