Tool CPAchecker 1.4-svn 18356M
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-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]]
Run set sv-comp16.ControlFlow
Options -lpi-svcomp16 -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/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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 38   17   720 15   7.9 540 25 13 510
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c 20   6.7 540 14   7.4 490 26 14 520
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c 32   12   680 15   8.1 540 25 13 520
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c 9.6 3.3 410 15   8.0 540 24 15 490
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 19   4.2 520
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 46   8.5 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 13   3.2 460
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 19   4.1 530
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 4.8 1.8 240
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 7.4 2.5 260
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 24   5.4 520 11   5.8 480 21 14 500
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 26   5.7 570 15   7.8 500 22 14 500
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 25   5.3 560 14   7.6 500 20 11 490
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 28   6.1 530 12   6.6 480 22 14 490
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 8.6 2.7 360 8.4 4.6 420 19 10 400
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 43   12   990 16   8.3 500 28 15 560
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 40   11   940 15   7.8 490 24 13 520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 24   5.9 510 14   7.3 510 23 12 510
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 13   3.3 370
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 21   4.9 450 12   6.6 480 21 11 500
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 20   4.5 480 11   6.1 470 22 14 510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 8.6 2.7 360 9.8 5.4 400 20 11 370
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 30   5.7 730
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 35   6.3 840
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 34   6.2 790
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 33   6.0 780
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 900   410   4500
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 17   3.9 410
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 5.6 1.9 310
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 900   410   4700
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 900   400   4800
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 900   400   4800
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 900   400   4900
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 900   410   4700
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 900   410   4700
locks/test_locks_14_false-unreach-call.c 900   900   950
locks/test_locks_15_false-unreach-call.c 6.6 2.2 320
locks/test_locks_10_true-unreach-call.c 6.6 2.2 330
locks/test_locks_11_true-unreach-call_false-termination.c 6.9 2.2 320
locks/test_locks_12_true-unreach-call_false-termination.c 6.3 2.0 320
locks/test_locks_13_true-unreach-call.c 6.8 2.2 320
locks/test_locks_14_true-unreach-call.c 7.3 2.3 330
locks/test_locks_15_true-unreach-call_false-termination.c 7.5 2.3 330
locks/test_locks_5_true-unreach-call_false-termination.c 5.6 1.9 300
locks/test_locks_6_true-unreach-call_false-termination.c 5.9 2.0 300
locks/test_locks_7_true-unreach-call_false-termination.c 6.6 2.3 310
locks/test_locks_8_true-unreach-call_false-termination.c 5.7 1.9 320
locks/test_locks_9_true-unreach-call.c 5.9 2.1 310
../../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 7900 3900 54000 48 200   110   7300   48 340   200   7400  
    correct results 38 700 180 19000 15 200   110   7300   14 340   200   7400  
        correct true 23 340 78 10000 0 0   0   0   0 0   0   0  
        correct false 15 370 110 8600 15 200   110   7300   14 340   200   7400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 61
Run set sv-comp16.ControlFlow