Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .98  47 12    false(unreach-call) 1 wit inspect 3.1  280 true -32 wit inspect 6.0   400   unknown 0 wit inspect 3.3  270 true -32 wit inspect .82   18    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .76  33 6.9  false(unreach-call) 1 wit inspect 3.1  280 true -32 wit inspect 7.4   300   unknown 0 wit inspect 2.8  220 true -32 wit inspect .71   18    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 1.0   36 9.0  false(unreach-call) 1 wit inspect 3.2  280 true -32 wit inspect 8.3   350   unknown 0 wit inspect 2.9  220 true -32 wit inspect .72   18    - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .53  32 4.3  false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 4.5   290   unknown 0 wit inspect 2.6  220 true -32 wit inspect .67   18    - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .64  45 7.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    520 true 2 wit inspect 67     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .32  31 3.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 61     890  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .22  31 2.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  360 true 2 wit inspect 65     960  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .36  34 4.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    360 true 2 wit inspect 79     980  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .12  29 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  260 true 2 wit inspect 23     520  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .15  30 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 true 2 wit inspect 18     500  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1   56 27    false(unreach-call) 1 wit inspect 2.9  270 true -32 wit inspect 5.4   270   unknown 0 wit inspect 2.7  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.3   56 24    false(unreach-call) 1 wit inspect 4.8  270 true -32 wit inspect 4.3   270   unknown 0 wit inspect 2.8  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8   65 27    false(unreach-call) 1 wit inspect 3.0  280 true -32 wit inspect 6.0   280   unknown 0 wit inspect 2.9  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4   57 25    false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 4.3   270   unknown 0 wit inspect 4.3  240 true -32 wit inspect .67   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .63  31 6.8  false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.1   270   unknown 0 wit inspect 3.7  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8   86 61    false(unreach-call) 1 wit inspect 3.1  280 true -32 wit inspect 8.0   280   unknown 0 wit inspect 3.0  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.6   66 36    false(unreach-call) 1 wit inspect 3.2  280 true -32 wit inspect 6.3   270   unknown 0 wit inspect 4.2  220 true -32 wit inspect .69   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.4   44 19    false(unreach-call) 1 wit inspect 3.6  280 true -32 wit inspect 6.2   280   unknown 0 wit inspect 2.9  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.2   31 15    false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 6.3   280   unknown 0 wit inspect 4.0  220 true -32 wit inspect .67   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.7   44 16    false(unreach-call) 1 wit inspect 2.9  270 true -32 wit inspect 6.0   260   unknown 0 wit inspect 4.1  240 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.7   42 19    false(unreach-call) 1 wit inspect 3.0  270 true -32 wit inspect 4.2   270   unknown 0 wit inspect 4.0  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.1   31 11    false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 7.2   310   unknown 0 wit inspect 3.6  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 14     190 160    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    500 true 2 wit inspect 34     860  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 14     200 210    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    510 true 2 wit inspect 45     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 17     240 180    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    520 true 2 wit inspect 40     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 15     200 170    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    510 true 2 wit inspect 46     980  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     1900 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .020 4.8
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2300 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .024 4.8
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2300 8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .024 4.8
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2300 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2300 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2200 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 5.0
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2400 8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .022 5.0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900     2200 8000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .76  29 6.6  false(unreach-call) 1 wit inspect 2.4  260 true -32 wit inspect 3.6   240   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .86  29 7.0  false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 3.8   250   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .099 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 true 2 wit inspect 16     700  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 22     1200  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  280 true 2 wit inspect 29     2300  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  290 true 2 wit inspect 39     3700  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14  27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 78     5800  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14  27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 out of memory 0 wit inspect 110     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 .70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  270 true 2 wit inspect 8.0   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .10  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  280 true 2 wit inspect 6.4   330  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 9.5   370  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  280 true 2 wit inspect 8.3   500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13  27 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 13     500  
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 wit inspect 1.5   290 18    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.0   88 12    timeout 0 wit inspect 92    2100 true -32 wit inspect 9.3   460   unknown 0 wit inspect 3.5  280 timeout 0 wit inspect 96      19    - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c timeout 0 wit inspect 900     1100 11000    error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .044 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 wit inspect .63  73 9.1  error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0026 .26 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 28     490 310    error (invalid witness file) 0 wit inspect 5.0  220 true -32 wit inspect 25     700   error (invalid witness file) 0 wit inspect 3.5  240 error (1) 0 wit inspect 1.3    22    - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect .87  280 10    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .023 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 wit inspect .31  82 4.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .018 4.8
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 wit inspect 900     430 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .024 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 900     1000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .020 4.9
ntdrivers/parport_true-unreach-call.i.cil.c true 2 wit inspect 33     660 420    - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 14    430 true 2 wit inspect 280     4600  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 19     790 190    false(unreach-call) 1 wit inspect 8.7  280 true -32 wit inspect 8.0   330   unknown 0 wit inspect 3.2  260 error (2) 0 wit inspect .72   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 11     510 140    false(unreach-call) 1 wit inspect 5.0  290 true -32 wit inspect 7.9   320   unknown 0 wit inspect 3.2  270 error (2) 0 wit inspect .78   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 11     510 130    false(unreach-call) 1 wit inspect 7.4  280 true -32 wit inspect 5.5   320   unknown 0 wit inspect 3.2  270 error (2) 0 wit inspect .75   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 12     510 110    false(unreach-call) 1 wit inspect 4.5  280 true -32 wit inspect 5.4   330   unknown 0 wit inspect 4.7  270 error (2) 0 wit inspect .78   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 6.6   340 68    error (invalid witness file) 0 wit inspect 3.5  210 true -32 wit inspect 5.7   330   error (invalid witness file) 0 wit inspect 3.5  210 error (1) 0 wit inspect .68   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 7.4   340 81    error (invalid witness file) 0 wit inspect 3.8  210 true -32 wit inspect 9.2   330   error (invalid witness file) 0 wit inspect 2.5  210 error (1) 0 wit inspect .71   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 7.2   340 94    error (invalid witness file) 0 wit inspect 2.2  210 true -32 wit inspect 6.0   330   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 7.2   340 93    error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 8.7   320   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16     610 180    error (invalid witness file) 0 wit inspect 2.3  210 true -32 wit inspect 6.1   340   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16     620 170    error (invalid witness file) 0 wit inspect 2.2  210 true -32 wit inspect 8.5   340   error (invalid witness file) 0 wit inspect 3.5  220 error (1) 0 wit inspect .72   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 49     1400 660    error (invalid witness file) 0 wit inspect 2.3  210 true -32 wit inspect 8.3   330   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16     620 210    error (invalid witness file) 0 wit inspect 2.2  210 true -32 wit inspect 5.5   330   error (invalid witness file) 0 wit inspect 3.4  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 48     1400 650    error (invalid witness file) 0 wit inspect 2.2  210 true -32 wit inspect 5.6   320   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 15     620 200    error (invalid witness file) 0 wit inspect 3.6  210 true -32 wit inspect 5.7   320   error (invalid witness file) 0 wit inspect 3.5  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 15     610 200    error (invalid witness file) 0 wit inspect 2.2  210 true -32 wit inspect 8.4   340   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .68   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 15     620 180    error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 5.7   330   error (invalid witness file) 0 wit inspect 2.5  220 error (1) 0 wit inspect .68   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 15     610 160    error (invalid witness file) 0 wit inspect 2.8  210 true -32 wit inspect 8.1   340   error (invalid witness file) 0 wit inspect 3.5  220 error (1) 0 wit inspect .71   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 48     1400 720    error (invalid witness file) 0 wit inspect 3.3  210 true -32 wit inspect 6.2   330   error (invalid witness file) 0 wit inspect 2.5  220 error (1) 0 wit inspect .73   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16     610 200    error (invalid witness file) 0 wit inspect 3.4  210 true -32 wit inspect 8.4   330   error (invalid witness file) 0 wit inspect 3.5  210 error (1) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 90     2700 990    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 110     2800 1600    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 110     2800 1400    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 110     2800 1200    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 timeout 0 wit inspect 960     4600  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900     15000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 5.0
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900     15000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .022 5.0
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 9300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900     15000 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .026 4.8
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 5.0
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900     15000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .020 5.0
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900     15000 8100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.8
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .025 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900     14000 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .018 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 94 70 23000 240000 250000 42 22 230 12000 42 -1215 270   13000 42 0 120 8900 42 -510 120   730 52 40 4200 23000 52 42 4900 55000
    correct results 44 66 180 5100 2100 22 22 87 6000 1 1 7.2 310 0 2 2 1.2 36 20 40 160 6900 21 42 990 29000
        correct true 22 44 96 2000 1200 0 0 0 0 20 40 160 6900 21 42 990 29000
        correct false 22 22 85 3200 900 22 22 87 6000 1 1 7.2 310 0 2 2 1.2 36 0 0
    correct-unconfimed results 21 4 740 22000 9300 0 0 0 0 0 0
        correct-unconfirmed true 4 4 410 11000 5100 0 0 0 0 0 0
        correct-unconfirmed false 17 0 330 11000 4200 0 0 0 0 0 0
    incorrect results 0 0 38 -1216 260   12000 0 16 -512 11   300 0 0
        incorrect true 0 0 38 -1216 260   12000 0 16 -512 11   300 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 70 22 -1215 0 -510 40 42
Run set esbmc-kind.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-ControlFlow