Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-23-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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 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/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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) 800    690    5100 wit false(reach) 24   13   840 true 17 9.9 380
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 800    690    4900 wit false(reach) 20   11   640 true 14 8.0 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 810    510    7700 wit false(reach) 22   13   650 true 16 9.1 350
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c witness timeout 860    560    7600 wit timeout 91   73   1500 true 13 7.2 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true .58 .59 62 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true .28 .29 30 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true .21 .22 24 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true .25 .26 35 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true .11 .12 17 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true .17 .18 21 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 810    540    6200 wit false(reach) 12   6.7 480 true 14 8.3 340
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 810    550    6400 wit false(reach) 13   7.1 510 true 13 8.2 330
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c unknown 900    900    4300 wit - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 810    560    6000 wit false(reach) 12   6.8 480 true 13 8.0 330
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 810    680    5000 wit false(reach) 15   7.8 510 true 13 9.3 330
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c witness timeout 810    650    5400 wit timeout 90   71   1300 true 13 7.3 340
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 800    650    5600 wit timeout 90   69   1200 true 13 8.0 330
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c witness timeout 800    660    5400 wit timeout 90   74   1200 true 13 7.4 350
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c unknown 890    900    1900 wit - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c unknown 890    900    2000 wit - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c unknown 890    900    1800 wit - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c unknown 890    900    1900 wit - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 61    61    1800 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 62    62    1800 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c unknown 890    900    4300 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 62    62    1800 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c unknown 890    900    1800 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 1.9  1.9  140 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .97 .98 70 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c unknown 890    900    1800 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c unknown 890    900    1800 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c unknown 900    900    1800 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c unknown 890    900    1900 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c unknown 890    900    1900 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c unknown 890    900    1900 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 100    84    2700 wit false(reach) 9.6 5.4 380 true 12 7.4 340
locks/test_locks_15_false-unreach-call.c false(reach) 110    100    3700 wit false(reach) 9.5 5.4 400 true 11 6.4 330
locks/test_locks_10_true-unreach-call.c true 9.2  9.2  830 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 11    11    1000 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 14    14    1200 wit - -
locks/test_locks_13_true-unreach-call.c true 16    16    1400 wit - -
locks/test_locks_14_true-unreach-call.c true 19    19    1600 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 23    23    1800 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 2.3  2.3  230 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 3.1  3.1  320 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 4.3  4.3  430 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 5.3  5.4  550 wit - -
locks/test_locks_9_true-unreach-call.c true 7.2  7.2  680 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 21000 19000 120000 48 500   360   10000   48 170   100   4400  
    correct results 31 6200 4700 64000 9 140   76   4900   9 120   75   3100  
        correct true 22 300 300 16000 0 0   0   0   9 0   0   0  
        correct false 9 5900 4400 48000 9 140   76   4900   0 120   75   3100  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 53
Run set sv-comp16.ControlFlow