Tool symbiotic 3.0.1
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-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 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/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.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 witness unconfirmed 550    550    69   wit true 17   9.0 740 unknown 9.9 6.0 310
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 420    420    20   wit false(reach) 19   10   590 unknown 9.7 6.1 300
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c timeout 900    900    37   wit - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 350    350    15   wit false(reach) 17   9.3 600 unknown 9.3 5.9 310
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c timeout 900    900    69   wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c timeout 900    900    20   wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c timeout 900    900    20   wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c timeout 900    900    37   wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 230    230    9.3 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 620    620    15   wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c witness unconfirmed 660    660    22   wit true 14   7.6 510 unknown 9.2 5.2 310
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c witness unconfirmed 700    700    23   wit true 11   6.2 410 unknown 9.6 5.7 310
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness unconfirmed 650    650    26   wit true 22   12   830 unknown 9.7 5.5 320
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c witness unconfirmed 770    770    22   wit true 11   6.0 400 unknown 8.5 5.8 300
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c witness unconfirmed 18    18    22   wit true 9.5 5.2 340 unknown 8.9 5.4 310
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c timeout 900    900    23   wit - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c timeout 900    900    26   wit - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c timeout 900    900    23   wit - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 120    120    23   wit false(reach) 13   6.9 510 unknown 9.2 5.1 330
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 670    670    22   wit false(reach) 14   7.4 490 unknown 9.5 5.5 320
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 570    570    22   wit false(reach) 15   7.8 500 unknown 9.5 5.6 310
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) .79 .82 25   wit false(reach) 9.1 4.9 390 unknown 8.7 5.5 300
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 900    900    23   wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c timeout 900    900    26   wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 900    900    23   wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c timeout 900    900    7.8 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c timeout 900    900    7.0 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900    900    25   wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900    900    22   wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900    900    23   wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 3.3  3.4  120   wit false(reach) 8.3 4.7 390 unknown 9.4 7.3 310
locks/test_locks_15_false-unreach-call.c false(reach) 6.8  6.9  250   wit false(reach) 8.8 4.9 360 unknown 9.3 7.4 300
locks/test_locks_10_true-unreach-call.c timeout 900    900    170   wit - -
locks/test_locks_11_true-unreach-call_false-termination.c timeout 900    900    170   wit - -
locks/test_locks_12_true-unreach-call_false-termination.c timeout 900    900    190   wit - -
locks/test_locks_13_true-unreach-call.c timeout 900    900    220   wit - -
locks/test_locks_14_true-unreach-call.c timeout 900    900    290   wit - -
locks/test_locks_15_true-unreach-call_false-termination.c timeout 900    900    510   wit - -
locks/test_locks_5_true-unreach-call_false-termination.c timeout 900    900    25   wit - -
locks/test_locks_6_true-unreach-call_false-termination.c timeout 900    900    160   wit - -
locks/test_locks_7_true-unreach-call_false-termination.c timeout 900    900    530   wit - -
locks/test_locks_8_true-unreach-call_false-termination.c timeout 900    900    320   wit - -
locks/test_locks_9_true-unreach-call.c timeout 900    900    220   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 35000 35000 4000 48 190   100   7100   48 130   82   4300  
    correct results 10 3000 3000 510 8 100   56   3800   0 75   48   2500  
        correct true 2 850 850 24 0 0   0   0   0 0   0   0  
        correct false 8 2100 2100 490 8 100   56   3800   0 75   48   2500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 12
Run set sv-comp16.ControlFlow