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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.ControlFlow
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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) 11   3.4 450 wit false(reach) 15   8.0 550 false(reach) 27 14   510
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 13   3.9 480 wit false(reach) 14   7.4 510 false(reach) 32 18   560
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 14   4.3 540 wit false(reach) 15   7.9 540 false(reach) 34 22   540
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 9.2 2.9 320 wit false(reach) 15   8.2 540 false(reach) 23 12   500
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 10   3.5 430 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 110   92   2300 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 10   3.4 440 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 11   3.8 470 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 4.3 1.7 210 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 6.3 2.1 280 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 8.5 2.6 350 wit false(reach) 12   6.5 450 false(reach) 21 11   490
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 10   3.1 350 wit false(reach) 12   6.5 460 false(reach) 19 11   490
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 8.6 2.7 360 wit false(reach) 12   6.4 480 unknown 18 9.9 470
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 10   3.1 350 wit false(reach) 12   6.6 460 false(reach) 22 16   390
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 18   8.2 690 wit false(reach) 10   5.7 380 false(reach) 18 12   390
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 160   100   2700 wit false(reach) 14   7.8 520 false(reach) 25 14   530
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 160   100   3900 wit false(reach) 16   8.7 540 false(reach) 23 12   520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 130   91   3800 wit false(reach) 13   7.1 470 false(reach) 21 11   510
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 76   49   3700 wit false(reach) 12   6.4 440 false(reach) 19 10   450
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 7.8 2.4 310 wit false(reach) 12   6.5 450 false(reach) 21 11   500
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 9.3 2.9 310 wit false(reach) 11   6.1 430 false(reach) 21 12   510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 5.2 2.1 230 wit false(reach) 8.8 4.9 390 false(reach) 18 12   360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 26   16   1300 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 29   17   1300 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 32   20   1300 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 27   16   1800 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 33   22   2300 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 3.7 1.5 210 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2.9 1.3 190 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 36   23   2300 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 34   23   2300 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 35   23   2300 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 120   98   3600 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 100   85   3600 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 34   23   2300 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 95   83   3600 wit false(reach) 7.2 4.0 270 false(reach) 16 8.9 350
locks/test_locks_15_false-unreach-call.c false(reach) 96   82   2400 wit false(reach) 6.9 3.8 270 false(reach) 17 9.9 340
locks/test_locks_10_true-unreach-call.c true 33   24   2300 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 160   140   3600 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 160   140   3600 wit - -
locks/test_locks_13_true-unreach-call.c true 160   140   3500 wit - -
locks/test_locks_14_true-unreach-call.c true 160   140   2500 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 160   140   3600 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 4.2 1.5 220 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 5.5 2.0 230 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 7.2 2.8 330 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 9.6 3.4 650 wit - -
locks/test_locks_9_true-unreach-call.c true 18   8.0 690 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 2400 1800 75000 48 220   120   8100   48 400   230   8400  
    correct results 48 2400 1800 75000 18 220   120   8100   17 400   230   8400  
        correct true 30 1500 1200 50000 0 0   0   0   0 0   0   0  
        correct false 18 850 550 25000 18 220   120   8100   17 400   230   8400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 78
Run set sv-comp16.ControlFlow