Tool CBMC 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:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 false(unreach-call) 1 wit inspect .99 .98 120   11   .0082 0      false(unreach-call) 1 wit inspect 8.0 4.2 300 0   0   false(unreach-call) 1 --- inspect 13   7.5 450 .62 0   false(unreach-call) 1 --- inspect 6.8 3.7 290 0   0     false(unreach-call) 1 --- inspect .86 .86 21 .33  0      - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 17   2.7 .0082 0      false(unreach-call) 1 wit inspect 6.5 3.5 290 0   0   false(unreach-call) 1 --- inspect 14   8.1 470 .66 0   unknown 0 --- inspect 5.6 3.2 270 0   0     true -32 --- inspect .79 .78 21 .21  .033  - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .42 39   6.0 .0082 0      false(unreach-call) 1 wit inspect 8.2 4.4 290 0   0   false(unreach-call) 1 --- inspect 18   10   470 .62 0   unknown 0 --- inspect 5.7 3.2 270 0   0     true -32 --- inspect .80 .80 21 .27  .049  - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 13   1.9 .0082 0      false(unreach-call) 1 wit inspect 6.5 3.4 280 0   0   false(unreach-call) 1 --- inspect 9.9 5.9 330 .66 0   false(unreach-call) 1 --- inspect 5.7 3.1 280 0   .053 false(unreach-call) 1 --- inspect .77 .77 21 .18  0      - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.8  1.8  120   19   .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    7.4  620 0   0   true 2 --- inspect 100     60     1100   .62 0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 0 --- inspect 880    880    5600   4200   6.7    .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31 .30 18   3.2 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    5.4  490 0   0   true 2 --- inspect 71     40     840   .62 .0082
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .68 .68 39   8.2 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    6.7  540 0   0   true 2 --- inspect 100     58     890   .62 0     
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .12 .11 7.1 1.1 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  270 0   0   true 2 --- inspect 24     13     510   .66 0     
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .18 .18 10   2.2 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.3  3.4  280 0   0   true 2 --- inspect 24     13     520   .66 0     
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  65   16   .10   0      false(unreach-call) 1 wit inspect 7.2 3.9 270 0   0   false(unreach-call) 1 --- inspect 10   5.9 330 .66 0   unknown 0 --- inspect 6.6 3.7 270 0   0     false(unreach-call) 1 --- inspect .75 .74 21 .15  0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.4  1.4  66   17   .10   0      false(unreach-call) 1 wit inspect 6.8 3.7 290 0   0   false(unreach-call) 1 --- inspect 10   5.8 330 .66 0   unknown 0 --- inspect 6.3 3.5 280 0   0     false(unreach-call) 1 --- inspect .73 .73 21 .15  0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.7  1.7  77   20   .11   0      false(unreach-call) 1 wit inspect 7.6 4.0 270 0   0   false(unreach-call) 1 --- inspect 12   6.6 350 .66 0   unknown 0 --- inspect 6.9 3.8 280 0   0     false(unreach-call) 1 --- inspect .77 .76 21 .17  0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  66   17   .11   0      false(unreach-call) 1 wit inspect 7.2 3.8 280 0   0   false(unreach-call) 1 --- inspect 12   7.2 350 .66 0   unknown 0 --- inspect 7.0 3.9 290 0   0     false(unreach-call) 1 --- inspect .75 .75 21 .16  .037  - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12 .11 9.6 1.2 .0082 0      false(unreach-call) 1 wit inspect 4.9 2.6 260 0   0   false(unreach-call) 1 --- inspect 10   5.7 330 .62 0   unknown 0 --- inspect 5.5 3.0 270 0   0     false(unreach-call) 1 --- inspect .73 .73 21 .17  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12    12    270   130   .49   0      false(unreach-call) 1 wit inspect 8.7 4.6 300 0   0   false(unreach-call) 1 --- inspect 14   7.7 540 .62 0   unknown 0 --- inspect 11   6.3 440 0   .13  false(unreach-call) 1 --- inspect .78 .78 22 .18  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.5  2.5  120   31   .13   0      false(unreach-call) 1 wit inspect 6.6 3.5 270 0   0   false(unreach-call) 1 --- inspect 11   6.5 410 .62 0   unknown 0 --- inspect 9.7 5.2 390 0   0     false(unreach-call) 1 --- inspect .78 .77 22 .19  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.3  2.3  120   28   .098  0      false(unreach-call) 1 wit inspect 6.6 3.5 290 0   0   false(unreach-call) 1 --- inspect 12   6.7 380 .62 0   unknown 0 --- inspect 7.1 3.9 290 0   0     false(unreach-call) 1 --- inspect .73 .73 21 .16  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .12 .11 9.8 1.3 .0082 0      false(unreach-call) 1 wit inspect 5.7 3.0 280 0   0   false(unreach-call) 1 --- inspect 13   7.5 370 .66 0   unknown 0 --- inspect 6.2 3.4 280 0   0     false(unreach-call) 1 --- inspect .75 .75 21 .16  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.2  2.2  110   32   .11   0      false(unreach-call) 1 wit inspect 7.3 3.9 270 0   0   false(unreach-call) 1 --- inspect 12   6.8 360 .66 0   unknown 0 --- inspect 8.9 4.8 350 0   0     false(unreach-call) 1 --- inspect .77 .78 21 .16  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.1  2.1  100   26   .11   0      false(unreach-call) 1 wit inspect 7.6 4.1 280 0   0   false(unreach-call) 1 --- inspect 13   7.2 360 .66 0   unknown 0 --- inspect 8.9 4.8 350 0   0     false(unreach-call) 1 --- inspect .74 .74 21 .16  0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .13 .12 9.5 1.0 .0082 0      false(unreach-call) 1 wit inspect 6.1 3.3 260 0   0   false(unreach-call) 1 --- inspect 10   5.7 320 .66 0   unknown 0 --- inspect 5.4 3.0 270 0   0     false(unreach-call) 1 --- inspect .69 .68 21 .15  0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    310   260   1.8    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 300    290    4300 0   0   true 2 --- inspect 48     27     850   .62 0     
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    320   250   1.8    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 250    240    4900 0   0   true 2 --- inspect 50     27     1000   .66 0     
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 26    26    360   310   2.0    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 320    310    4300 0   0   true 2 --- inspect 48     27     910   .62 0     
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 22    22    320   260   1.9    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 260    250    4900 0   0   true 2 --- inspect 58     32     930   .62 0     
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    690   6300   9.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0   error (2) 0 --- inspect .022 .023 5.8 0    0     
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    930   7300   5.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0     
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    2400   6600   7.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    980   5000   9.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    970   4000   9.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0     
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    970   5000   9.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0     
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    990   5200   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0     
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    1000   6500   9.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0     
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c error (42) 0 --- inspect 880    880    980   5600   9.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .16 .15 9.2 1.7 .0082 0      false(unreach-call) 1 wit inspect 6.0 3.2 260 0   0   false(unreach-call) 1 --- inspect 10   5.9 310 .62 0   false(unreach-call) 1 --- inspect 4.3 2.5 250 0   0     false(unreach-call) 1 --- inspect .66 .65 21 .090 0      - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .14 .13 9.2 1.5 .0082 0      false(unreach-call) 1 wit inspect 5.5 3.0 260 0   0   false(unreach-call) 1 --- inspect 8.8 5.0 310 .62 0   false(unreach-call) 1 --- inspect 4.3 2.5 260 0   0     false(unreach-call) 1 --- inspect .66 .66 21 .094 .0082 - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    960   7600   9.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0     
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    1100   7600   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0     
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    1400   11000   12      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 870    880    1500   8800   12      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    1800   11000   13      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 40 0   0   error (2) 0 --- inspect .026 .027 5.7 0    0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    2000   8300   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    1000   7700   13      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    1400   8800   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 870    880    1900   8500   17      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0     
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    2300   9100   7.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .024 .026 5.6 0    0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 --- inspect 880    880    2400   8700   8.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0     
ntdrivers/cdaudio_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 120    120    3700   1200   23      0      error (invalid witness file) 0 --- inspect 9.7 5.0 370 0   0   timeout 0 --- inspect 97   80   2400 .68 0   error (invalid witness file) 0 --- inspect 9.1 4.8 380 0   0     error (1) 0 --- inspect 1.6  1.6  35 .34  0      - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.7  1.7  110   23   .016  0      timeout 0 wit inspect 94   78   2100 0   0   true -32 --- inspect 88   64   3000 .62 0   unknown 0 --- inspect 12   6.0 450 0   0     timeout 0 --- inspect 96    96    22 .16  0      - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 2.4  2.4  95   29   .016  0      false(unreach-call) 1 wit inspect 19   12   530 0   0   error (7) 0 --- inspect 19   11   370 .71 0   unknown 0 --- inspect 9.0 4.9 290 0   0     timeout 0 --- inspect 96    96    21 .27  0      - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect .96 .95 42   15   .012  0      true -32 wit inspect 12   6.3 460 0   0   true -32 --- inspect 61   44   1400 .62 0   unknown 0 --- inspect 6.5 3.6 290 0   .041 error (1) 0 --- inspect .79 .80 21 .13  0      - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 20    20    760   220   .016  0      unknown 0 wit inspect 13   6.6 400 0   0   timeout 0 --- inspect 96   79   3100 1.2  0   unknown 0 --- inspect 21   13   830 0   0     error (1) 0 --- inspect 1.3  1.3  27 .32  0      - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 25    25    190   300   .50   0      - --- inspect - --- inspect - --- inspect - --- inspect assertion 0 --- inspect 11    5.5  320 0   0   true 2 --- inspect 660     590     3200   .62 0     
ntdrivers/diskperf_true-unreach-call.i.cil.c out of memory 0 --- inspect 590    590    12000   5200   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (42) 0 --- inspect 880    880    3800   12000   41      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0     
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (42) 0 --- inspect 880    880    5100   10000   330      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0     
ntdrivers/parport_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    5300   7000   70      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .031 .032 5.6 0    0     
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 16    16    410   230   .48   0      false(unreach-call) 1 wit inspect 10   5.6 330 0   0   error (7) 0 --- inspect 13   7.6 300 .75 0   unknown 0 --- inspect 7.4 4.1 290 0   0     error (2) 0 --- inspect .75 .75 21 .098 0      - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  180   81   .090  0      false(unreach-call) 1 wit inspect 9.2 4.9 300 0   0   error (7) 0 --- inspect 12   7.3 290 .71 0   unknown 0 --- inspect 6.7 3.7 270 0   0     error (2) 0 --- inspect .75 .75 21 .098 0      - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  180   65   .090  0      false(unreach-call) 1 wit inspect 8.6 4.6 330 0   0   error (7) 0 --- inspect 14   8.2 290 .68 0   unknown 0 --- inspect 6.7 3.7 280 0   0     error (2) 0 --- inspect .75 .75 21 .098 0      - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.2  5.2  180   72   .090  0      false(unreach-call) 1 wit inspect 9.9 5.3 300 0   0   error (7) 0 --- inspect 15   8.7 290 .68 0   unknown 0 --- inspect 7.1 3.9 280 0   0     error (2) 0 --- inspect .75 .75 21 .098 0      - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   92   .098  0      false(unreach-call) 1 wit inspect 8.2 4.4 280 0   0   error (7) 0 --- inspect 14   7.8 300 .75 0   unknown 0 --- inspect 8.8 4.7 350 0   0     error (2) 0 --- inspect .77 .76 21 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   94   .090  0      false(unreach-call) 1 wit inspect 7.7 4.1 290 0   0   error (7) 0 --- inspect 14   8.5 300 .75 0   unknown 0 --- inspect 8.2 4.4 310 0   0     error (2) 0 --- inspect .79 .79 21 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   98   .10   0      false(unreach-call) 1 wit inspect 7.9 4.2 300 0   0   error (7) 0 --- inspect 13   7.3 290 .75 0   unknown 0 --- inspect 9.4 5.1 360 0   0     error (2) 0 --- inspect .78 .78 21 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   110   .090  0      false(unreach-call) 1 wit inspect 7.8 4.1 300 0   0   error (7) 0 --- inspect 15   8.4 290 .75 0   unknown 0 --- inspect 8.2 4.4 320 0   0     error (2) 0 --- inspect .76 .76 21 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.3  7.3  230   100   .11   0      false(unreach-call) 1 wit inspect 7.9 4.2 300 0   0   error (7) 0 --- inspect 16   9.3 300 .75 0   unknown 0 --- inspect 10   5.6 430 0   0     error (2) 0 --- inspect .78 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.2  7.2  230   100   .13   0      false(unreach-call) 1 wit inspect 9.7 5.1 300 0   0   error (7) 0 --- inspect 15   8.8 290 .68 0   unknown 0 --- inspect 12   6.5 430 0   0     error (2) 0 --- inspect .79 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 25    25    450   390   .59   0      false(unreach-call) 1 wit inspect 13   6.8 360 0   0   error (7) 0 --- inspect 14   8.0 300 .68 0   unknown 0 --- inspect 13   7.5 440 0   0     error (2) 0 --- inspect .80 .80 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.2  7.2  230   97   .13   0      false(unreach-call) 1 wit inspect 8.5 4.6 290 0   0   error (7) 0 --- inspect 14   7.9 300 .71 0   unknown 0 --- inspect 11   5.8 440 0   0     error (2) 0 --- inspect .77 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 25    25    450   280   .57   0      false(unreach-call) 1 wit inspect 13   6.9 360 0   0   error (7) 0 --- inspect 17   9.2 300 .71 0   unknown 0 --- inspect 12   6.9 430 0   0     error (2) 0 --- inspect .79 .79 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.2  7.2  230   120   .11   0      false(unreach-call) 1 wit inspect 8.3 4.4 310 0   0   error (7) 0 --- inspect 15   8.8 280 .75 0   unknown 0 --- inspect 9.7 5.2 360 0   .29  error (2) 0 --- inspect .78 .78 21 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   100   .13   0      false(unreach-call) 1 wit inspect 11   5.5 300 0   0   error (7) 0 --- inspect 12   7.4 290 .75 0   unknown 0 --- inspect 10   5.7 430 0   0     error (2) 0 --- inspect .78 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.1  7.1  230   100   .11   0      false(unreach-call) 1 wit inspect 8.2 4.4 300 0   0   error (7) 0 --- inspect 14   8.4 290 .31 0   unknown 0 --- inspect 11   6.0 430 0   0     error (2) 0 --- inspect .77 .77 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.2  7.2  230   96   .13   0      false(unreach-call) 1 wit inspect 11   5.7 300 0   0   error (7) 0 --- inspect 13   7.6 290 .68 0   unknown 0 --- inspect 12   6.5 430 0   0     error (2) 0 --- inspect .79 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 25    25    450   310   .58   0      false(unreach-call) 1 wit inspect 10   5.5 350 0   0   error (7) 0 --- inspect 13   7.8 290 .75 0   unknown 0 --- inspect 15   8.1 440 0   0     error (2) 0 --- inspect .79 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 7.3  7.3  230   110   .13   0      false(unreach-call) 1 wit inspect 8.5 4.5 290 0   0   error (7) 0 --- inspect 13   7.1 290 .75 0   unknown 0 --- inspect 11   6.4 440 0   0     error (2) 0 --- inspect .79 .78 22 .11  0      - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 49    49    560   660   2.5    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1900 0   0   error (7) 0 --- inspect 36     21     440   .71 0     
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 48    48    530   600   2.3    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1900 0   0   error (7) 0 --- inspect 40     22     440   .71 0     
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 48    48    530   560   2.3    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1800 0   0   error (7) 0 --- inspect 32     18     430   .71 0     
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 48    48    530   640   2.3    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    2100 0   0   error (7) 0 --- inspect 35     20     430   .75 0     
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1600   6300   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0     
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   6800   9.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0   error (2) 0 --- inspect .022 .025 5.6 0    0     
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   6100   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0     
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   7000   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0     
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   6000   9.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1600   6100   10      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .50 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   7000   9.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0     
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1600   6600   9.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   4800   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0     
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1600   9000   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0     
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   7600   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0     
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   7100   9.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .027 .029 5.7 0    0     
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (42) 0 --- inspect 880    880    1500   6600   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .027 .027 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 62 34000 34000 95000 280000 840   .14 42 6 450 270   15000 0   0   42 -46 840 550 23000 29   0   42 4 370 200 15000 0   .51  42 -48 220   220   920 6.4  .13  52 18 4800 4700 30000 0   0   52 20 1300 970 13000 9.2 .0082
    correct results 48 58 340 340 8000 4400 13   0    38 38 320 170   11000 0   0   18 18 210 120 6800 12   0   4 4 21 12 1100 0   .053 16 16 12   12   340 2.7  .045 9 18 1200 1100 21000 0   0   10 20 1200 890 11000 6.3 .0082
        correct true 10 20 120 120 1700 1400 8.0 0    0 0 0 0 9 18 1200 1100 21000 0   0   10 20 1200 890 11000 6.3 .0082
        correct false 38 38 220 220 6300 3000 5.3 0    38 38 320 170   11000 0   0   18 18 210 120 6800 12   0   4 4 21 12 1100 0   .053 16 16 12   12   340 2.7  .045 0 0
    correct-unconfimed results 8 4 330 330 6700 3900 32   0    0 0 0 0 0 0
        correct-unconfirmed true 4 4 190 190 2100 2500 9.5 0    0 0 0 0 0 0
        correct-unconfirmed false 4 0 140 140 4600 1500 23   0    0 0 0 0 0 0
    incorrect results 0 1 -32 12 6.3 460 0   0   2 -64 150 110 4400 1.2 0   0 2 -64 1.6 1.6 42 .48 .082 0 0
        incorrect true 0 1 -32 12 6.3 460 0   0   2 -64 150 110 4400 1.2 0   0 2 -64 1.6 1.6 42 .48 .082 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 62 6 -46 4 -48 18 20
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow