Tool CBMC 5.8 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:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.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.4  160 15   true -32 wit inspect 4.8 280 false(unreach-call) 1 wit inspect 10   450 unknown 0 wit inspect 8.7 280 false(unreach-call) 1 wit inspect .88 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 .48 41 5.5 true -32 wit inspect 4.6 280 false(unreach-call) 1 wit inspect 16   530 unknown 0 wit inspect 5.1 280 false(unreach-call) 1 wit inspect .77 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 .76 60 10   true -32 wit inspect 4.6 260 false(unreach-call) 1 wit inspect 15   530 unknown 0 wit inspect 5.8 270 false(unreach-call) 1 wit inspect .80 20 - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .39 38 4.5 true -32 wit inspect 4.5 270 false(unreach-call) 1 wit inspect 8.3 350 unknown 0 wit inspect 4.5 220 false(unreach-call) 1 wit inspect .76 19 - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.9  160 31   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    600 true 2 wit inspect 100     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 0 wit inspect 870    4500 3700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 5.0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .84 42 8.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    360 true 2 wit inspect 64     930  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.4  60 15   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    390 true 2 wit inspect 76     1000  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .52 35 5.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  260 true 2 wit inspect 20     540  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .63 36 9.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  270 true 2 wit inspect 18     510  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0  87 24   true -32 wit inspect 4.9 260 false(unreach-call) 1 wit inspect 7.8 360 unknown 0 wit inspect 5.4 280 true -32 wit inspect .73 19 - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1  87 23   true -32 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 11   360 unknown 0 wit inspect 6.1 290 true -32 wit inspect .93 19 - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.4  100 30   true -32 wit inspect 4.5 260 false(unreach-call) 1 wit inspect 7.8 360 unknown 0 wit inspect 5.7 280 error (2) 0 wit inspect .87 19 - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.1  87 24   true -32 wit inspect 5.4 260 false(unreach-call) 1 wit inspect 7.5 350 unknown 0 wit inspect 6.1 280 true -32 wit inspect .79 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 35 3.0 false(unreach-call) 1 wit inspect 4.3 260 false(unreach-call) 1 wit inspect 8.9 320 unknown 0 wit inspect 4.5 260 false(unreach-call) 1 wit inspect .74 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14    330 170   true -32 wit inspect 7.6 270 false(unreach-call) 1 wit inspect 12   550 unknown 0 wit inspect 9.9 420 true -32 wit inspect .76 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.5  150 41   true -32 wit inspect 5.7 260 false(unreach-call) 1 wit inspect 8.8 410 unknown 0 wit inspect 7.9 370 true -32 wit inspect 1.0  19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.3  140 37   true -32 wit inspect 5.5 270 false(unreach-call) 1 wit inspect 9.1 360 unknown 0 wit inspect 6.0 290 true -32 wit inspect .84 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 35 3.1 true -32 wit inspect 3.5 260 false(unreach-call) 1 wit inspect 8.8 340 unknown 0 wit inspect 5.3 280 true -32 wit inspect .75 19 - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.1  140 38   true -32 wit inspect 5.6 270 false(unreach-call) 1 wit inspect 9.0 390 unknown 0 wit inspect 7.5 330 true -32 wit inspect .73 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.0  130 35   true -32 wit inspect 5.4 270 false(unreach-call) 1 wit inspect 9.1 390 unknown 0 wit inspect 7.5 300 true -32 wit inspect .89 20 - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 37 2.8 false(unreach-call) 1 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 7.8 310 unknown 0 wit inspect 4.7 260 false(unreach-call) 1 wit inspect .84 19 - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 25    380 270   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2600 true 2 wit inspect 36     890  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 26    390 260   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    2700 true 2 wit inspect 41     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 30    460 420   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    3700 true 2 wit inspect 41     1200  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 26    390 300   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    2800 true 2 wit inspect 44     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1100 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .049 5.0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1100 3600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .020 4.9
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    2700 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .023 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 4300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 5200   - 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_6_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .020 4.9
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 45 error (2) 0 wit inspect .020 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c error (42) 0 wit inspect 870    1200 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .021 4.9
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .31 33 3.0 false(unreach-call) 1 wit inspect 4.2 260 false(unreach-call) 1 wit inspect 6.2 270 unknown 0 wit inspect 3.4 210 false(unreach-call) 1 wit inspect .67 19 - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .33 36 3.5 false(unreach-call) 1 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 7.4 270 unknown 0 wit inspect 3.5 210 false(unreach-call) 1 wit inspect .73 19 - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    3300 6400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    4000 5600   - 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
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    4800 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .048 4.9
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    5500 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .047 4.8
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    6200 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .023 4.8
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    6900 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .052 4.8
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    5900 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .81 46 error (2) 0 wit inspect .022 5.0
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    7900 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .018 4.9
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1900 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .022 4.8
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    2300 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.9
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    2800 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .025 4.9
ntdrivers/cdaudio_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 100    5100 1300   true -32 wit inspect 8.4 410 timeout 0 wit inspect 97   870 unknown 0 wit inspect 16   450 error (1) 0 wit inspect 1.8  33 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 1.7  120 17   false(unreach-call) 1 wit inspect 16   460 false(unreach-call) 1 wit inspect 15   470 unknown 0 wit inspect 7.0 300 timeout 0 wit inspect 96    19 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 3.5  170 38   true -32 wit inspect 17   480 true -32 wit inspect 25   580 unknown 0 wit inspect 11   450 timeout 0 wit inspect 96    20 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 1.5  73 15   true -32 wit inspect 6.7 270 true -32 wit inspect 69   810 unknown 0 wit inspect 5.9 270 error (1) 0 wit inspect .84 20 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 14    790 150   false(unreach-call) 1 wit inspect 9.3 330 timeout 0 wit inspect 97   880 unknown 0 wit inspect 6.8 300 error (1) 0 wit inspect 1.4  22 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 39    410 470   - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 7.9  300 true 2 wit inspect 170     2000  
ntdrivers/diskperf_true-unreach-call.i.cil.c error (42) 0 wit inspect 880    7500 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (42) 0 wit inspect 870    7500 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 5.0
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (42) 0 wit inspect 870    4400 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .036 4.9
ntdrivers/parport_true-unreach-call.i.cil.c error (42) 0 wit inspect 880    5200 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 15    470 170   true -32 wit inspect 15   390 false(unreach-call) 1 wit inspect 42   610 unknown 0 wit inspect 9.6 280 error (2) 0 wit inspect .87 20 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.4  210 58   true -32 wit inspect 19   630 false(unreach-call) 1 wit inspect 39   530 unknown 0 wit inspect 7.1 270 error (2) 0 wit inspect .95 19 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.3  210 57   true -32 wit inspect 12   620 false(unreach-call) 1 wit inspect 38   530 unknown 0 wit inspect 7.6 270 error (2) 0 wit inspect .80 19 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 5.3  210 60   true -32 wit inspect 21   630 false(unreach-call) 1 wit inspect 33   560 unknown 0 wit inspect 5.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) 1 wit inspect 6.7  270 67   true -32 wit inspect 13   450 false(unreach-call) 1 wit inspect 31   510 unknown 0 wit inspect 8.3 350 error (2) 0 wit inspect .82 19 - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  250 76   true -32 wit inspect 35   920 false(unreach-call) 1 wit inspect 33   500 unknown 0 wit inspect 9.0 410 error (2) 0 wit inspect .90 19 - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  250 76   false(unreach-call) 1 wit inspect 6.5 280 false(unreach-call) 1 wit inspect 24   480 unknown 0 wit inspect 9.3 280 error (2) 0 wit inspect .77 19 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.5  260 74   true -32 wit inspect 31   900 false(unreach-call) 1 wit inspect 27   510 unknown 0 wit inspect 7.4 280 error (2) 0 wit inspect .79 19 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.7  260 82   true -32 wit inspect 30   1100 false(unreach-call) 1 wit inspect 63   680 unknown 0 wit inspect 13   320 error (2) 0 wit inspect .88 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  260 91   true -32 wit inspect 29   880 false(unreach-call) 1 wit inspect 51   640 unknown 0 wit inspect 11   310 error (2) 0 wit inspect .86 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 19    510 220   true -32 wit inspect 65   1800 timeout 0 wit inspect 97   960 unknown 0 wit inspect 11   420 error (2) 0 wit inspect 1.0  20 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  260 100   true -32 wit inspect 31   940 false(unreach-call) 1 wit inspect 47   650 unknown 0 wit inspect 11   420 error (2) 0 wit inspect .82 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 19    510 250   timeout 0 wit inspect 92   2600 timeout 0 wit inspect 97   930 unknown 0 wit inspect 11   420 error (2) 0 wit inspect .80 21 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 6.8  260 75   true -32 wit inspect 29   930 timeout 0 wit inspect 97   740 unknown 0 wit inspect 7.6 360 error (2) 0 wit inspect 1.0  20 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  260 77   true -32 wit inspect 26   930 false(unreach-call) 1 wit inspect 54   670 unknown 0 wit inspect 10   310 error (2) 0 wit inspect 1.1  20 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.6  260 76   true -32 wit inspect 32   890 false(unreach-call) 1 wit inspect 53   650 unknown 0 wit inspect 11   410 error (2) 0 wit inspect .86 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.7  260 69   true -32 wit inspect 31   920 false(unreach-call) 1 wit inspect 51   670 unknown 0 wit inspect 9.7 310 error (2) 0 wit inspect .84 20 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 20    510 230   timeout 0 wit inspect 92   2500 timeout 0 wit inspect 97   940 unknown 0 wit inspect 10   420 error (2) 0 wit inspect .84 21 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 6.7  260 89   true -32 wit inspect 28   960 false(unreach-call) 1 wit inspect 50   680 unknown 0 wit inspect 12   420 error (2) 0 wit inspect .82 20 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 39    650 420   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 13    420 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 38    600 370   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 11    430 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 1 wit inspect 38    600 400   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 16    440 timeout 0 wit inspect 960     4600  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 1 wit inspect 38    600 500   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 14    430 timeout 0 wit inspect 960     4600  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .039 4.9
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 5.0
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .023 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.8
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 5000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .017 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (42) 0 wit inspect 870    1700 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 5.0
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 59 34000 130000 210000 42 -1049 780 26000 42 -30 1500 23000 42 0 340 13000 42 -280 230   840 52 18 750 17000 52 20 4500 29000
    correct results 45 55 310 8900 3600 7 7 49 2100 34 34 820 16000 0 8 8 6.2 150 9 18 660 14000 10 20 610 11000
        correct true 10 20 150 2400 1800 0 0 0 0 9 18 660 14000 10 20 610 11000
        correct false 35 35 160 6600 1900 7 7 49 2100 34 34 820 16000 0 8 8 6.2 150 0 0
    correct-unconfimed results 11 4 330 9600 3800 0 0 0 0 0 0
        correct-unconfirmed true 4 4 150 2500 1700 0 0 0 0 0 0
        correct-unconfirmed false 7 0 170 7100 2100 0 0 0 0 0 0
    incorrect results 0 33 -1056 550 19000 2 -64 94 1400 0 9 -288 7.5 180 0 0
        incorrect true 0 33 -1056 550 19000 2 -64 94 1400 0 9 -288 7.5 180 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 59 -1049 -30 0 -280 18 20
Run set cbmc.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-ControlFlow