Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 09:26:28 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .45 .45 51 6.3 1.0  0      1 6.2  3.3  270 0   0   -32 12     7.2   400   .66 0   0 5.4  3.1  270 0   0   -32 .82   .82   20    .29  .070 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .24 .24 38 4.0 1.0  0      1 5.2  2.8  270 0   0   -32 10     5.9   320   .62 0   0 4.6  2.6  260 0   0   -32 .69   .69   20    .19  0     - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .33 .33 41 4.1 1.0  0      1 5.6  3.0  270 0   0   -32 12     7.0   360   .62 0   0 4.9  2.8  270 0   0   -32 .75   .75   20    .24  0     - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .22 .22 38 2.9 1.0  0      1 6.3  3.4  260 0   0   -32 8.8   5.0   310   .66 0   0 4.7  2.7  260 0   0   -32 .70   .70   20    .16  0     - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 2.0  1.8  66 24   31    0      - - - - 2 9.5  5.2  520 0   0   2 110     65     1000   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 1.3  .98 66 15   31    0      - - - - 0 520    500    7000 0   0   2 68     39     880   .62 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 1.2  .90 66 12   31    0      - - - - 2 8.9  4.9  360 0   0   2 87     48     830   .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 1.5  1.3  67 18   31    0      - - - - 2 9.4  5.1  450 0   0   2 79     45     880   .62 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 .89 .64 67 9.9 31    0      - - - - 2 5.0  2.7  260 0   0   2 22     12     550   .62 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 1.0  .75 66 11   31    0      - - - - 2 5.9  3.2  270 0   0   2 20     11     530   .66 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 5.0  5.0  64 64   150    0      1 6.3  3.4  270 0   0   -32 8.7   5.3   320   .62 0   0 5.5  3.1  270 0   0   -32 .66   .65   20    .12  .037 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 5.1  5.0  65 56   150    0      1 6.7  3.6  260 0   0   -32 9.0   5.1   320   .62 0   0 4.7  2.7  260 0   0   -32 .64   .64   20    .12  0     - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 5.8  5.7  72 82   150    0      1 6.5  3.5  270 0   0   -32 8.4   4.8   310   .62 0   0 4.9  2.8  260 0   0   -32 .69   .68   20    .13  0     - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 5.2  5.1  65 74   150    0      1 5.4  2.9  270 0   0   -32 8.5   5.2   310   .62 0   0 4.9  2.8  270 0   0   -32 .65   .65   21    .12  0     - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 .16 .16 36 2.6 1.0  0      1 4.6  2.5  260 0   0   -32 9.8   5.8   300   .62 0   0 4.4  2.5  260 0   0   -32 .68   .68   20    .14  0     - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 1 9.0  9.0  79 110   180    0      1 6.0  3.2  280 0   0   -32 9.0   5.1   320   .62 0   0 5.0  2.8  270 0   0   -32 .68   .68   21    .14  .045 - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 1 8.1  8.0  82 110   150    0      1 5.7  3.0  280 0   0   -32 8.6   4.9   300   .62 0   0 5.4  3.0  280 0   0   -32 .67   .67   21    .14  0     - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 3.7  3.7  56 63   77    0      1 6.5  3.5  280 0   0   -32 8.6   5.2   310   .62 0   0 4.9  2.8  260 0   0   -32 .68   .69   21    .14  0     - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 .74 .74 40 9.5 31    0      1 5.6  3.0  270 0   0   -32 8.5   5.1   310   .62 0   0 4.9  2.8  270 0   0   -32 .68   .68   20    .14  0     - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 2.6  2.6  55 33   92    0      1 5.5  3.0  270 0   0   -32 9.2   5.2   310   .62 0   0 4.8  2.7  260 0   0   -32 .69   .70   21    .14  .045 - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 2.6  2.5  53 33   92    0      1 6.5  3.5  270 0   0   -32 8.7   5.2   310   .62 0   0 4.7  2.7  270 0   0   -32 .65   .65   21    .14  0     - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 .15 .15 36 1.9 1.0  0      1 4.4  2.4  260 0   0   1 9.8   5.5   330   .62 0   0 4.5  2.6  250 0   0   1 .65   .65   20    .14  0     - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 0 36    36    170 500   360    .0041 - - - - 2 16    9.0  540 0   0   2 35     19     840   .62 0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 37    37    180 510   430    0      - - - - 2 16    8.7  560 0   0   2 38     21     930   .62 0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 0 42    41    200 520   430    .0041 - - - - 2 14    7.9  580 0   0   2 37     21     990   .62 0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 0 37    37    180 470   410    0      - - - - 2 12    7.3  540 0   0   2 38     21     900   .62 0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 900    900    390 14000   1500    .0041 - - - - 0 .61 .38 42 0   0   0 .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 280    280    120 3500   3000    .012  - - - - 0 .61 .37 41 0   0   0 .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 110    110    78 1500   2800    .012  - - - - 0 .71 .44 40 0   0   0 .023 .024 5.6 0    0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 900    900    380 12000   1500    .0041 - - - - 0 .63 .39 42 0   0   0 .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 900    900    390 10000   1500    0      - - - - 0 .62 .38 40 0   0   0 .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 900    900    390 11000   1500    .0041 - - - - 0 .66 .41 40 0   0   0 .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 900    900    420 12000   1400    0      - - - - 0 .68 .41 42 0   0   0 .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 900    900    400 11000   1500    0      - - - - 0 .73 .45 40 0   0   0 .025 .026 5.6 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 900    900    390 12000   1400    0      - - - - 0 .74 .44 40 0   0   0 .021 .022 5.6 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 .15 .15 34 1.7 1.0  0      1 5.0  2.8  260 0   0   -32 7.4   4.2   310   .62 0   1 3.8  2.2  250 0   0   1 .59   .59   20    .057 0     - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 .15 .15 35 1.5 1.0  0      1 4.7  2.6  260 0   0   -32 7.8   4.4   310   .62 0   1 3.8  2.2  250 0   0   1 .61   .61   20    .061 0     - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 .99 .72 66 12   31    0      - - - - 2 5.4  3.0  300 0   0   2 21     12     620   .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 1.0  .77 67 10   31    0      - - - - 2 5.1  2.8  290 0   0   2 25     13     920   .62 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 1.0  .79 67 11   31    0      - - - - 2 5.9  3.2  300 0   0   2 31     18     2200   .62 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 1.1  .83 67 14   31    0      - - - - 2 5.7  3.1  300 0   0   2 50     30     3800   .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 1.2  .90 68 14   31    0      - - - - 2 5.7  3.2  300 0   0   2 80     50     5900   .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 1.2  .93 74 15   31    0      - - - - 2 7.0  3.8  300 0   0   0 150     92     7000   1.0  0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 0 .86 .61 66 8.9 26    0      - - - - 2 4.7  2.7  280 0   0   2 9.4   5.4   320   .62 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 0 .88 .63 66 7.8 31    0      - - - - 2 5.0  2.8  290 0   0   2 14     7.7   370   .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 .89 .63 67 9.4 31    0      - - - - 2 5.5  3.0  290 0   0   2 13     7.0   440   .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 .96 .69 66 9.7 31    0      - - - - 2 5.2  2.9  290 0   0   2 14     8.0   530   .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 .96 .69 67 11   26    0      - - - - 2 5.5  3.0  290 0   0   2 16     8.9   480   .62 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 900    900    760 12000   1500    .0041 0 .59 .37 40 0   0   0 .022 .023 5.6 0    0   0 .92 .60 47 0   0   0 .0023 .0030 .53 0     0     - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 1.8  1.8  120 23   1.0  0      -32 9.4  4.9  300 0   0   -32 61     50     3200   .62 0   0 5.9  3.2  290 0   0   0 96      96      21    .17  0     - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 4.6  4.6  370 56   1.0  0      0 5.5  2.9  270 0   0   0 18     9.9   370   .75 0   0 5.8  3.2  280 0   0   0 96      97      21    .28  0     - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 190    190    600 2200   980    0      0 .70 .43 42 0   0   0 .048 .053 5.5 0    0   0 .95 .64 49 0   0   0 .0053 .0070 .54 0     0     - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 7.5  7.5  390 92   .85 0      0 7.8  4.1  270 0   0   0 93     77     2800   .62 0   0 6.9  3.7  280 0   0   0 1.3    1.3    25    .32  .34  - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 560    560    690 7200   1000    0      - - - - 0 .66 .41 41 0   0   0 .027 .028 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 49    49    100 590   1500    .0082 - - - - 0 .66 .40 42 0   0   0 .021 .022 5.7 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 900    900    1100 11000   18    0      - - - - 0 .62 .39 42 0   0   0 .022 .023 5.6 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 900    900    730 12000   21    0      - - - - 0 .61 .39 40 0   0   0 .021 .023 5.6 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c 0 360    360    13000 4000   33    0      - - - - 0 15    7.6  660 0   0   0 960     870     3500   .63 0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 1 30    30    400 390   180    0      1 9.9  5.4  330 0   0   0 12     6.9   290   .75 0   0 5.3  3.0  270 0   0   0 .72   .72   21    .098 0     - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 23    23    350 230   130    0      1 8.1  4.4  300 0   0   0 13     7.6   280   .75 0   0 5.5  3.1  260 0   0   0 .76   .76   21    .29  0     - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 23    23    350 280   150    0      1 9.4  5.0  290 0   0   0 14     7.8   290   .71 0   0 5.2  3.0  260 0   0   0 .77   .77   21    .29  0     - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 23    23    350 280   150    0      1 9.4  5.0  330 0   0   0 13     7.6   290   .75 0   0 5.4  3.0  270 0   0   0 .75   .76   21    .29  0     - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 1 15    15    270 180   92    0      1 6.9  3.7  280 0   0   0 13     7.7   290   .75 0   0 5.1  2.9  260 0   0   0 .72   .71   21    .11  0     - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 1 16    16    270 220   92    0      1 6.9  3.7  290 0   0   0 12     7.2   290   .71 0   0 5.3  3.0  270 0   0   -32 .80   .81   20    .30  0     - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 1 16    16    270 180   92    0      1 7.3  4.0  300 0   0   0 13     7.9   300   .71 0   0 5.2  2.9  270 0   0   -32 .77   .77   20    .30  0     - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 1 16    16    270 190   92    0      1 8.8  4.7  290 0   0   0 13     7.9   280   .71 0   0 5.3  3.0  270 0   0   -32 .75   .75   21    .30  0     - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 1 39    39    410 460   150    0      1 10    5.4  300 0   0   0 13     7.5   300   .68 0   0 5.4  3.0  270 0   0   -32 .76   .76   21    .30  0     - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 1 38    38    410 490   130    0      1 8.3  4.4  310 0   0   0 14     8.3   300   .71 0   0 5.5  3.1  270 0   0   -32 .76   .76   21    .30  0     - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 1 120    120    700 1400   270    0      1 9.0  4.9  340 0   0   0 12     7.5   290   .71 0   0 7.7  4.3  270 0   0   -32 .83   .83   21    .30  0     - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 1 38    38    410 470   150    0      1 7.6  4.1  290 0   0   0 13     7.3   290   .68 0   0 5.6  3.1  260 0   0   -32 .75   .75   20    .30  0     - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 1 120    120    700 1400   270    0      1 10    5.5  340 0   0   0 13     7.5   290   .71 0   0 5.6  3.1  270 0   0   -32 .76   .76   21    .30  0     - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 26    26    350 300   120    0      -32 16    8.5  440 0   0   0 12     6.8   280   .75 0   0 5.6  3.1  270 0   0   -32 .76   .77   21    .30  0     - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 1 38    38    410 460   150    0      1 8.1  4.4  300 0   0   0 13     7.6   290   .75 0   0 5.7  3.2  270 0   0   -32 .78   .78   21    .30  0     - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 1 38    38    410 560   150    0      1 8.6  4.6  320 0   0   0 13     7.7   290   .68 0   0 5.3  3.0  270 0   0   -32 .76   .76   20    .30  0     - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 1 38    38    410 470   150    0      1 8.9  4.8  300 0   0   0 13     7.5   290   .71 0   0 5.3  3.0  270 0   0   -32 .76   .77   21    .30  0     - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 1 120    120    700 1400   270    0      1 9.4  5.1  340 0   0   0 14     7.7   300   .71 0   0 6.0  3.3  270 0   0   -32 .76   .76   21    .30  0     - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 1 38    38    400 470   140    0      1 8.1  4.4  290 0   0   0 12     7.1   290   .71 0   0 5.4  3.0  270 0   0   -32 .75   .75   21    .30  .078 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 150    150    1400 1800   430    0      - - - - 0 900    890    1700 0   0   0 13     7.2   290   .75 0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 190    190    1500 2300   430    0      - - - - 0 900    890    1700 0   0   0 12     7.2   290   .68 0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 180    180    1500 2200   430    0      - - - - 0 900    890    1600 0   0   0 13     7.7   290   .75 0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 180    180    1500 2600   430    0      - - - - 0 900    890    1700 0   0   0 12     7.1   290   .75 0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900    900    1900 11000   790    0      - - - - 0 .59 .36 41 0   0   0 .027 .027 5.6 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900    900    2000 11000   760    0      - - - - 0 .61 .38 41 0   0   0 .020 .021 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900    900    1900 12000   740    0      - - - - 0 .59 .37 41 0   0   0 .022 .023 5.7 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900    900    2000 12000   740    0      - - - - 0 .60 .37 41 0   0   0 .022 .023 5.6 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900    900    2000 11000   740    0      - - - - 0 .61 .38 40 0   0   0 .020 .021 5.6 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900    900    2000 11000   740    0      - - - - 0 .60 .38 41 0   0   0 .020 .021 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900    900    1900 12000   740    0      - - - - 0 .66 .40 40 0   0   0 .022 .023 5.6 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900    900    2000 11000   740    0      - - - - 0 .77 .47 40 0   0   0 .021 .022 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900    900    1900 10000   740    0      - - - - 0 .57 .36 41 0   0   0 .023 .025 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900    900    2000 10000   720    0      - - - - 0 .63 .39 40 0   0   0 .020 .021 5.6 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900    900    1900 12000   710    0      - - - - 0 .62 .37 42 0   0   0 .024 .025 5.6 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900    900    1900 10000   730    0      - - - - 0 .61 .37 40 0   0   0 .021 .022 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900    900    1900 12000   730    0      - - - - 0 .76 .47 42 0   0   0 .021 .022 5.7 0    0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 94 36 24000 24000 63000 300000 39000 .057 42 -28 300 160 12000 0   0   42 -575 580   380   18000 27    0   42 2 210   120   11000 0   0   42 -925 220   220   830 8.6  .61 52 40 4300 4200 23000 0   0   52 40 2000 1500 36000 17 0  
    correct results 36 36 840 840 8400 10000 4100 0     36 36 260 140 10000 0   0   1 1 9.8 5.5 330 .62 0   2 2 7.6 4.4 500 0   0   3 3 1.9 1.9 61 .26 0    20 40 160 88 7300 0   0   20 40 810 460 24000 13 0  
        correct true 0 0 0 0 0 20 40 160 88 7300 0   0   20 40 810 460 24000 13 0  
        correct false 36 36 840 840 8400 10000 4100 0     36 36 260 140 10000 0   0   1 1 9.8 5.5 330 .62 0   2 2 7.6 4.4 500 0   0   3 3 1.9 1.9 61 .26 0    0 0
    correct-unconfimed results 4 0 40 40 1200 470 120 0     0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 40 40 1200 470 120 0     0 0 0 0 0 0
    incorrect results 0 2 -64 26 13 740 0   0   18 -576 220   140   8700 11    0   0 29 -928 21   21   600 6.5  .27 0 0
        incorrect true 0 2 -64 26 13 740 0   0   18 -576 220   140   8700 11    0   0 29 -928 21   21   600 6.5  .27 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 36 -28 -575 2 -925 40 40
Run set depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow