Tool skink 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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.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 unknown 0 wit inspect 88   1600 590 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 52   960 530 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0033 .29 - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 50   1100 430 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 28   930 260 error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 94   1500 570 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 46 error (2) 0 wit inspect .020 4.8
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 53   1200 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.8
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 51   970 500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .021 4.9
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 49   1100 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 5.0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 29   800 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .024 4.8
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 27   820 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 67   750 720 error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 44   720 440 error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 53   720 560 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c unknown 0 wit inspect 72   750 750 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 110   820 1400 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 9.9 500 93 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0032 .26 - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 11   640 90 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0016 .31 - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 150   1100 1800 error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 15   650 130 error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 14   640 120 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0026 .29 - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 15   660 110 error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c unknown 0 wit inspect 14   660 120 error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .037 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 67   730 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 47 error (2) 0 wit inspect .020 4.8
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 46   720 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .020 5.0
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 47   720 490 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 5.0
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c unknown 0 wit inspect 33   700 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 14   650 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .023 4.9
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 31   690 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 96   720 1000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .023 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 15   650 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .018 4.8
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 16   640 140 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .021 4.8
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 16   640 150 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 20   670 160 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 18   660 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 46 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 16   700 130 - 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
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 0 wit inspect 6.0 330 58 true -32 wit inspect 4.4  270 true -32 wit inspect 4.2   240   unknown 0 wit inspect 2.2  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 0 wit inspect 5.7 320 53 true -32 wit inspect 5.3  270 true -32 wit inspect 4.4   240   unknown 0 wit inspect 3.3  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 260 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 16     640  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 270 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  280 true 2 wit inspect 23     1200  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 270 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  280 true 2 wit inspect 27     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 270 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  290 true 2 wit inspect 42     3800  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  290 true 2 wit inspect 69     5800  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  290 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 4.3 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  290 true 2 wit inspect 7.6   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 310 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  280 true 2 wit inspect 8.3   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.0 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 9.8   370  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 260 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  280 true 2 wit inspect 13     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.0 260 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  280 true 2 wit inspect 16     530  
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 wit inspect 69   1700 380 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .051 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c unknown 0 wit inspect 59   1400 290 error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 0 wit inspect 32   1100 170 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unknown 0 wit inspect 20   760 120 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 wit inspect 340   1700 1700 error (invalid witness file) 0 wit inspect .72 46 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0023 .26 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect 53   1500 260 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 wit inspect 83   1700 390 - 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
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c unknown 0 wit inspect 5.0 350 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unknown 0 wit inspect 32   1200 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
ntdrivers/parport_true-unreach-call.i.cil.c unknown 0 wit inspect 340   1700 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .021 4.8
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect 9.6 540 85 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 52 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c unknown 0 wit inspect 9.8 540 87 error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0029 .29 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c unknown 0 wit inspect 9.5 550 85 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect 10   560 90 error (invalid witness file) 0 wit inspect .68 47 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect 12   700 95 error (invalid witness file) 0 wit inspect .41 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c unknown 0 wit inspect 12   680 100 error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c unknown 0 wit inspect 11   680 95 error (invalid witness file) 0 wit inspect .41 40 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect 11   670 93 error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .050 5.0 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0031 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c unknown 0 wit inspect 12   690 97 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 48 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c unknown 0 wit inspect 11   670 89 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c unknown 0 wit inspect 12   680 110 error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c unknown 0 wit inspect 11   670 94 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0041 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c unknown 0 wit inspect 11   660 100 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c unknown 0 wit inspect 12   670 96 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c unknown 0 wit inspect 12   760 99 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0027 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c unknown 0 wit inspect 12   680 91 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c unknown 0 wit inspect 12   670 100 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c unknown 0 wit inspect 12   670 100 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c unknown 0 wit inspect 12   680 99 error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect 10   530 84 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 4.8
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect 9.4 560 83 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .025 5.0
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c unknown 0 wit inspect 9.6 550 80 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .024 5.0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c unknown 0 wit inspect 9.7 650 84 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .021 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect 11   680 92 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 5.0
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect 12   680 94 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.8
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c unknown 0 wit inspect 12   690 94 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 45 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c unknown 0 wit inspect 11   670 99 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .027 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c unknown 0 wit inspect 12   670 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .024 5.0
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c unknown 0 wit inspect 12   680 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c unknown 0 wit inspect 12   680 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c unknown 0 wit inspect 12   670 84 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .025 5.0
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c unknown 0 wit inspect 12   670 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c unknown 0 wit inspect 11   670 84 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c unknown 0 wit inspect 12   690 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .019 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c unknown 0 wit inspect 11   670 91 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .017 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c unknown 0 wit inspect 12   680 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .025 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 22 3000 69000 24000 42 -64 34   2300 42 -64 9.4 680 42 0 37 2300 42 -64 1.3 48 52 22 81 4900 52 20 340 23000
    correct results 11 22 46 3000 450 0 0 0 0 11 22 58 3100 10 20 230 15000
        correct true 11 22 46 3000 450 0 0 0 0 11 22 58 3100 10 20 230 15000
        correct false 0 0 0 0 0 0 0
    correct-unconfimed results 2 0 12 660 110 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 12 660 110 0 0 0 0 0 0
    incorrect results 0 2 -64 9.7 540 2 -64 8.5 480 0 2 -64 1.2 37 0 0
        incorrect true 0 2 -64 9.7 540 2 -64 8.5 480 0 2 -64 1.2 37 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 22 -64 -64 0 -64 22 20
Run set skink.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-ControlFlow