Tool CPAchecker 1.4-svcomp16c
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 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.ControlFlow
Options -sv-comp16--k-induction -disable-java-assertions -heap 10000m -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-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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) 52   19   1100 wit false(reach) 15   8.1 560 false(reach) 26 14 510
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 31   8.4 800 wit false(reach) 14   7.6 510 false(reach) 26 14 520
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 39   13   1000 wit false(reach) 15   8.2 550 false(reach) 24 13 510
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 7.8 3.0 390 wit false(reach) 14   7.8 540 false(reach) 22 13 470
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 41   7.5 960 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 26   5.4 800 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 19   4.3 600 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 25   5.2 760 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 5.3 2.1 230 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 6.4 2.4 250 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 33   6.9 920 wit false(reach) 13   7.1 480 false(reach) 22 13 500
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 34   6.8 910 wit false(reach) 10   5.6 480 false(reach) 21 12 510
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 36   7.2 950 wit false(reach) 13   7.4 500 unknown 18 11 480
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 34   7.0 910 wit false(reach) 15   8.2 520 false(reach) 20 12 500
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 8.6 2.8 370 wit false(reach) 11   5.7 430 false(reach) 18 10 390
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 51   14   1000 wit false(reach) 14   7.3 510 false(reach) 25 14 550
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 53   14   1200 wit false(reach) 14   7.5 510 false(reach) 24 14 520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 31   6.8 880 wit false(reach) 14   7.4 480 false(reach) 21 12 500
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 17   4.0 550 wit false(reach) 9.6 5.2 450 false(reach) 20 11 450
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 30   5.8 780 wit false(reach) 12   6.2 470 false(reach) 22 12 510
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 27   5.7 680 wit false(reach) 11   6.0 500 false(reach) 23 13 510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 6.9 2.3 370 wit false(reach) 10   5.6 410 false(reach) 19 10 380
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 35   6.5 900 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 34   6.4 890 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 43   7.9 1000 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 36   6.8 900 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 33   6.2 900 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 7.5 2.3 390 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 4.9 1.8 270 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 33   6.4 860 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 38   7.1 940 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 36   6.8 890 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 54   11   1300 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 50   10   1200 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 34   6.1 890 wit - -
locks/test_locks_14_false-unreach-call.c timeout 900   890   970 wit - -
locks/test_locks_15_false-unreach-call.c timeout 900   890   1200 wit - -
locks/test_locks_10_true-unreach-call.c true 7.2 2.3 290 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 6.4 2.0 300 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 6.9 2.1 350 wit - -
locks/test_locks_13_true-unreach-call.c true 7.4 2.2 330 wit - -
locks/test_locks_14_true-unreach-call.c true 10   2.9 480 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 11   3.1 450 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 5.0 1.8 260 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 5.2 1.9 270 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 6.2 2.2 270 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 6.8 2.3 290 wit - -
locks/test_locks_9_true-unreach-call.c true 5.8 2.0 280 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 2900 2100 34000 48 200   110   7900   48 350   200   7800  
    correct results 46 1100 260 31000 16 200   110   7900   15 350   200   7800  
        correct true 30 640 140 19000 0 0   0   0   0 0   0   0  
        correct false 16 490 130 13000 16 200   110   7900   15 350   200   7800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 76
Run set sv-comp16.ControlFlow