Tool ULTIMATE Kojak fd30d3d8
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-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set sv-comp16.ControlFlow
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.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 timeout 140 930   1800 wit - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c timeout 120 930   1800 wit - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c timeout 120 930   1500 wit - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 39 13   780 wit false(reach) 14   7.8 510 false(reach) 21 12   480
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c timeout 120 930   2300 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c timeout 150 930   1900 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c timeout 110 930   2200 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c timeout 99 930   1400 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 36 9.4 750 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 56 21   1000 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c timeout 35 930   580 wit - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c timeout 38 930   580 wit - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c timeout 40 930   810 wit - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c timeout 36 930   700 wit - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 14 4.1 350 wit false(reach) 10   5.8 400 false(reach) 17 9.4 390
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c timeout 65 930   1600 wit - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c timeout 38 930   740 wit - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c timeout 61 930   1300 wit - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 17 4.9 370 wit false(reach) 12   6.3 440 false(reach) 20 11   450
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 15 4.2 370 wit timeout 91   71   3700 false(reach) 19 11   500
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 15 4.3 470 wit false(reach) 12   6.6 450 false(reach) 19 11   500
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 13 3.8 420 wit false(reach) 9.8 5.4 410 false(reach) 16 9.1 360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c timeout 34 930   570 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 37 930   710 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c timeout 37 930   640 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 35 930   690 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 54 930   1100 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 55 25   1400 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 22 6.1 430 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 55 930   1200 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 44 930   890 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 54 930   840 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 29 930   690 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 56 930   1200 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 45 930   1000 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 11 3.3 330 wit false(reach) 8.7 5.0 370 false(reach) 15 8.1 350
locks/test_locks_15_false-unreach-call.c false(reach) 12 3.6 340 wit false(reach) 8.9 4.9 380 false(reach) 15 8.2 360
locks/test_locks_10_true-unreach-call.c true 16 5.4 380 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 20 7.0 420 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 22 7.2 510 wit - -
locks/test_locks_13_true-unreach-call.c true 24 8.9 620 wit - -
locks/test_locks_14_true-unreach-call.c true 26 9.2 620 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 27 11   630 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 13 3.6 370 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 13 3.7 340 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 15 4.2 450 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 15 4.4 490 wit - -
locks/test_locks_9_true-unreach-call.c true 16 5.2 350 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 2200 23000 41000 48 170   110   6700   48 140   79   3400  
    correct results 23 510 170 12000 7 170   110   6700   8 140   79   3400  
        correct true 15 380 130 8800 0 0   0   0   0 0   0   0  
        correct false 8 140 41 3400 7 170   110   6700   8 140   79   3400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 38
Run set sv-comp16.ControlFlow