Tool ULTIMATE Kojak 0.1.23-635dfa2a 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-08 11:04:44 CET 2018-12-09 20:15:59 CET 2018-12-09 20:59:07 CET 2018-12-09 21:01:30 CET 2018-12-12 21:11:08 CET 2018-12-09 19:35:17 CET 2018-12-09 20:36:45 CET
Run set ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options --full-output -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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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 timeout 0 --- inspect 900   730   1800 8400 .62 0     error (invalid witness file) 0 --- inspect .66 .41 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 48 0   0     error (invalid witness file) 0 --- inspect .0049 .0060 .52 0     0   - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   750   1300 7200 .63 0     error (invalid witness file) 0 --- inspect .71 .43 42 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .69 47 0   0     error (invalid witness file) 0 --- inspect .0050 .0066 .53 0     0   - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   740   1500 8500 .64 0     error (invalid witness file) 0 --- inspect .77 .48 41 0   0      error (2) 0 --- inspect .021 .032 5.7 0    0     error (invalid witness file) 0 --- inspect .91 .60 47 0   0     error (invalid witness file) 0 --- inspect .0042 .0054 .53 0     0   - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 52   22   1000 550 .62 0     true -32 wit inspect 9.8  5.2  400 0   0      false(unreach-call) 1 --- inspect 9.7   5.5   340   .62 0     unknown 0 --- inspect 4.9  2.8  260 0   .053 true -32 --- inspect .72   .72   21    .16  0   - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   740   1600 9900 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   750   1400 7400 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 43 0   0      error (2) 0 --- inspect .021 .031 5.6 0    0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   750   1300 7000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900   740   1300 7500 .63 .049 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 36   18   910 360 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.3  3.4  280 0   0      false(unreach-call) -16 --- inspect 21     12     530   .66 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 58   29   1100 460 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.7  3.6  270 0   0      false(unreach-call) -16 --- inspect 17     9.5   480   .66 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 420   340   3000 3600 .62 0     false(unreach-call) 1 wit inspect 6.2  3.3  260 0   .0041 false(unreach-call) 1 --- inspect 10     5.5   350   .62 0     unknown 0 --- inspect 6.2  3.4  270 0   .037 true -32 --- inspect .65   .66   22    .12  0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 510   420   2900 4200 .62 0     false(unreach-call) 1 wit inspect 6.4  3.5  260 0   0      false(unreach-call) 1 --- inspect 10     6.1   350   .62 .037 unknown 0 --- inspect 5.9  3.3  260 0   .037 true -32 --- inspect .67   .67   22    .12  0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 860   700   5000 6800 .62 0     false(unreach-call) 1 wit inspect 5.4  2.9  260 0   0      false(unreach-call) 1 --- inspect 10     6.0   370   .62 0     unknown 0 --- inspect 6.4  3.6  270 0   0     true -32 --- inspect .67   .66   22    .13  0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c timeout 0 --- inspect 900   730   5400 8500 .64 0     error (invalid witness file) 0 --- inspect .67 .40 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .63 48 0   0     error (invalid witness file) 0 --- inspect .0041 .0053 .57 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 13   4.3 490 110 .66 0     false(unreach-call) 1 wit inspect 6.6  3.6  250 0   0      false(unreach-call) 1 --- inspect 9.2   5.1   320   .66 .045 unknown 0 --- inspect 5.5  3.1  260 0   0     true -32 --- inspect .65   .65   21    .14  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   740   4500 7000 .63 .045 error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .027 .027 5.5 0    0     error (invalid witness file) 0 --- inspect .94 .66 46 0   0     error (invalid witness file) 0 --- inspect .0052 .0074 .53 0     0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 590   480   3300 4800 .62 0     false(unreach-call) 1 wit inspect 7.3  3.9  270 0   0      false(unreach-call) 1 --- inspect 12     6.6   480   .62 0     unknown 0 --- inspect 8.5  4.6  330 0   .14  true -32 --- inspect .67   .67   22    .14  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 210   160   1900 1800 .62 0     false(unreach-call) 1 wit inspect 5.5  3.0  260 0   0      false(unreach-call) 1 --- inspect 13     6.9   390   .62 0     unknown 0 --- inspect 6.7  3.6  320 0   .045 true -32 --- inspect .68   .69   21    .14  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 270   220   970 1600 .62 0     false(unreach-call) 1 wit inspect 6.3  3.4  260 0   0      false(unreach-call) 1 --- inspect 11     6.0   360   .62 0     unknown 0 --- inspect 5.3  2.9  260 0   0     true -32 --- inspect .67   .66   21    .14  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 89   51   1400 840 .62 0     false(unreach-call) 1 wit inspect 7.0  3.8  260 0   0      false(unreach-call) 1 --- inspect 10     6.0   370   .66 0     unknown 0 --- inspect 7.7  4.2  290 0   0     true -32 --- inspect .68   .67   22    .13  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 360   290   3000 3600 .62 0     false(unreach-call) 1 wit inspect 5.7  3.1  260 0   0      false(unreach-call) 1 --- inspect 10     6.1   360   .62 0     unknown 0 --- inspect 7.7  4.2  290 0   0     true -32 --- inspect .68   .68   22    .13  0   - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.8 3.1 370 77 .66 0     false(unreach-call) 1 wit inspect 6.1  3.3  260 0   0      false(unreach-call) 1 --- inspect 11     6.1   340   .62 0     unknown 0 --- inspect 4.0  2.3  250 0   0     false(unreach-call) 1 --- inspect .65   .65   21    .14  0   - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c timeout 0 --- inspect 900   720   5600 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 0 --- inspect 900   740   3900 5900 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0      error (2) 0 --- inspect .027 .027 5.5 0    0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c timeout 0 --- inspect 900   750   2400 6100 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .030 .031 5.7 0    0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c timeout 0 --- inspect 900   740   3100 6500 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   750   3500 6800 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 71   43   1200 860 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.0  4.8  390 0   .17   true 2 --- inspect 40     22     540   .62 0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 18   7.3 550 160 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  2.9  290 0   0      true 2 --- inspect 14     7.9   440   .62 0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   740   4100 6400 .65 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   730   5200 8000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   740   3100 5800 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 43 0   0      error (2) 0 --- inspect .027 .029 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   740   4200 6500 .63 .049 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   740   3800 6300 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900   730   4800 6500 .64 .045 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .028 .029 5.7 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 9.1 3.1 360 64 .66 0     false(unreach-call) 1 wit inspect 4.7  2.5  260 0   0      false(unreach-call) 1 --- inspect 8.6   4.8   310   .62 0     unknown 0 --- inspect 4.5  2.5  250 0   0     true -32 --- inspect .60   .60   21    .057 0   - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 8.5 3.0 340 64 .66 0     false(unreach-call) 1 wit inspect 4.8  2.6  250 0   0      false(unreach-call) 1 --- inspect 8.2   5.1   320   .62 0     unknown 0 --- inspect 4.5  2.6  260 0   0     true -32 --- inspect .63   .63   21    .061 0   - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 43   26   970 410 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.1  3.8  290 0   0      true 2 --- inspect 21     11     550   .62 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 51   31   890 600 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.2  3.4  300 0   0      true 2 --- inspect 29     15     890   .62 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 82   57   960 810 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.0  3.8  300 0   0      true 2 --- inspect 45     25     2100   .66 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 91   67   1100 920 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.5  3.5  300 0   .0082 true 2 --- inspect 46     28     3400   .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 130   100   950 1100 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  300 0   0      true 2 --- inspect 99     61     6100   .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 160   120   1100 1700 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.3  3.5  300 0   0      out of memory 0 --- inspect 100     65     7000   .68 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 13   4.9 580 110 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.9  3.2  290 0   0      true 2 --- inspect 9.9   6.1   320   .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 17   6.4 530 160 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  290 0   0      true 2 --- inspect 11     6.7   380   .62 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 19   8.5 710 180 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.3  2.9  290 0   0      true 2 --- inspect 13     7.4   450   .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 26   13   790 240 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.9  3.7  290 0   0      true 2 --- inspect 17     9.6   470   .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 31   17   900 360 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.5  3.0  290 0   0      true 2 --- inspect 16     8.9   500   .62 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 --- inspect 900   810   2100 8700 .64 0     error (invalid witness file) 0 --- inspect .74 .47 41 0   0      error (2) 0 --- inspect .020 .021 5.8 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0     error (invalid witness file) 0 --- inspect .0017 .0019 .40 0     0   - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 350   320   1500 4400 .62 0     assertion 0 --- inspect 5.8  3.1  270 0   .0082 timeout 0 --- inspect 96     80     3300   .65 0     assertion 0 --- inspect 5.7  3.1  280 0   0     timeout 0 --- inspect 96      96      23    .17  0   - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c error (7) 0 --- inspect 21   5.9 400 160 .75 0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0     error (invalid witness file) 0 --- inspect .98 .64 47 0   0     error (invalid witness file) 0 --- inspect .0019 .0025 .53 0     0   - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c timeout 0 --- inspect 900   830   2300 10000 .64 0     error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .65 47 0   0     error (invalid witness file) 0 --- inspect .0048 .0059 .53 0     0   - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c error (7) 0 --- inspect 390   350   2300 3000 .71 0     error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0     error (invalid witness file) 0 --- inspect .0019 .0045 .54 0     0   - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c timeout 0 --- inspect 900   830   2200 9200 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 0 --- inspect 900   760   4000 12000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 --- inspect 900   560   3300 10000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 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 (7) 0 --- inspect 21   6.6 400 170 .75 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0      error (2) 0 --- inspect .021 .023 5.7 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 --- inspect 900   670   2800 8800 .65 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.9 360 110 .75 0     error (invalid witness file) 0 --- inspect .68 .43 41 0   0      error (2) 0 --- inspect .025 .034 5.5 0    0     error (invalid witness file) 0 --- inspect .94 .60 46 0   0     error (invalid witness file) 0 --- inspect .0039 .0052 .53 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.2 340 100 .73 0     error (invalid witness file) 0 --- inspect .69 .42 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .60 47 0   0     error (invalid witness file) 0 --- inspect .0046 .0060 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.3 350 110 .73 0     error (invalid witness file) 0 --- inspect .57 .36 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0     error (invalid witness file) 0 --- inspect .0034 .0069 .48 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.2 340 110 .73 0     error (invalid witness file) 0 --- inspect .68 .41 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0     error (invalid witness file) 0 --- inspect .0049 .0062 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.6 340 100 .74 0     error (invalid witness file) 0 --- inspect .64 .39 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .62 47 0   0     error (invalid witness file) 0 --- inspect .0053 .0066 .42 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.9 350 110 .75 0     error (invalid witness file) 0 --- inspect .76 .48 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 49 0   0     error (invalid witness file) 0 --- inspect .0042 .0048 .39 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.4 320 110 .73 0     error (invalid witness file) 0 --- inspect .78 .48 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0     error (invalid witness file) 0 --- inspect .0056 .0069 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.2 340 100 .73 0     error (invalid witness file) 0 --- inspect .64 .39 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .63 49 0   0     error (invalid witness file) 0 --- inspect .0051 .0062 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   5.2 330 120 .75 0     error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .93 .59 47 0   0     error (invalid witness file) 0 --- inspect .0055 .0065 .55 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.8 350 110 .74 0     error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .62 47 0   0     error (invalid witness file) 0 --- inspect .0021 .0028 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.4 360 120 .73 0     error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .63 46 0   0     error (invalid witness file) 0 --- inspect .0049 .0056 .40 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.4 340 99 .73 0     error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .021 .031 5.5 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 50 0   0     error (invalid witness file) 0 --- inspect .0046 .0057 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.6 330 100 .74 0     error (invalid witness file) 0 --- inspect .72 .45 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .99 .66 47 0   0     error (invalid witness file) 0 --- inspect .0060 .0077 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.5 320 110 .74 0     error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .63 47 0   0     error (invalid witness file) 0 --- inspect .0049 .0062 .53 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.7 370 120 .74 0     error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0     error (invalid witness file) 0 --- inspect .0019 .0024 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.5 350 98 .74 0     error (invalid witness file) 0 --- inspect .77 .47 41 0   0      error (2) 0 --- inspect .039 .040 5.5 0    0     error (invalid witness file) 0 --- inspect .96 .64 47 0   0     error (invalid witness file) 0 --- inspect .0047 .0054 .39 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.9 350 110 .75 0     error (invalid witness file) 0 --- inspect .90 .55 42 0   0      error (2) 0 --- inspect .025 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .90 .60 47 0   0     error (invalid witness file) 0 --- inspect .0057 .0070 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.8 350 110 .75 0     error (invalid witness file) 0 --- inspect .78 .47 41 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .93 .62 47 0   0     error (invalid witness file) 0 --- inspect .0057 .0069 .52 0     0   - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.4 340 110 .73 0     error (invalid witness file) 0 --- inspect .86 .53 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .64 48 0   0     error (invalid witness file) 0 --- inspect .0024 .0033 .52 0     0   - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.7 330 120 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.6 360 110 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.3 350 100 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.3 350 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.2 360 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0      error (2) 0 --- inspect .023 .024 5.8 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.8 350 110 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.6 340 130 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.2 350 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.6 360 120 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.7 360 120 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .40 43 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.4 350 100 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (7) 0 --- inspect 13   5.3 320 110 .75 .074 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0      error (2) 0 --- inspect .033 .034 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.8 350 120 .74 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.4 360 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (7) 0 --- inspect 13   4.6 350 110 .74 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/s3_srvr.blast.15_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.3 360 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (7) 0 --- inspect 14   4.3 350 110 .73 0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .022 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 43 29000 23000 130000 250000 64    .26 42 -20 110   59   4900 0   .012  42 13 230 160 8100 8.8 .082 42 0 110 64 5200 0   .31 42 -383 110    110    310 1.8  0   52 30 120 66 6000 0   .18 52 -8 500 300 24000 9.6 0  
    correct results 28 43 4300 3200 37000 36000 18    0    12 12 72   39   3100 0   .0041 13 13 130 76 4700 8.2 .082 0 1 1 .65 .65 21 .14 0   15 30 95 52 4500 0   .18 12 24 360 210 16000 7.6 0  
        correct true 15 30 840 550 13000 8400 9.6  0    0 0 0 0 15 30 95 52 4500 0   .18 12 24 360 210 16000 7.6 0  
        correct false 13 13 3400 2700 24000 28000 8.2  0    12 12 72   39   3100 0   .0041 13 13 130 76 4700 8.2 .082 0 1 1 .65 .65 21 .14 0   0 0
    correct-unconfimed results 1 0 350 320 1500 4400 .62 0    0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 350 320 1500 4400 .62 0    0 0 0 0 0 0
    incorrect results 0 1 -32 9.8 5.2 400 0   0      0 0 12 -384 8.0  8.0  260 1.5  0   0 2 -32 38 22 1000 1.3 0  
        incorrect true 0 1 -32 9.8 5.2 400 0   0      0 0 12 -384 8.0  8.0  260 1.5  0   0 0
        incorrect false 0 0 0 0 0 0 2 -32 38 22 1000 1.3 0  
score (94 tasks, max score: 146) 43 -20 13 0 -383 30 -8
Run set ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow