Tool skink 2.0 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-07 12:00:55 CET 2018-12-07 18:03:00 CET 2018-12-07 19:11:22 CET 2018-12-07 19:49:22 CET 2018-12-12 21:02:00 CET 2018-12-07 17:09:07 CET 2018-12-07 18:50:30 CET
Run set skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-skink.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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/skink.2018-12-07_1200.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/skink.2018-12-07_1200.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 unknown 0 --- inspect 120   57   4400 1100 51     .0041 error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .67 46 0   0   error (invalid witness file) 0 --- inspect .0018 .0030 .49 0     0   - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 120   75   3000 1400 34     0      error (invalid witness file) 0 --- inspect .65 .41 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 46 0   0   error (invalid witness file) 0 --- inspect .0059 .0078 .52 0     0   - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 93   48   3600 940 40     0      error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .74 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0065 .54 0     0   - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 65   32   4300 610 42     0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .031 .032 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0074 .53 0     0   - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 120   58   4400 1200 52     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 98   45   3700 1000 25     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 120   77   3100 1300 39     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .38 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 95   49   3500 850 42     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 67   38   3900 650 44     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 --- inspect 64   31   4200 600 38     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   100   2800 1700 11     0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0080 .53 0     0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 100   74   2700 1100 24     0      error (invalid witness file) 0 --- inspect .72 .46 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .62 47 0   0   error (invalid witness file) 0 --- inspect .0060 .0081 .53 0     0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 96   65   2200 1200 38     0      error (invalid witness file) 0 --- inspect .75 .48 41 0   0   error (2) 0 --- inspect .025 .026 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 47 0   0   error (invalid witness file) 0 --- inspect .0046 .0056 .52 0     0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   97   2500 1800 2.4   0      error (invalid witness file) 0 --- inspect .79 .47 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0087 .54 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 280   230   2600 3300 35     0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0   error (invalid witness file) 0 --- inspect .0023 .0029 .52 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 18   16   490 190 .70  0      error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .63 48 0   0   error (invalid witness file) 0 --- inspect .0013 .0019 .52 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 20   17   530 190 .84  0      error (invalid witness file) 0 --- inspect .68 .43 41 0   0   error (2) 0 --- inspect .020 .021 5.8 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0082 .40 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   810   5400 10000 .045 0      error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0022 .52 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 280   250   2500 3800 100     0      error (invalid witness file) 0 --- inspect .77 .46 42 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .82 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0020 .53 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 430   370   2600 5200 28     0      error (invalid witness file) 0 --- inspect .71 .43 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .66 49 0   0   error (invalid witness file) 0 --- inspect .0052 .0065 .39 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 260   220   2800 3000 28     0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .028 .030 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0059 .010  .52 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c unknown 0 --- inspect 760   670   5100 8300 60     .0041 error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .64 46 0   0   error (invalid witness file) 0 --- inspect .0050 .0065 .53 0     0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 130   100   2600 1600 73     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 100   73   2700 1200 22     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 98   68   2700 1000 6.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c unknown 0 --- inspect 64   38   2200 670 6.9   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .038 .040 5.6 0    0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 360   300   2900 3900 90     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 49   24   1200 520 16     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 110   76   1500 1100 32     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 270   230   3500 3100 84     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .40 41 0   0   error (2) 0 --- inspect .027 .030 5.7 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 250   200   2800 3500 68     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 280   230   2800 3200 53     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 250   210   3400 3300 78     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   830   5200 9700 .049 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c unknown 0 --- inspect 240   210   3100 3100 61     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.4 2.4 320 56 .037 0      false(unreach-call) 1 wit inspect 5.2  2.8  260 0   0   true -32 --- inspect 9.1   5.3   300   .66 0   false(unreach-call) 1 --- inspect 4.6  2.6  250 0   0   false(unreach-call) 1 --- inspect .62   .61   20    .057 0   - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.5 2.4 330 59 .037 0      false(unreach-call) 1 wit inspect 5.8  3.2  260 0   0   true -32 --- inspect 7.3   4.0   310   .66 0   false(unreach-call) 1 --- inspect 4.5  2.6  250 0   0   false(unreach-call) 1 --- inspect .59   .59   20    .061 0   - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.8 1.8 240 42 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  300 0   0   true 2 --- inspect 19     11     540   .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.9 1.9 240 36 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.8  300 0   0   true 2 --- inspect 22     12     880   .62 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.8 1.8 240 34 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.2  300 0   0   true 2 --- inspect 38     21     2200   .66 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 1.9 240 41 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.5  3.5  300 0   0   true 2 --- inspect 44     27     3200   .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 1.8 240 44 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  300 0   0   true 2 --- inspect 85     54     6300   .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 1.8 240 40 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.2  300 0   0   out of memory 0 --- inspect 130     80     7000   .63 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 1.8 220 39 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  290 0   0   true 2 --- inspect 9.3   5.7   320   .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 1.9 230 39 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  290 0   0   true 2 --- inspect 12     6.4   370   .62 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 1.9 230 39 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.6  3.6  290 0   0   true 2 --- inspect 14     7.5   450   .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 1.8 230 44 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  290 0   0   true 2 --- inspect 14     7.6   460   .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.0 1.8 230 41 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  290 0   0   true 2 --- inspect 19     11     480   .66 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 --- inspect 120   44   3000 870 12     0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0073 .39 0     0   - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c unknown 0 --- inspect 110   32   2100 650 9.0   0      error (invalid witness file) 0 --- inspect .81 .49 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0054 .0068 .53 0     0   - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 0 --- inspect 58   24   1600 490 7.4   0      error (invalid witness file) 0 --- inspect .72 .44 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .60 47 0   0   error (invalid witness file) 0 --- inspect .0060 .0078 .40 0     0   - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 --- inspect 39   14   1200 350 3.9   0      error (invalid witness file) 0 --- inspect .63 .40 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0054 .0071 .53 0     0   - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 --- inspect 240   110   5100 1800 25     0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .74 47 0   0   error (invalid witness file) 0 --- inspect .0052 .0068 .52 0     0   - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 --- inspect 91   35   2400 640 12     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 --- inspect 120   39   2600 870 12     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .026 .027 5.5 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c unknown 0 --- inspect 22   19   330 260 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unknown 0 --- inspect 59   25   1700 460 7.5   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c unknown 0 --- inspect 280   110   5100 2000 26     0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unknown 0 --- inspect 17   6.2 500 160 1.1   0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .60 47 0   0   error (invalid witness file) 0 --- inspect .0027 .0034 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c unknown 0 --- inspect 18   6.2 490 180 1.1   0      error (invalid witness file) 0 --- inspect .81 .49 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0073 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c unknown 0 --- inspect 18   6.2 500 170 1.1   0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0073 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c unknown 0 --- inspect 18   6.2 490 150 1.1   0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0065 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 580 190 1.6   .0041 error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 49 0   0   error (invalid witness file) 0 --- inspect .0055 .0080 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.0 590 190 1.6   0      error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0060 .0075 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.0 600 170 1.6   0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0   0   error (invalid witness file) 0 --- inspect .0055 .0069 .40 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 590 170 1.6   0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .026 .028 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .73 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0071 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c unknown 0 --- inspect 22   7.2 620 180 1.7   0      error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0066 .0085 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 610 170 1.6   0      error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 46 0   0   error (invalid witness file) 0 --- inspect .0018 .0022 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 600 190 1.6   0      error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 48 0   0   error (invalid witness file) 0 --- inspect .0054 .014  .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 660 180 1.6   0      error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .023 .025 5.8 0    0   error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0   error (invalid witness file) 0 --- inspect .0059 .014  .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 600 200 1.6   .0041 error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0071 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c unknown 0 --- inspect 20   7.0 670 160 1.6   0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .62 49 0   0   error (invalid witness file) 0 --- inspect .0060 .0079 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 610 200 1.6   0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0040 .0061 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 690 160 1.6   .0041 error (invalid witness file) 0 --- inspect .83 .50 40 0   0   error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .67 46 0   0   error (invalid witness file) 0 --- inspect .0048 .0059 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 620 190 1.6   0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 48 0   0   error (invalid witness file) 0 --- inspect .0058 .0084 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.0 600 170 1.6   0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .63 49 0   0   error (invalid witness file) 0 --- inspect .0062 .0073 .41 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 620 170 1.7   0      error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .020 .020 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0   error (invalid witness file) 0 --- inspect .0070 .0092 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unknown 0 --- inspect 17   6.1 490 140 1.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c unknown 0 --- inspect 17   6.2 490 160 1.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c unknown 0 --- inspect 18   6.3 560 160 1.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c unknown 0 --- inspect 18   6.2 490 160 1.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.0 590 180 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 600 180 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 680 170 1.7   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 660 190 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 610 200 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 600 170 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 600 160 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .030 .031 5.6 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c unknown 0 --- inspect 22   7.2 600 180 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 610 180 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 43 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 610 180 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 620 170 1.7   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.1 610 170 1.6   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 43 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c unknown 0 --- inspect 21   7.2 660 210 1.7   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .40 41 0   0   error (2) 0 --- inspect .020 .020 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 24 9400 6800   160000 100000 1500     .029 42 2 39 23   2100 0   0   42 -64 17 10   840 1.3 0   42 2 51   32   2400 0   0   42 2 1.4 1.5 61 .12 0   52 22 86 49 4900 0   0   52 20 410 240 22000 7.1 0  
    correct results 13 24 58 25   3200 550 .48  0     2 2 11 6.0 520 0   0   0 2 2 9.2 5.2 510 0   0   2 2 1.2 1.2 41 .12 0   11 22 62 34 3200 0   0   10 20 280 160 15000 6.4 0  
        correct true 11 22 45 20   2600 440 .41  0     0 0 0 0 11 22 62 34 3200 0   0   10 20 280 160 15000 6.4 0  
        correct false 2 2 13 4.9 650 120 .074 0     2 2 11 6.0 520 0   0   0 2 2 9.2 5.2 510 0   0   2 2 1.2 1.2 41 .12 0   0 0
    incorrect results 0 0 2 -64 16 9.3 620 1.3 0   0 0 0 0
        incorrect true 0 0 2 -64 16 9.3 620 1.3 0   0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 24 2 -64 2 2 22 20
Run set skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-skink.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow