Tool Pinaka 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
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-06 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 16:17:05 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-pinaka.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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 1.4  1.4  160 18   .0041 0     false(unreach-call) 1 wit inspect 6.2  3.3  290 0   0   false(unreach-call) 1 --- inspect 16     9.1   440   .62 0   false(unreach-call) 1 --- inspect 6.7  3.7  270 0   0   false(unreach-call) 1 --- inspect .88   .88   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 1.1  1.1  120 17   .0041 0     false(unreach-call) 1 wit inspect 6.1  3.3  270 0   0   false(unreach-call) 1 --- inspect 19     11     530   .66 0   false(unreach-call) 1 --- inspect 5.9  3.2  270 0   0   false(unreach-call) 1 --- inspect .77   .77   21    .22  .033 - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 1.4  1.4  170 19   .0041 0     false(unreach-call) 1 wit inspect 6.0  3.2  270 0   0   false(unreach-call) 1 --- inspect 16     9.3   530   .62 0   false(unreach-call) 1 --- inspect 6.0  3.3  290 0   0   false(unreach-call) 1 --- inspect .84   .83   21    .27  0     - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .78 .78 72 8.4 .0041 0     false(unreach-call) 1 wit inspect 5.7  3.1  270 0   0   false(unreach-call) 1 --- inspect 12     6.5   350   .66 0   false(unreach-call) 1 --- inspect 5.4  3.0  270 0   0   false(unreach-call) 1 --- inspect .74   .74   21    .18  0     - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.8  5.8  1200 87   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.5  5.1  520 0   0   true 2 --- inspect 120     67     1000   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900    900    560 5100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 4.8  4.8  740 56   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.4  4.0  360 0   0   true 2 --- inspect 77     43     870   .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.9  6.9  1200 89   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.4  4.6  430 0   0   true 2 --- inspect 93     52     870   .62 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .79 .79 89 8.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.2  3.3  270 0   0   true 2 --- inspect 22     12     480   .62 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.5  1.5  160 18   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.8  3.7  270 0   0   true 2 --- inspect 21     12     530   .62 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4  2.4  500 34   .0041 0     false(unreach-call) 1 wit inspect 6.1  3.2  290 0   0   false(unreach-call) 1 --- inspect 10     5.9   360   .66 0   unknown 0 --- inspect 8.3  4.5  310 0   0   true -32 --- 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 2.4  2.4  510 29   .0041 0     false(unreach-call) 1 wit inspect 6.1  3.3  280 0   0   false(unreach-call) 1 --- inspect 11     5.9   350   .66 0   unknown 0 --- inspect 7.9  4.3  310 0   0   true -32 --- inspect .74   .73   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.6  2.6  590 30   .0041 0     false(unreach-call) 1 wit inspect 6.2  3.3  290 0   0   false(unreach-call) 1 --- inspect 13     7.3   380   .62 0   unknown 0 --- inspect 7.3  4.0  300 0   0   error (2) 0 --- inspect .73   .72   21    .074 0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4  2.4  530 29   .0041 0     false(unreach-call) 1 wit inspect 6.8  3.7  300 0   0   false(unreach-call) 1 --- inspect 13     7.3   360   .62 0   unknown 0 --- inspect 8.0  4.3  300 0   0   true -32 --- inspect .74   .73   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .46 .46 61 5.0 .0041 0     false(unreach-call) 1 wit inspect 4.8  2.6  270 0   0   false(unreach-call) 1 --- inspect 12     6.3   330   .66 0   unknown 0 --- inspect 5.8  3.3  270 0   0   false(unreach-call) 1 --- inspect .74   .74   21    .18  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.1  9.1  2200 140   .0041 0     false(unreach-call) 1 wit inspect 6.7  3.5  300 0   0   false(unreach-call) 1 --- inspect 15     7.8   560   .66 0   unknown 0 --- inspect 14    7.7  320 0   0   true -32 --- inspect .76   .76   22    .18  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .86 .86 110 13   .0041 0     false(unreach-call) 1 wit inspect 17    9.2  540 0   0   false(unreach-call) 1 --- inspect 15     8.3   480   .66 0   unknown 0 --- inspect 13    6.7  430 0   0   true -32 --- inspect .79   .79   21    .18  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .85 .85 100 11   .0041 0     false(unreach-call) 1 wit inspect 5.8  3.1  290 0   0   false(unreach-call) 1 --- inspect 12     6.6   390   .62 0   unknown 0 --- inspect 10    5.5  320 0   0   true -32 --- inspect .75   .75   21    .17  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .53 .52 67 5.1 .0041 0     false(unreach-call) 1 wit inspect 5.3  2.8  270 0   0   false(unreach-call) 1 --- inspect 13     7.2   350   .62 0   unknown 0 --- inspect 6.6  3.6  280 0   0   false(unreach-call) 1 --- inspect .71   .71   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .75 .75 100 8.3 .0041 0     false(unreach-call) 1 wit inspect 6.3  3.4  280 0   0   false(unreach-call) 1 --- inspect 10     6.0   370   .66 0   unknown 0 --- inspect 12    6.2  360 0   0   false(unreach-call) 1 --- inspect .75   .76   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .78 .78 110 8.1 .0041 0     false(unreach-call) 1 wit inspect 5.9  3.2  280 0   0   false(unreach-call) 1 --- inspect 12     6.8   370   .62 0   unknown 0 --- inspect 11    6.1  350 0   0   true -32 --- inspect .76   .76   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 62 5.9 .0041 0     false(unreach-call) 1 wit inspect 4.8  2.6  270 0   0   false(unreach-call) 1 --- inspect 12     6.9   320   .66 0   unknown 0 --- inspect 6.1  3.4  270 0   0   false(unreach-call) 1 --- inspect .70   .71   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c out of memory 0 --- inspect 44    44    15000 550   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .025 .026 5.5 0    0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c out of memory 0 --- inspect 44    44    15000 730   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c out of memory 0 --- inspect 44    44    15000 570   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c out of memory 0 --- inspect 44    44    15000 560   .037  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 50    50    15000 690   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 43 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900    900    5900 5800   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 53    53    15000 650   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 700   .053  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 680   .066  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_4_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 800   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .025 .035 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 600   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 730   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c out of memory 0 --- inspect 49    48    15000 650   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 43 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    2100 12000   .016  0     error (invalid witness file) 0 --- inspect .64 .39 42 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0040 .0050 .54 0     0     - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    2200 14000   .016  0     error (invalid witness file) 0 --- inspect .57 .37 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 46 0   0   error (invalid witness file) 0 --- inspect .0021 .0046 .53 0     0     - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1700 11000   .016  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  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1900 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .42 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1900 13000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    2000 14000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    2100 11000   .016  .057 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    2200 14000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .39 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1200 14000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 44 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1300 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1400 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1500 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 43 0   0   error (2) 0 --- inspect .025 .027 5.7 0    0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900    900    1600 12000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c error (8) 0 --- inspect 1.5  1.4  120 12   .016  0     error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 49 0   0   error (invalid witness file) 0 --- inspect .0022 .0030 .53 0     0     - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.2  1.2  91 11   .016  0     assertion 0 --- inspect 4.7  2.5  270 0   0   timeout 0 --- inspect 97     76     3200   1.7  0   assertion 0 --- inspect 6.0  3.2  280 0   0   timeout 0 --- inspect 96      96      21    .46  0     - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.6  1.6  110 16   .016  0     assertion 0 --- inspect 5.8  3.1  270 0   0   error (7) 0 --- inspect 23     12     370   .54 0   assertion 0 --- inspect 6.3  3.4  280 0   0   timeout 0 --- inspect 96      96      21    .54  0     - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c error (8) 0 --- inspect .93 .92 81 9.3 .012  .057 error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0080 .52 0     0     - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c error (8) 0 --- inspect 1.5  1.5  120 11   .016  0     error (invalid witness file) 0 --- inspect .56 .36 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .63 47 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .53 0     0     - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c error (8) 0 --- inspect 1.4  1.3  120 16   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c error (8) 0 --- inspect 1.3  1.3  110 12   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (8) 0 --- inspect 4.7  4.7  440 56   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (8) 0 --- inspect 1.6  1.6  110 14   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c error (8) 0 --- inspect 1.5  1.5  120 11   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error (8) 0 --- inspect .80 .80 70 8.2 .012  0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .59 47 0   0   error (invalid witness file) 0 --- inspect .0032 .0042 .53 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error (8) 0 --- inspect .77 .77 70 7.2 .012  0     error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .59 47 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .52 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error (8) 0 --- inspect .80 .79 70 6.5 .012  .057 error (invalid witness file) 0 --- inspect .79 .48 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 47 0   0   error (invalid witness file) 0 --- inspect .0024 .0031 .52 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error (8) 0 --- inspect .77 .77 70 7.9 .012  0     error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0026 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error (8) 0 --- inspect .83 .83 70 8.6 .012  0     error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .60 46 0   0   error (invalid witness file) 0 --- inspect .0015 .0022 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error (8) 0 --- inspect .87 .87 70 8.0 .012  0     error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .82 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0023 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error (8) 0 --- inspect .88 .87 70 8.1 .012  0     error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 49 0   0   error (invalid witness file) 0 --- inspect .0069 .0087 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 71 7.7 .012  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 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0027 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c error (8) 0 --- inspect .86 .86 70 8.0 .012  0     error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0024 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c error (8) 0 --- inspect .90 .90 70 7.4 .012  0     error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .62 48 0   0   error (invalid witness file) 0 --- inspect .0023 .0031 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 71 10   .012  0     error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 48 0   0   error (invalid witness file) 0 --- inspect .0047 .0060 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 70 8.9 .012  0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .60 48 0   0   error (invalid witness file) 0 --- inspect .0012 .0016 .39 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c error (8) 0 --- inspect .87 .86 71 7.4 .012  0     error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .025 .026 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .78 48 0   0   error (invalid witness file) 0 --- inspect .0018 .0029 .48 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 70 9.0 .012  0     error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0073 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c error (8) 0 --- inspect .89 .89 71 7.2 .012  0     error (invalid witness file) 0 --- inspect .63 .38 43 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0028 .0033 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c error (8) 0 --- inspect .89 .89 70 7.9 .012  0     error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .61 48 0   0   error (invalid witness file) 0 --- inspect .0065 .0085 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c error (8) 0 --- inspect .83 .82 70 9.4 .012  0     error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0   error (invalid witness file) 0 --- inspect .0043 .0072 .52 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c error (8) 0 --- inspect .92 .91 70 7.5 .012  0     error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .59 47 0   0   error (invalid witness file) 0 --- inspect .0050 .0062 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c error (8) 0 --- inspect .89 .88 71 7.6 .012  0     error (invalid witness file) 0 --- inspect .61 .38 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 .0059 .0077 .40 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c error (8) 0 --- inspect .75 .76 70 8.3 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c error (8) 0 --- inspect .76 .76 70 7.7 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c error (8) 0 --- inspect .79 .79 70 6.7 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c error (8) 0 --- inspect .74 .74 70 8.7 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .027 .029 5.6 0    0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (8) 0 --- inspect .85 .85 70 6.9 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (8) 0 --- inspect .85 .85 71 7.9 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (8) 0 --- inspect .81 .81 71 9.3 .012  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.07_true-unreach-call.i.cil.c error (8) 0 --- inspect .83 .83 70 9.1 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (8) 0 --- inspect .86 .85 71 7.8 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 71 8.0 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (8) 0 --- inspect .86 .85 70 7.4 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (8) 0 --- inspect .85 .85 71 8.3 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (8) 0 --- inspect .85 .85 70 9.3 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (8) 0 --- inspect .84 .84 71 9.6 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 42 0   0   error (2) 0 --- inspect .027 .029 5.7 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (8) 0 --- inspect .86 .86 70 7.4 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (8) 0 --- inspect .83 .83 71 8.4 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .025 .025 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (8) 0 --- inspect .87 .87 71 7.7 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .021 .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 26 14000   14000   220000 180000 1.6   .17 42 16 130 71 6300 0   0   42 16 330 210 10000 12 0   42 4 170 95 6600 0   0   42 -216 210   210   390 3.9 .033 52 10 68 39 3800 0   0   52 10 330 190 4000 3.1 0  
    correct results 21 26 48   48   8800 640 .086 0    16 16 110 57 4800 0   0   16 16 210 120 6500 10 0   4 4 24 13 1100 0   0   8 8 6.1 6.1 170 1.6 .033 5 10 38 21 1800 0   0   5 10 330 190 3700 3.1 0  
        correct true 5 10 20   20   3400 260 .020 0    0 0 0 0 5 10 38 21 1800 0   0   5 10 330 190 3700 3.1 0  
        correct false 16 16 28   28   5400 380 .066 0    16 16 110 57 4800 0   0   16 16 210 120 6500 10 0   4 4 24 13 1100 0   0   8 8 6.1 6.1 170 1.6 .033 0 0
    correct-unconfimed results 2 0 2.8 2.7 200 26 .033 0    0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 2.8 2.7 200 26 .033 0    0 0 0 0 0 0
    incorrect results 0 0 0 0 7 -224 5.3 5.3 150 1.1 0     0 0
        incorrect true 0 0 0 0 7 -224 5.3 5.3 150 1.1 0     0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 26 16 16 4 -216 10 10
Run set pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow