Tool 2LS 0.6.0 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*
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-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.2017-11-30_1120.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.3  380 19    true -32 wit inspect 7.0  290 false(unreach-call) 1 wit inspect 14     450   unknown 0 wit inspect 5.4  270 false(unreach-call) 1 wit inspect .87   19    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .38 65 3.2  true -32 wit inspect 5.1  260 false(unreach-call) 1 wit inspect 12     370   unknown 0 wit inspect 4.4  270 true -32 wit inspect .79   19    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .54 130 6.2  true -32 wit inspect 5.6  270 false(unreach-call) 1 wit inspect 10     420   unknown 0 wit inspect 4.6  220 true -32 wit inspect .81   19    - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .28 41 2.2  true -32 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 8.9   350   unknown 0 wit inspect 4.1  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.4  410 15    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    490 true 2 wit inspect 91     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53 110 5.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 58     910  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .36 71 4.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  330 true 2 wit inspect 64     870  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .58 140 5.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    480 true 2 wit inspect 86     950  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .18 27 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  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 .27 47 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  270 true 2 wit inspect 18     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.6  170 69    true -32 wit inspect 4.6  290 true -32 wit inspect 6.8   310   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 10    180 91    true -32 wit inspect 4.2  260 true -32 wit inspect 6.8   310   unknown 0 wit inspect 4.9  220 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 0 wit inspect 15    230 140    true -32 wit inspect 4.4  270 true -32 wit inspect 8.3   320   unknown 0 wit inspect 4.7  220 error (2) 0 wit inspect .90   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 9.1  180 80    true -32 wit inspect 4.5  270 true -32 wit inspect 8.3   310   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .74   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 42 2.9  true -32 wit inspect 5.0  270 true -32 wit inspect 6.9   280   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .94   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14    230 110    true -32 wit inspect 6.2  270 true -32 wit inspect 9.4   400   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .81   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 16    230 120    true -32 wit inspect 6.3  270 true -32 wit inspect 6.9   350   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .79   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 13    170 96    true -32 wit inspect 6.0  270 true -32 wit inspect 6.8   320   unknown 0 wit inspect 4.5  230 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9  89 37    true -32 wit inspect 5.1  270 true -32 wit inspect 8.6   290   unknown 0 wit inspect 4.1  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 13    170 100    true -32 wit inspect 5.4  270 true -32 wit inspect 7.1   320   unknown 0 wit inspect 4.1  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.9  150 77    true -32 wit inspect 5.4  270 true -32 wit inspect 8.1   330   unknown 0 wit inspect 5.3  230 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 43 2.8  true -32 wit inspect 5.0  270 true -32 wit inspect 6.4   280   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.0  250 82    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    400 true 2 wit inspect 31     950  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 11    250 95    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    400 true 2 wit inspect 33     1000  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 16    320 140    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    420 true 2 wit inspect 29     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.9  260 86    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    520 true 2 wit inspect 36     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    8200 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect .61 39 9.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  330 true 2 wit inspect 8.0   310  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect .39 29 4.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 7.2   260  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    7800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    7800 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.8
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    7800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .026 5.0
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    7800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 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    7900 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .043 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900    7800 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .018 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .14 26 1.3  true -32 wit inspect 3.7  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .15 28 1.2  true -32 wit inspect 4.2  260 true -32 wit inspect 5.5   250   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 24 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 16     640  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 27 .98 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  290 true 2 wit inspect 22     930  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  300 true 2 wit inspect 27     2100  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 26 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  290 true 2 wit inspect 36     3300  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15 26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  290 true 2 wit inspect 62     5700  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15 26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  290 out of memory 0 wit inspect 98     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 23 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  280 true 2 wit inspect 7.4   270  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 23 .86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 9.7   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 24 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  280 true 2 wit inspect 9.6   380  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12 24 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 11     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11 24 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  280 true 2 wit inspect 14     500  
ntdrivers/cdaudio_false-unreach-call.i.cil.c error (6) 0 wit inspect .56 63 4.3  error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c error (134) 0 wit inspect .60 44 5.3  error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c error (134) 0 wit inspect 2.2  59 19    error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c error (134) 0 wit inspect .41 36 3.7  error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c error (5) 0 wit inspect 3.0  100 25    error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c error (6) 0 wit inspect .53 64 6.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.8
ntdrivers/diskperf_true-unreach-call.i.cil.c error (134) 0 wit inspect .60 46 6.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (5) 0 wit inspect 820    2800 4200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (134) 0 wit inspect 2.3  61 20    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.9
ntdrivers/parport_true-unreach-call.i.cil.c error (5) 0 wit inspect 3.1  100 32    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 46 error (2) 0 wit inspect .020 4.9
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error (134) 0 wit inspect .78 180 8.0  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error (134) 0 wit inspect .80 180 9.0  error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .94 49 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error (134) 0 wit inspect .81 180 9.2  error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error (134) 0 wit inspect .81 180 8.1  error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error (134) 0 wit inspect .85 210 9.1  error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .93 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error (134) 0 wit inspect .89 210 11    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error (134) 0 wit inspect .89 210 11    error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error (134) 0 wit inspect .87 210 11    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c error (134) 0 wit inspect .92 220 10    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c error (134) 0 wit inspect .91 210 11    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect 1.2  51 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c error (134) 0 wit inspect .89 210 13    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c error (134) 0 wit inspect .90 210 11    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c error (134) 0 wit inspect .90 210 9.3  error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error (134) 0 wit inspect .88 210 8.5  error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0021 .35 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c error (134) 0 wit inspect .90 210 11    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c error (134) 0 wit inspect .93 210 10    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .92 47 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c error (134) 0 wit inspect .92 220 8.8  error (invalid witness file) 0 wit inspect .58 46 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c error (134) 0 wit inspect .89 220 10    error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c error (134) 0 wit inspect .90 220 11    error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c error (134) 0 wit inspect .79 180 8.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c error (134) 0 wit inspect .78 180 8.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c error (134) 0 wit inspect .76 180 9.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c error (134) 0 wit inspect .78 180 7.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (134) 0 wit inspect .89 210 11    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (134) 0 wit inspect .86 210 11    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (134) 0 wit inspect .94 220 11    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (134) 0 wit inspect .90 210 10    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .032 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (134) 0 wit inspect .88 210 10    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.8
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (134) 0 wit inspect .85 210 9.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .026 4.8
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (134) 0 wit inspect .91 210 9.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (134) 0 wit inspect .87 210 8.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .047 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (134) 0 wit inspect .88 210 11    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .024 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (134) 0 wit inspect .85 210 12    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (134) 0 wit inspect .90 220 10    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (134) 0 wit inspect .90 220 10    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (134) 0 wit inspect .93 220 9.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .047 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 63 7300 71000 79000 42 -576 110 5900 42 -444 150 6000 42 0 100 5200 42 -49 14   350 52 44 560 16000 52 44 790 31000
    correct results 40 63 150 4600 1300 0 4 4 44 1600 0 15 15 11   290 22 44 180 7300 22 44 690 24000
        correct true 23 46 52 2200 460 0 0 0 0 22 44 180 7300 22 44 690 24000
        correct false 17 17 100 2300 810 0 4 4 44 1600 0 15 15 11   290 0 0
    correct-unconfimed results 1 0 15 230 140 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 15 230 140 0 0 0 0 0 0
    incorrect results 0 18 -576 93 4900 14 -448 100 4300 0 2 -64 1.6 39 0 0
        incorrect true 0 18 -576 93 4900 14 -448 100 4300 0 2 -64 1.6 39 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 63 -576 -444 0 -49 44 44
Run set 2ls.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-ControlFlow