Tool CBMC Path 5.10 () 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*
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-04 22:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 07:24:45 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml -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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 0 86    86    140   1100   13      0      0 .63 .39 40 0   0   0 .024 .025 5.6 0    0   0 .94 .59 47 0   0     0 .0052 .0064 .53 0     0     - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .49 .48 46   6.0 .066  0      -32 7.1  3.8  290 0   0   1 16     9.0   510   .66 0   0 6.0  3.3  280 0   .29  -32 .77   .78   21    .21  0     - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .86 .85 72   10   .066  0      -32 7.0  3.8  280 0   0   1 15     8.6   480   .62 0   0 7.2  4.0  290 0   4.9   -32 .83   .83   21    .27  0     - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .37 .36 20   4.4 .14   0      -32 6.9  3.7  260 0   0   1 12     6.3   340   .66 0   1 5.2  2.9  280 0   1.3   1 .74   .74   21    .18  0     - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 7.7  7.7  140   100   .0082 0      - - - - 0 .67 .40 43 0   0   0 5.8   3.4   270   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 880    880    700   10000   4.6    0      - - - - 0 .57 .37 40 0   0   0 .023 .025 5.7 0    0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 2.5  2.5  100   36   .0082 0      - - - - 0 .67 .41 44 0   0   0 5.0   2.8   260   .61 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 5.6  5.6  170   65   .0082 0      - - - - 0 .77 .47 42 0   0   0 5.4   2.9   270   .61 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 .53 .53 15   6.0 .0082 0      - - - - 0 .80 .49 42 0   0   0 6.1   3.3   270   .33 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 1.0  1.0  22   12   .0082 0      - - - - 0 .62 .38 43 0   0   0 6.9   3.9   260   .65 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 14    14    1600   170   1.8    0      -32 5.4  2.9  270 0   0   1 11     5.8   340   .62 0   0 6.4  3.5  290 0   4.7   -32 .73   .73   21    .15  0     - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 14    14    1600   210   1.8    0      -32 6.7  3.6  260 0   0   1 10     5.7   340   .66 0   0 6.9  3.8  270 0   4.4   -32 .75   .74   21    .15  0     - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 15    15    1800   200   1.8    0      -32 6.9  3.6  280 0   0   1 10     6.0   360   .66 0   0 7.0  3.8  280 0   0     -32 .76   .75   21    .17  0     - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 14    14    1700   170   1.8    0      -32 6.8  3.6  280 0   0   1 9.4   5.6   350   .66 0   0 6.3  3.5  290 0   .029 -32 .75   .76   21    .16  .037 - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 .17 .16 12   1.4 .0082 0      -32 7.7  4.1  280 0   0   1 9.8   5.4   320   .66 0   0 5.6  3.1  270 0   4.4   1 .73   .73   21    .17  0     - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 110    110    15000   1200   .033  .0041 0 .61 .39 41 0   0   0 .023 .024 5.6 0    0   0 .97 .63 49 0   0     0 .0021 .0027 .54 0     0     - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 110    110    15000   1400   .033  .0041 0 .70 .43 42 0   0   0 .025 .026 5.6 0    0   0 .93 .61 46 0   0     0 .0042 .0067 .52 0     0     - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 0 110    110    15000   1300   3.3    .0041 0 .60 .37 41 0   0   0 .027 .028 5.6 0    0   0 .95 .62 47 0   0     0 .0043 .0054 .53 0     0     - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 0 1.1  1.1  170   14   .21   0      0 3.9  2.1  200 0   0   1 11     6.3   370   .66 0   0 3.5  2.0  200 0   0     0 .56   .56   21    .045 0     - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 2.0  2.0  150   22   .18   0      -32 8.3  4.4  280 0   0   1 9.9   5.7   360   .66 0   0 7.5  4.1  310 0   0     -32 .71   .71   21    .16  0     - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 2.0  2.0  160   28   .18   0      -32 6.6  3.5  280 0   0   1 10     5.5   350   .62 0   0 7.5  4.1  300 0   0     -32 .77   .77   21    .16  0     - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 .11 .11 9.5 1.3 .0082 0      -32 8.0  4.3  260 0   0   1 9.6   5.4   330   .62 0   0 4.9  2.8  270 0   0     1 .70   .69   21    .15  0     - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 0 160    160    15000   1500   .025  0      - - - - 0 .57 .35 41 0   0   0 .025 .025 5.6 0    0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 160    160    15000   1800   .025  0      - - - - 0 .76 .46 41 0   0   0 .022 .025 5.6 0    0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 0 160    160    15000   2100   .025  .0041 - - - - 0 .80 .50 41 0   0   0 .024 .025 5.7 0    0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 0 160    160    15000   2000   .025  0      - - - - 0 .60 .37 41 0   0   0 .029 .030 5.6 0    0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 110    110    15000   1400   .033  0      - - - - 0 .76 .49 42 0   0   0 .027 .029 5.7 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 170    170    15000   2200   130      0      - - - - 0 .77 .47 41 0   0   0 .027 .028 5.6 0    0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 880    880    540   9300   720      0      - - - - 0 .66 .40 40 0   0   0 .022 .022 5.6 0    0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 110    110    15000   1300   .033  0      - - - - 0 .68 .42 41 0   0   0 .022 .023 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 110    110    15000   1300   .033  .0041 - - - - 0 .71 .44 41 0   0   0 .023 .023 5.6 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 110    110    15000   1400   .033  .0041 - - - - 0 .79 .48 41 0   0   0 .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 110    110    15000   1300   .033  0      - - - - 0 .73 .44 40 0   0   0 .025 .026 5.6 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 110    110    15000   1300   .033  0      - - - - 0 .69 .42 40 0   0   0 .023 .024 5.7 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 110    110    15000   1400   .033  0      - - - - 0 .73 .45 40 0   0   0 .023 .024 5.7 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 140    140    14000   1900   380      0      -32 5.3  2.9  250 0   0   1 8.2   5.1   310   .62 0   1 4.9  2.8  260 0   0     1 .66   .66   21    .090 0     - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 83    83    15000   1000   .033  0      0 .61 .39 41 0   0   0 .022 .023 5.6 0    0   0 .99 .67 48 0   0     0 .0061 .0077 .52 0     0     - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 170    170    15000   2400   540      0      - - - - 0 .59 .37 41 0   0   0 .021 .022 5.6 0    0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 160    160    15000   2100   510      0      - - - - 0 .77 .47 40 0   0   0 .025 .026 5.5 0    0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 160    160    15000   2000   470      0      - - - - 0 .66 .41 41 0   0   0 .025 .026 5.7 0    0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 140    140    15000   1600   350      0      - - - - 0 .59 .36 40 0   0   0 .022 .024 5.7 0    0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 110    110    15000   1400   180      0      - - - - 0 .73 .45 41 0   0   0 .033 .036 5.6 0    0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 83    83    15000   1000   .029  0      - - - - 0 .71 .44 41 0   0   0 .027 .028 5.6 0    0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 0 150    150    15000   2200   540      0      - - - - 0 .76 .46 41 0   0   0 .023 .024 5.7 0    0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 0 83    83    15000   1100   9.8    0      - - - - 0 .58 .35 40 0   0   0 .027 .033 5.6 0    0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 90    90    15000   1100   33      0      - - - - 0 .82 .49 41 0   0   0 .028 .030 5.6 0    0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 110    110    15000   1400   110      0      - - - - 0 .73 .45 41 0   0   0 .027 .030 5.6 0    0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 180    180    15000   2400   380      0      - - - - 0 .73 .45 40 0   0   0 .021 .022 5.7 0    0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 880    880    520   9100   180      0      0 .82 .50 41 0   0   0 .021 .021 5.6 0    0   0 .95 .60 48 0   0     0 .0052 .0063 .52 0     0     - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 .36 .35 28   3.9 .016  0      -32 8.2  4.3  300 0   0   0 97     79     2500   .66 0   0 6.9  3.8  290 0   .15  0 96      96      21    .17  0     - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 .59 .58 43   6.8 .016  0      -32 13    6.8  460 0   0   0 18     10     370   .71 0   0 7.8  4.3  300 0   4.9   0 96      96      21    .27  0     - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 3.7  3.7  110   42   .012  0      0 .70 .43 42 0   0   0 .026 .028 5.7 0    0   0 .95 .63 47 0   0     0 .0048 .0061 .53 0     0     - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 .65 .64 51   6.8 .016  0      -32 13    6.7  340 0   0   0 96     78     3200   1.8  0   0 9.3  5.1  320 0   .11  0 1.3    1.3    25    .32  0     - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 81    81    390   880   .070  0      - - - - 0 .84 .51 43 0   0   0 7.1   3.8   260   .65 0  
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 520    520    15000   3400   .033  0      - - - - 0 .66 .42 40 0   0   0 .028 .028 5.6 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 530    530    15000   5100   9.4    0      - - - - 0 .69 .42 40 0   0   0 .026 .026 5.6 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 120    120    4900   960   .016  0      - - - - 0 .74 .45 41 0   0   0 .028 .029 5.6 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c 0 280    280    15000   3000   .033  .0041 - - - - 0 .57 .35 40 0   0   0 .023 .024 5.6 0    0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 310    310    15000   2600   .029  .0041 0 .77 .47 41 0   0   0 .022 .022 5.6 0    0   0 1.2  .77 46 0   0     0 .0050 .0064 .53 0     0     - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 310    310    15000   2400   .029  0      0 .81 .50 40 0   0   0 .021 .022 5.6 0    0   0 .95 .62 47 0   0     0 .0048 .0062 .52 0     0     - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 290    290    15000   2800   .029  0      0 .65 .40 41 0   0   0 .022 .022 5.6 0    0   0 1.0  .67 46 0   0     0 .0022 .0028 .52 0     0     - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 280    280    15000   3100   .029  0      0 .76 .46 40 0   0   0 .026 .026 5.6 0    0   0 1.1  .72 47 0   0     0 .0057 .0080 .53 0     0     - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 260    260    15000   2700   .029  0      0 .75 .46 41 0   0   0 .023 .023 5.6 0    0   0 .92 .60 46 0   0     0 .0044 .0058 .52 0     0     - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 260    260    15000   2400   .029  .0041 0 .62 .38 40 0   0   0 .021 .023 5.6 0    0   0 .98 .64 46 0   0     0 .0042 .0056 .52 0     0     - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 280    280    15000   2400   .029  .0041 0 .61 .37 43 0   0   0 .021 .022 5.6 0    0   0 .97 .62 47 0   0     0 .0015 .0022 .52 0     0     - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 280    280    15000   2100   .029  0      0 .76 .46 40 0   0   0 .025 .027 5.6 0    0   0 .98 .65 47 0   0     0 .0048 .0066 .53 0     0     - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 260    260    15000   2800   .029  0      0 .66 .41 41 0   0   0 .028 .028 5.6 0    0   0 .93 .62 47 0   0     0 .0019 .0024 .53 0     0     - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 260    260    15000   3000   .029  0      0 .76 .47 41 0   0   0 .022 .023 5.6 0    0   0 .93 .60 47 0   0     0 .0058 .0074 .53 0     0     - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 280    280    15000   2100   .029  0      0 .78 .46 41 0   0   0 .022 .024 5.6 0    0   0 .94 .61 46 0   0     0 .0048 .0060 .52 0     0     - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 270    270    15000   2200   .029  0      0 .60 .37 40 0   0   0 .021 .022 5.6 0    0   0 .95 .62 47 0   0     0 .0057 .0071 .52 0     0     - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 260    260    15000   3000   .029  0      0 .74 .45 41 0   0   0 .026 .027 5.6 0    0   0 .93 .60 47 0   0     0 .0027 .0034 .52 0     0     - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 280    280    15000   2400   .029  .0041 0 .65 .40 40 0   0   0 .022 .022 5.6 0    0   0 .92 .60 46 0   0     0 .0061 .0077 .53 0     0     - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 260    260    15000   2200   .029  .0041 0 .65 .41 42 0   0   0 .021 .022 5.7 0    0   0 1.0  .67 46 0   0     0 .0035 .0048 .53 0     0     - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 270    270    15000   2000   .029  0      0 .72 .47 41 0   0   0 .021 .023 5.6 0    0   0 .93 .62 47 0   0     0 .0021 .0026 .53 0     0     - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 270    270    15000   1700   .029  .0041 0 .74 .46 40 0   0   0 .021 .023 5.6 0    0   0 1.0  .68 48 0   0     0 .0017 .0028 .53 0     0     - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 280    280    15000   2100   .029  .0041 0 .68 .41 42 0   0   0 .022 .023 5.7 0    0   0 .95 .62 47 0   0     0 .0047 .0053 .40 0     0     - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 270    270    15000   1900   .029  0      0 .75 .45 42 0   0   0 .026 .028 5.7 0    0   0 .94 .62 48 0   0     0 .0053 .0068 .52 0     0     - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 310    310    15000   2800   .029  0      - - - - 0 .59 .36 41 0   0   0 .026 .027 5.7 0    0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 290    290    15000   2300   .029  0      - - - - 0 .78 .47 40 0   0   0 .021 .023 5.7 0    0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 310    310    15000   2200   .029  0      - - - - 0 .66 .41 42 0   0   0 .021 .022 5.6 0    0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 290    290    15000   2500   .029  0      - - - - 0 .78 .47 41 0   0   0 .026 .027 5.6 0    0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 240    240    15000   3100   .029  0      - - - - 0 .61 .39 42 0   0   0 .027 .029 5.6 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 280    280    15000   2300   .029  0      - - - - 0 .59 .35 40 0   0   0 .021 .021 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 280    280    15000   2000   .029  0      - - - - 0 .58 .37 40 0   0   0 .022 .022 5.6 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 270    270    15000   2300   .029  0      - - - - 0 .75 .45 40 0   0   0 .020 .020 5.6 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 270    270    15000   2300   .029  0      - - - - 0 .66 .41 42 0   0   0 .022 .022 5.6 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 280    280    15000   2300   .029  0      - - - - 0 .68 .43 41 0   0   0 .033 .034 5.7 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 280    280    15000   1800   .029  0      - - - - 0 .57 .35 40 0   0   0 .024 .026 5.7 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 260    260    15000   2200   .029  0      - - - - 0 .59 .37 40 0   0   0 .021 .022 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 280    280    15000   2200   .029  0      - - - - 0 .62 .38 41 0   0   0 .023 .025 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 280    280    15000   2500   .029  0      - - - - 0 .74 .45 42 0   0   0 .024 .025 5.6 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 270    270    15000   2300   .029  0      - - - - 0 .62 .38 40 0   0   0 .025 .026 5.8 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 260    260    15000   2300   .029  .0041 - - - - 0 .73 .45 41 0   0   0 .022 .024 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 250    250    15000   2500   .029  0      - - - - 0 .59 .35 41 0   0   0 .025 .026 5.6 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 12 18000   18000   1000000 180000 4600    .061 42 -480 140 75 5600 0   0   42 13 350 250 11000 11   0   42 2 130 73   5700 0   25   42 -252 200   200   350 2.8  .037 52 0 36 22 2100 0   0   52 0 37 21 1900 3.5 0  
    correct results 12 12 210   210   22000 2700 390    0     0 13 13 140 80 4700 8.4 0   2 2 10 5.7 550 0   1.3 4 4 2.8 2.8 83 .59 0     0 0
        correct true 0 0 0 0 0 0 0
        correct false 12 12 210   210   22000 2700 390    0     0 13 13 140 80 4700 8.4 0   2 2 10 5.7 550 0   1.3 4 4 2.8 2.8 83 .59 0     0 0
    correct-unconfimed results 4 0 2.7 2.6 290 31 .26 0     0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 2.7 2.6 290 31 .26 0     0 0 0 0 0 0
    incorrect results 0 15 -480 120 62 4400 0   0   0 0 8 -256 6.1 6.1 170 1.4  .037 0 0
        incorrect true 0 15 -480 120 62 4400 0   0   0 0 8 -256 6.1 6.1 170 1.4  .037 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 12 -480 13 2 -252 0 0
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow