Tool 2LS 0.3.4
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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set sv-comp16.ControlFlow
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.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) 2.3  2.3  460 wit timeout 91   67   3800 false(reach) 25 13   540
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) .69 .70 110 wit true 11   6.2 510 false(reach) 25 13   520
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) .86 .87 190 wit true 13   7.2 590 false(reach) 30 18   550
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) .46 .46 63 wit true 12   6.3 410 false(reach) 22 12   480
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 2.3  2.3  460 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true .75 .75 150 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true .67 .67 110 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 1.1  1.1  190 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true .21 .22 32 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true .44 .44 63 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 35    35    240 wit timeout 90   74   3600 false(reach) 19 12   470
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 41    41    260 wit timeout 90   75   3600 false(reach) 20 12   470
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness timeout 78    78    340 wit timeout 90   75   3600 unknown 19 10   490
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 45    45    260 wit timeout 90   76   3600 false(reach) 21 11   490
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) .40 .41 43 wit timeout 90   73   3700 false(reach) 17 9.7 390
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 86    86    340 wit timeout 90   74   3600 false(reach) 24 13   540
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 71    71    320 wit timeout 91   72   3700 true 17 9.4 470
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 29    29    200 wit timeout 90   72   3600 false(reach) 22 12   510
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 5.5  5.5  90 wit timeout 90   73   3700 false(reach) 21 12   490
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 30    30    200 wit timeout 90   74   3700 false(reach) 22 12   510
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 19    19    170 wit timeout 90   74   3700 false(reach) 21 13   490
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) .36 .36 42 wit timeout 90   74   3700 false(reach) 20 12   370
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 65    65    350 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 82    82    370 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 150    150    490 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 78    78    370 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900    900    7500 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 2.0  2.0  53 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .80 .81 33 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900    900    7700 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900    900    7600 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900    900    7400 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900    900    7400 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900    900    7500 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900    900    7700 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) .18 .19 27 wit false(reach) 8.8 4.8 390 false(reach) 22 12   550
locks/test_locks_15_false-unreach-call.c false(reach) .15 .16 29 wit false(reach) 8.7 4.8 390 false(reach) 21 12   470
locks/test_locks_10_true-unreach-call.c true .13 .13 26 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true .11 .11 26 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true .14 .14 26 wit - -
locks/test_locks_13_true-unreach-call.c true .11 .11 27 wit - -
locks/test_locks_14_true-unreach-call.c true .15 .15 29 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true .16 .16 27 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true .11 .12 24 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true .15 .15 24 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true .12 .13 25 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true .12 .13 25 wit - -
locks/test_locks_9_true-unreach-call.c true .13 .13 25 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 7100 7100 59000 48 1200   980   50000   48 390   220   8800  
    correct results 39 680 680 5700 5 1000   830   43000   16 350   200   7900  
        correct true 23 380 380 2900 3 0   0   0   0 0   0   0  
        correct false 16 300 300 2700 2 1000   830   43000   16 350   200   7900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 62
Run set sv-comp16.ControlFlow