Tool CPAchecker 1.4-svn 18373
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-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.ControlFlow
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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) 79   57   900 wit false(reach) 13   7.1 550 false(reach) 26 14   520
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 97   74   820 wit false(reach) 11   6.0 480 false(reach) 30 17   560
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 120   91   830 wit false(reach) 14   7.3 510 false(reach) 33 19   550
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 10   3.4 440 wit false(reach) 13   6.9 470 false(reach) 22 12   460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 370   340   820 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 170   150   820 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 90   75   800 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 120   96   830 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 5.6 2.3 240 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 7.9 2.9 300 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 10   3.4 440 wit false(reach) 12   6.3 440 false(reach) 19 10   510
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 11   3.5 450 wit false(reach) 10   5.6 430 false(reach) 20 11   490
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 11   3.5 460 wit false(reach) 11   6.0 440 unknown 20 14   480
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 11   3.6 450 wit false(reach) 11   6.0 440 false(reach) 20 11   480
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 38   11   930 wit false(reach) 8.9 4.9 420 false(reach) 18 10   400
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 71   29   1500 wit false(reach) 15   7.8 520 false(reach) 25 14   530
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 540   490   1200 wit false(reach) 14   7.3 470 false(reach) 23 13   520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 660   610   1500 wit false(reach) 13   6.8 450 false(reach) 24 13   520
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 50   20   1500 wit false(reach) 11   6.2 450 false(reach) 21 11   470
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 8.8 2.8 430 wit false(reach) 11   5.8 420 false(reach) 21 11   510
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 8.2 2.7 430 wit false(reach) 11   5.9 430 false(reach) 21 13   430
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 5.8 2.3 260 wit false(reach) 9.4 5.2 380 false(reach) 18 12   360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 33   7.7 800 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 32   7.8 880 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 32   7.3 870 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 35   8.0 850 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 260   230   890 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 4.0 1.7 230 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 3.8 1.7 210 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 210   180   880 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 350   320   980 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 320   290   1300 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 390   350   1000 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 440   400   1400 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 390   350   1100 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 17   4.9 700 wit false(reach) 7.2 4.0 370 false(reach) 16 9.0 360
locks/test_locks_15_false-unreach-call.c false(reach) 20   4.7 760 wit false(reach) 7.1 3.9 350 false(reach) 18 9.6 350
locks/test_locks_10_true-unreach-call.c true 340   290   2700 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c timeout 900   840   2800 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c timeout 900   840   1300 wit - -
locks/test_locks_13_true-unreach-call.c timeout 900   860   1500 wit - -
locks/test_locks_14_true-unreach-call.c timeout 900   860   1500 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c timeout 900   860   1100 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 4.9 2.0 230 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 6.4 2.3 270 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 6.7 2.4 300 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 13   3.7 580 wit - -
locks/test_locks_9_true-unreach-call.c true 140   120   1400 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 10000 8900 43000 48 200   110   8000   48 390   220   8500  
    correct results 43 5500 4600 35000 18 200   110   8000   17 390   220   8500  
        correct true 25 3800 3200 21000 0 0   0   0   0 0   0   0  
        correct false 18 1800 1400 14000 18 200   110   8000   17 390   220   8500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 68
Run set sv-comp16.ControlFlow