Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 .55  .55  51 6.4 1.0  0      false(unreach-call) 1 wit inspect 6.4  3.5  270 0   0     true -32 --- inspect 12     7.1   390   .62 0   unknown 0 --- inspect 5.4  3.0  280 0   0   true -32 --- inspect .78   .78   20    .29  0     - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .22  .22  32 2.7 1.0  0      false(unreach-call) 1 wit inspect 6.0  3.2  270 0   0     true -32 --- inspect 10     5.6   320   .62 0   unknown 0 --- inspect 5.8  3.3  260 0   0   true -32 --- inspect .69   .69   20    .19  0     - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .34  .34  39 3.8 .85 0      false(unreach-call) 1 wit inspect 5.7  3.1  280 0   0     true -32 --- inspect 13     7.5   360   .62 0   unknown 0 --- inspect 4.9  2.7  270 0   0   true -32 --- inspect .76   .76   20    .24  .049 - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .17  .17  30 2.3 .85 0      false(unreach-call) 1 wit inspect 5.3  2.9  260 0   0     true -32 --- inspect 9.5   5.8   320   .62 0   unknown 0 --- inspect 4.5  2.6  260 0   0   true -32 --- inspect .68   .68   20    .16  0     - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .74  .74  51 9.7 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    6.7  520 0   0   true 2 --- inspect 120     67     1100   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .56  .56  31 7.8 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 540    510    7000 0   0   true 2 --- inspect 68     39     840   .62 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .26  .27  32 3.5 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.0  4.9  350 0   0   true 2 --- inspect 75     41     830   .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .41  .42  39 6.1 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.3  4.5  430 0   0   true 2 --- inspect 90     50     790   .62 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .13  .13  28 1.8 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.2  270 0   0   true 2 --- inspect 27     15     480   .66 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .18  .18  30 1.7 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.6  4.1  270 0   0   true 2 --- inspect 24     13     480   .66 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.9   1.9   64 25   .85 0      false(unreach-call) 1 wit inspect 5.9  3.2  270 0   0     true -32 --- inspect 10     5.6   310   .62 0   unknown 0 --- inspect 5.0  2.8  280 0   0   true -32 --- inspect .67   .67   21    .12  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.9   1.9   65 23   1.0  0      false(unreach-call) 1 wit inspect 5.8  3.1  280 0   0     true -32 --- inspect 9.6   5.9   310   .62 0   unknown 0 --- inspect 5.1  2.8  270 0   0   true -32 --- inspect .64   .64   21    .12  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   2.3   76 25   .85 0      false(unreach-call) 1 wit inspect 5.7  3.1  270 0   .041 true -32 --- inspect 10     5.6   310   .62 0   unknown 0 --- inspect 5.1  2.9  280 0   0   true -32 --- inspect .66   .66   21    .13  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.9   1.9   66 21   .85 0      false(unreach-call) 1 wit inspect 5.5  3.0  270 0   0     true -32 --- inspect 9.4   5.3   320   .62 0   unknown 0 --- inspect 5.2  2.9  270 0   0   true -32 --- inspect .65   .65   21    .12  .037 - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .16  .16  29 1.6 1.0  0      false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0     true -32 --- inspect 9.4   5.3   320   .66 0   unknown 0 --- inspect 4.5  2.6  260 0   0   true -32 --- inspect .65   .65   20    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.5   2.5   73 31   1.0  0      false(unreach-call) 1 wit inspect 7.5  4.0  280 0   0     true -32 --- inspect 9.7   5.9   320   .62 0   unknown 0 --- inspect 5.2  2.9  280 0   0   true -32 --- inspect .66   .65   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.9   2.9   77 36   .85 0      false(unreach-call) 1 wit inspect 5.9  3.2  280 0   0     true -32 --- inspect 9.2   5.1   320   .62 0   unknown 0 --- inspect 5.4  3.0  280 0   0   true -32 --- inspect .66   .66   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.5   1.5   52 19   1.0  0      false(unreach-call) 1 wit inspect 6.3  3.3  280 0   0     true -32 --- inspect 8.8   5.0   310   .50 0   unknown 0 --- inspect 4.9  2.8  260 0   0   true -32 --- inspect .65   .67   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29  .29  31 3.9 1.0  0      false(unreach-call) 1 wit inspect 6.3  3.4  260 0   0     true -32 --- inspect 8.5   5.2   310   .62 0   unknown 0 --- inspect 4.7  2.7  270 0   0   true -32 --- inspect .65   .65   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.3   1.3   51 20   .85 0      false(unreach-call) 1 wit inspect 5.8  3.2  260 0   0     true -32 --- inspect 9.2   5.2   310   .66 0   unknown 0 --- inspect 4.8  2.7  270 0   0   true -32 --- inspect .64   .64   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.3   1.3   49 15   1.0  0      false(unreach-call) 1 wit inspect 5.4  3.0  270 0   0     true -32 --- inspect 9.9   5.4   310   .62 0   unknown 0 --- inspect 4.8  2.7  260 0   0   true -32 --- inspect .65   .65   21    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .18  .18  29 2.0 .85 0      false(unreach-call) 1 wit inspect 4.6  2.5  260 0   0     false(unreach-call) 1 --- inspect 11     6.2   320   .66 0   unknown 0 --- inspect 4.7  2.7  250 0   0   false(unreach-call) 1 --- inspect .65   .65   20    .14  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 12     12     180 140   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 16    8.9  550 0   0   true 2 --- inspect 46     25     830   .66 0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 12     12     180 170   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 16    9.2  550 0   0   true 2 --- inspect 42     23     920   .66 0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 14     14     220 160   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    8.3  580 0   0   true 2 --- inspect 44     24     1100   .66 0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 12     12     190 140   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    10    550 0   0   true 2 --- inspect 47     26     960   .62 0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2700 10000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .49 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2100 11000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2500 8900   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 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 timeout 0 --- inspect 900     900     2700 11000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2700 10000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2700 11000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2600 12000   .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .026 .027 5.8 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2600 9600   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .027 .029 5.7 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900     900     2600 11000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 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 .097 .097 27 1.2 1.0  0      false(unreach-call) 1 wit inspect 4.3  2.4  250 0   0     true -32 --- inspect 7.5   4.3   300   .62 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .58   .58   20    .057 0     - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .13  .13  27 1.4 .85 0      false(unreach-call) 1 wit inspect 5.3  2.9  260 0   0     true -32 --- inspect 8.1   4.6   320   .62 0   false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0   false(unreach-call) 1 --- inspect .61   .61   20    .061 0     - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15  .15  27 1.9 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.0  290 0   0   true 2 --- inspect 22     12     560   .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .16  .16  27 2.1 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.9  3.8  290 0   0   true 2 --- inspect 24     13     830   .62 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .17  .17  27 2.4 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.4  3.5  290 0   0   true 2 --- inspect 40     22     2100   .66 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .18  .18  27 2.0 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  300 0   0   true 2 --- inspect 49     30     3600   .66 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .20  .20  27 2.4 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.6  3.6  300 0   0   true 2 --- inspect 94     59     5900   .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22  .22  27 2.5 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.0  3.3  300 0   0   out of memory 0 --- inspect 120     74     7000   .70 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  .11  26 1.1 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.3  290 0   0   true 2 --- inspect 12     6.7   320   .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  26 1.2 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.7  3.1  280 0   0   true 2 --- inspect 11     6.6   360   .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  27 1.3 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.8  290 0   0   true 2 --- inspect 16     8.4   440   .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  26 1.5 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.4  3.5  290 0   0   true 2 --- inspect 17     9.3   520   .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14  .14  26 1.9 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  290 0   0   true 2 --- inspect 18     9.6   530   .62 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 --- inspect 2.2   2.2   290 36   1.0  .0082 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 .91 .59 46 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .53 0     0     - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.8   1.8   110 22   .85 0      true -32 wit inspect 8.2  4.3  300 0   0     true -32 --- inspect 61     50     2200   .62 0   unknown 0 --- inspect 6.0  3.3  290 0   0   timeout 0 --- inspect 96      96      21    .17  .16  - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c timeout 0 --- inspect 900     900     400 12000   .86 0      error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .59 47 0   0   error (invalid witness file) 0 --- inspect .0067 .0085 .53 0     0     - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 --- inspect .49  .49  74 6.1 .85 0      error (invalid witness file) 0 --- inspect .61 .39 40 0   0     error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0079 .54 0     0     - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 7.4   7.4   380 80   .85 0      error (invalid witness file) 0 --- inspect 6.7  3.5  290 0   0     timeout 0 --- inspect 97     77     2600   1.6  0   error (invalid witness file) 0 --- inspect 6.3  3.4  300 0   0   error (1) 0 --- inspect 1.3    1.3    24    .32  0     - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 --- inspect .80  .80  250 9.8 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 --- inspect .36  .36  87 3.9 .85 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 --- inspect 900     900     380 12000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 42 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 --- inspect 900     900     390 12000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0   error (2) 0 --- inspect .027 .028 5.7 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c true 1 wit inspect 77     77     1500 910   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 18    9.2  510 0   0   timeout 0 --- inspect 960     860     3600   .65 0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 14     14     650 160   .85 0      false(unreach-call) 1 wit inspect 8.9  4.8  340 0   0     error (7) 0 --- inspect 14     8.5   290   .75 0   unknown 0 --- inspect 5.6  3.1  270 0   0   error (2) 0 --- inspect .71   .71   21    .098 0     - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15     15     660 170   .85 0      false(unreach-call) 1 wit inspect 8.8  4.8  330 0   0     error (7) 0 --- inspect 16     8.7   290   .71 0   unknown 0 --- inspect 5.2  2.9  260 0   0   error (2) 0 --- inspect .75   .75   21    .29  0     - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15     15     660 180   1.0  0      false(unreach-call) 1 wit inspect 8.2  4.4  320 0   0     error (7) 0 --- inspect 13     7.6   290   .71 0   unknown 0 --- inspect 5.6  3.1  270 0   0   error (2) 0 --- inspect .73   .73   21    .098 0     - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15     15     650 240   1.0  0      false(unreach-call) 1 wit inspect 10    5.4  330 0   0     error (7) 0 --- inspect 12     6.8   300   .68 0   unknown 0 --- inspect 5.4  3.0  270 0   0   error (2) 0 --- inspect .76   .76   21    .29  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 9.1   9.1   470 120   1.0  0      false(unreach-call) 1 wit inspect 8.9  4.7  290 0   0     error (7) 0 --- inspect 13     7.6   290   .68 0   unknown 0 --- inspect 5.5  3.2  260 0   0   error (2) 0 --- inspect .75   .77   21    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 10     10     480 130   1.0  0      false(unreach-call) 1 wit inspect 8.7  4.7  290 0   0     error (7) 0 --- inspect 12     7.3   280   .68 0   unknown 0 --- inspect 5.3  3.0  270 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 10     10     480 120   .85 0      false(unreach-call) 1 wit inspect 7.4  4.0  290 0   0     error (7) 0 --- inspect 13     7.6   290   .71 0   unknown 0 --- inspect 5.1  2.9  260 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 10     10     480 130   1.0  0      false(unreach-call) 1 wit inspect 7.1  3.8  290 0   0     error (7) 0 --- inspect 13     7.3   290   .68 0   unknown 0 --- inspect 5.3  2.9  260 0   0   true -32 --- inspect .75   .75   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 21     21     780 250   1.0  0      false(unreach-call) 1 wit inspect 9.6  5.2  290 0   0     error (7) 0 --- inspect 13     7.7   290   .68 0   unknown 0 --- inspect 5.7  3.2  280 0   0   true -32 --- inspect .79   .79   21    .30  .078 - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     790 230   1.0  0      false(unreach-call) 1 wit inspect 8.0  4.3  300 0   0     error (7) 0 --- inspect 14     8.2   300   .71 0   unknown 0 --- inspect 5.8  3.2  260 0   0   true -32 --- inspect .77   .77   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 55     55     1600 630   .85 0      false(unreach-call) 1 wit inspect 9.8  5.3  350 0   0     error (7) 0 --- inspect 12     7.5   300   .71 0   unknown 0 --- inspect 6.0  3.3  280 0   0   true -32 --- inspect .76   .77   21    .30  .074 - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     790 270   1.0  0      false(unreach-call) 1 wit inspect 8.6  4.6  290 0   0     error (7) 0 --- inspect 16     8.9   300   .71 0   unknown 0 --- inspect 6.0  3.4  270 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 54     54     1600 630   .85 0      false(unreach-call) 1 wit inspect 9.8  5.3  340 0   0     error (7) 0 --- inspect 13     7.6   290   .71 0   unknown 0 --- inspect 6.5  3.6  280 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10     10     480 150   .85 0      true -32 wit inspect 15    7.7  450 0   0     error (7) 0 --- inspect 14     7.7   300   .68 0   unknown 0 --- inspect 5.3  3.0  270 0   0   true -32 --- inspect .75   .75   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     780 240   1.0  0      false(unreach-call) 1 wit inspect 9.2  5.0  300 0   0     error (7) 0 --- inspect 14     8.1   300   .68 0   unknown 0 --- inspect 5.4  3.0  270 0   0   true -32 --- inspect .77   .78   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     800 230   1.0  0      false(unreach-call) 1 wit inspect 9.2  5.0  290 0   0     error (7) 0 --- inspect 15     8.5   300   .71 0   unknown 0 --- inspect 5.4  3.0  270 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     780 280   1.0  0      false(unreach-call) 1 wit inspect 8.4  4.5  300 0   0     error (7) 0 --- inspect 13     7.3   290   .68 0   unknown 0 --- inspect 6.0  3.3  260 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 55     55     1600 780   1.0  0      false(unreach-call) 1 wit inspect 9.2  5.0  350 0   0     error (7) 0 --- inspect 14     8.5   290   .68 0   unknown 0 --- inspect 5.7  3.2  280 0   0   true -32 --- inspect .77   .77   21    .30  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 20     20     780 280   1.0  0      false(unreach-call) 1 wit inspect 8.0  4.4  290 0   0     error (7) 0 --- inspect 14     7.8   290   .71 0   unknown 0 --- inspect 5.4  3.0  280 0   0   true -32 --- inspect .76   .76   21    .30  0     - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 80     80     2400 870   .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1700 0   0   error (7) 0 --- inspect 16     8.8   290   .75 0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 94     94     2500 1100   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1700 0   0   error (7) 0 --- inspect 15     8.4   290   .75 0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 93     93     2500 1400   .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1600 0   0   error (7) 0 --- inspect 17     9.5   290   .75 0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 97     97     2500 1200   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    1700 0   0   error (7) 0 --- inspect 14     8.0   290   .75 0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c out of memory 0 --- inspect 860     860     15000 9800   1.0  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/s3_srvr.blast.02_true-unreach-call.i.cil.c out of memory 0 --- inspect 900     890     15000 10000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     14000 11000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (2) 0 --- inspect .028 .028 5.6 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 9200   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 10000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 11000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 10000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 9500   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     14000 9300   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .030 .030 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 9400   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     14000 10000   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     15000 13000   .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 --- inspect 900     900     14000 9900   1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0   error (2) 0 --- inspect .022 .023 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 83 23000 23000 240000 280000 89   .0082 42 -28 290 160 12000 0   .041 42 -575 590 380   16000 27    0   42 2 210   120   11000 0   0   42 -925 120   120   810 8.2  .40 52 40 4400 4200 23000 0   0   52 40 2000 1500 35000 17 0  
    correct results 57 78 480 480 17000 5900 54   0      36 36 260 140 10000 0   .041 1 1 11 6.2 320 .66 0   2 2 8.0 4.6 510 0   0   3 3 1.8 1.8 61 .26 0    20 40 170 96 7300 0   0   20 40 880 500 23000 13 0  
        correct true 21 42 55 55 1300 660 20   0      0 0 0 0 20 40 170 96 7300 0   0   20 40 880 500 23000 13 0  
        correct false 36 36 420 420 16000 5300 34   0      36 36 260 140 10000 0   .041 1 1 11 6.2 320 .66 0   2 2 8.0 4.6 510 0   0   3 3 1.8 1.8 61 .26 0    0 0
    correct-unconfimed results 8 5 460 460 12000 5800 7.3 0      0 0 0 0 0 0
        correct-unconfirmed true 5 5 440 440 11000 5600 4.7 0      0 0 0 0 0 0
        correct-unconfirmed false 3 0 19 19 970 250 2.5 0      0 0 0 0 0 0
    incorrect results 0 2 -64 23 12 750 0   0     18 -576 230 140   7700 11    0   0 29 -928 21   21   600 6.5  .24 0 0
        incorrect true 0 2 -64 23 12 750 0   0     18 -576 230 140   7700 11    0   0 29 -928 21   21   600 6.5  .24 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 83 -28 -575 2 -925 40 40
Run set esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow