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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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]
Date of execution 2017-12-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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 1.0  47 12   false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 9.0   380   unknown 0 wit inspect 3.1  270 true -32 wit inspect .78   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 7.8 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 4.8   310   unknown 0 wit inspect 3.9  220 true -32 wit inspect .69   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.6 false(unreach-call) 1 wit inspect 4.7  280 true -32 wit inspect 8.8   340   unknown 0 wit inspect 4.4  260 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 .49 32 4.3 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 4.7   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 8.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    520 true 2 wit inspect 90     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900    990 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .024 5.0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .23 31 2.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  360 true 2 wit inspect 43     870  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .38 34 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    460 true 2 wit inspect 77     990  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .13 28 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  270 true 2 wit inspect 18     520  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .19 30 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  270 true 2 wit inspect 18     530  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  64 27   false(unreach-call) 1 wit inspect 5.0  280 true -32 wit inspect 6.0   270   unknown 0 wit inspect 2.8  220 true -32 wit inspect .67   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.8  65 25   false(unreach-call) 1 wit inspect 4.7  290 true -32 wit inspect 4.2   270   unknown 0 wit inspect 2.9  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.6  75 40   false(unreach-call) 1 wit inspect 4.8  270 true -32 wit inspect 4.8   280   unknown 0 wit inspect 2.9  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 3.0  65 33   false(unreach-call) 1 wit inspect 4.8  270 true -32 wit inspect 6.2   270   unknown 0 wit inspect 4.3  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .35 31 2.9 false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 6.9   270   unknown 0 wit inspect 3.8  220 true -32 wit inspect .68   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.8  71 38   false(unreach-call) 1 wit inspect 5.3  280 true -32 wit inspect 6.4   270   unknown 0 wit inspect 2.9  220 true -32 wit inspect .68   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.1  75 40   false(unreach-call) 1 wit inspect 5.4  280 true -32 wit inspect 6.3   280   unknown 0 wit inspect 4.3  220 true -32 wit inspect .67   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.5  51 22   false(unreach-call) 1 wit inspect 6.2  270 true -32 wit inspect 6.6   270   unknown 0 wit inspect 2.8  220 true -32 wit inspect .69   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.3  34 15   false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 6.2   270   unknown 0 wit inspect 4.0  220 true -32 wit inspect .66   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.9  50 14   false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.3   260   unknown 0 wit inspect 3.9  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.1  49 21   false(unreach-call) 1 wit inspect 5.2  270 true -32 wit inspect 6.3   270   unknown 0 wit inspect 4.0  220 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .33 31 3.5 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 4.7   300   unknown 0 wit inspect 2.6  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 12    180 130   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    510 true 2 wit inspect 38     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 12    180 130   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    410 true 2 wit inspect 41     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 14    210 150   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    520 true 2 wit inspect 41     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 12    180 140   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    400 true 2 wit inspect 34     1000  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2400 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .023 4.9
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    1900 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .022 4.8
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .022 4.8
ssh-simplified/s3_srvr_7_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 .40 43 error (2) 0 wit inspect .019 5.0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    2300 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .79 29 6.0 false(unreach-call) 1 wit inspect 4.4  260 true -32 wit inspect 5.7   250   unknown 0 wit inspect 2.2  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 .82 29 6.2 false(unreach-call) 1 wit inspect 4.3  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2100 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .025 4.8
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2300 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 44 error (2) 0 wit inspect .021 4.8
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2300 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2400 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2500 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2500 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .018 5.0
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1700 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1800 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.8
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1900 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 4.8
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2000 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2100 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .024 4.8
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900    5800 14000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 1.1  87 12   false(unreach-call) 1 wit inspect 32    600 true -32 wit inspect 13     490   unknown 0 wit inspect 4.7  270 timeout 0 wit inspect 96      19    - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 13    460 170   error (invalid witness file) 0 wit inspect 4.4  220 true -32 wit inspect 26     580   error (invalid witness file) 0 wit inspect 3.3  230 timeout 0 wit inspect 96      19    - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 wit inspect .65 72 8.7 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0025 .26 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 7.3  350 87   error (invalid witness file) 0 wit inspect 6.0  220 true -32 wit inspect 19     710   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 .77 280 8.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.8
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 wit inspect .51 83 6.7 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 wit inspect 900    7200 8300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .026 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 900    8000 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .020 4.9
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 wit inspect 900    5700 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 14    650 150   false(unreach-call) 1 wit inspect 7.4  280 true -32 wit inspect 8.0   320   unknown 0 wit inspect 3.2  270 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 15    650 140   false(unreach-call) 1 wit inspect 7.4  300 true -32 wit inspect 8.7   330   unknown 0 wit inspect 4.5  270 error (2) 0 wit inspect .77   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15    650 150   false(unreach-call) 1 wit inspect 7.1  280 true -32 wit inspect 8.2   330   unknown 0 wit inspect 4.7  270 error (2) 0 wit inspect .76   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15    650 190   false(unreach-call) 1 wit inspect 8.4  280 true -32 wit inspect 5.5   330   unknown 0 wit inspect 4.6  270 error (2) 0 wit inspect .76   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 9.5  460 110   error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 8.6   330   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.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10    470 120   error (invalid witness file) 0 wit inspect 3.1  210 true -32 wit inspect 8.0   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.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10    470 140   error (invalid witness file) 0 wit inspect 3.3  200 true -32 wit inspect 8.3   330   error (invalid witness file) 0 wit inspect 2.4  210 error (1) 0 wit inspect .72   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10    470 110   error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 5.9   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.06_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    780 250   error (invalid witness file) 0 wit inspect 3.6  210 true -32 wit inspect 8.8   330   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.07_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    790 210   error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 8.1   340   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.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 59    1600 720   error (invalid witness file) 0 wit inspect 3.6  210 true -32 wit inspect 8.1   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 20    790 250   error (invalid witness file) 0 wit inspect 3.2  210 true -32 wit inspect 8.3   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 59    1600 660   error (invalid witness file) 0 wit inspect 3.1  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.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 11    480 130   error (invalid witness file) 0 wit inspect 3.5  210 true -32 wit inspect 8.9   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.12_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    780 240   error (invalid witness file) 0 wit inspect 3.4  210 true -32 wit inspect 8.7   340   error (invalid witness file) 0 wit inspect 3.5  210 error (1) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    790 230   error (invalid witness file) 0 wit inspect 3.3  210 true -32 wit inspect 5.7   340   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.14_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    780 220   error (invalid witness file) 0 wit inspect 3.9  210 true -32 wit inspect 5.5   330   error (invalid witness file) 0 wit inspect 2.5  210 error (1) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 61    1600 720   error (invalid witness file) 0 wit inspect 3.7  210 true -32 wit inspect 9.0   330   error (invalid witness file) 0 wit inspect 3.4  210 error (1) 0 wit inspect .71   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21    780 250   error (invalid witness file) 0 wit inspect 4.2  210 true -32 wit inspect 8.9   330   error (invalid witness file) 0 wit inspect 3.6  210 error (1) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 79    2400 800   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 92    2500 1100   - 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 92    2500 1000   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 92    2500 1100   - 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 .40 43 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.02_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 .80 43 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900    14000 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.07_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 .57 45 error (2) 0 wit inspect .019 5.0
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900    14000 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .022 5.0
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900    15000 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 5.0
ssh/s3_srvr.blast.10_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 .53 43 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .018 4.8
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900    14000 8900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .023 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900    15000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 5.0
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 .64 44 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.15_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 .68 44 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.16_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 .65 43 error (2) 0 wit inspect .024 4.8
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 45 35000 290000 360000 42 23 210 10000 42 -1247 320   13000 42 0 140 9100 42 -510 220   750 52 18 3700 12000 52 18 4200 27000
    correct results 32 41 150 4500 1500 23 23 150 6600 1 1 4.7 300 0 2 2 1.2 36 9 18 92 3700 9 18 400 8500
        correct true 9 18 52 920 570 0 0 0 0 9 18 92 3700 9 18 400 8500
        correct false 23 23 94 3500 970 23 23 150 6600 1 1 4.7 300 0 2 2 1.2 36 0 0
    correct-unconfimed results 21 4 750 23000 8700 0 0 0 0 0 0
        correct-unconfirmed true 4 4 350 9800 4000 0 0 0 0 0 0
        correct-unconfirmed false 17 0 400 14000 4600 0 0 0 0 0 0
    incorrect results 0 0 39 -1248 310   13000 0 16 -512 11   300 0 0
        incorrect true 0 0 39 -1248 310   13000 0 16 -512 11   300 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 45 23 -1247 0 -510 18 18
Run set esbmc-incr.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-ControlFlow