Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 .39 16 4.7 false(unreach-call) 1 wit inspect 9.0  480 true -32 wit inspect 5.9   380   unknown 0 wit inspect 2.7  220 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 .26 13 3.7 false(unreach-call) 1 wit inspect 5.8  370 true -32 wit inspect 7.2   310   unknown 0 wit inspect 2.5  210 true -32 wit inspect .69   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 .38 14 4.5 false(unreach-call) 1 wit inspect 6.3  380 true -32 wit inspect 5.8   340   unknown 0 wit inspect 2.7  220 true -32 wit inspect .75   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 .24 13 2.9 false(unreach-call) 1 wit inspect 3.5  280 true -32 wit inspect 7.2   290   unknown 0 wit inspect 2.4  210 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 .42 16 5.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    520 true 2 wit inspect 99     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .35 13 3.7 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 71     860  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .29 13 3.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  360 true 2 wit inspect 46     930  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .38 14 5.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    370 true 2 wit inspect 70     950  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .19 11 2.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 20     510  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .27 12 2.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  270 true 2 wit inspect 17     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .29 12 3.1 false(unreach-call) 1 wit inspect 4.4  360 true -32 wit inspect 3.8   260   unknown 0 wit inspect 3.5  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .28 12 3.4 false(unreach-call) 1 wit inspect 7.8  350 true -32 wit inspect 6.1   260   unknown 0 wit inspect 2.6  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .32 12 3.5 false(unreach-call) 1 wit inspect 7.7  360 true -32 wit inspect 4.1   270   unknown 0 wit inspect 2.4  210 true -32 wit inspect .68   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .28 12 3.9 false(unreach-call) 1 wit inspect 8.7  350 true -32 wit inspect 4.1   270   unknown 0 wit inspect 2.5  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .26 12 2.6 false(unreach-call) 1 wit inspect 5.4  270 true -32 wit inspect 6.2   280   unknown 0 wit inspect 2.5  220 true -32 wit inspect .65   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .39 14 5.4 false(unreach-call) 1 wit inspect 70    820 true -32 wit inspect 6.8   270   unknown 0 wit inspect 2.5  220 true -32 wit inspect .68   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.1  23 14   false(unreach-call) 1 wit inspect 33    570 true -32 wit inspect 6.3   270   unknown 0 wit inspect 2.6  220 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 13 3.5 false(unreach-call) 1 wit inspect 7.3  300 true -32 wit inspect 6.4   260   unknown 0 wit inspect 3.7  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 12 3.4 false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 6.3   270   unknown 0 wit inspect 2.6  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 12 3.0 false(unreach-call) 1 wit inspect 5.5  280 true -32 wit inspect 4.2   270   unknown 0 wit inspect 3.5  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 12 3.1 false(unreach-call) 1 wit inspect 6.6  280 true -32 wit inspect 4.6   260   unknown 0 wit inspect 3.9  240 true -32 wit inspect .64   18    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .25 12 2.6 false(unreach-call) 1 wit inspect 4.7  260 false(unreach-call) 1 wit inspect 4.7   310   unknown 0 wit inspect 2.6  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 13 7.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    390 true 2 wit inspect 36     890  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect .60 13 7.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    390 true 2 wit inspect 42     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect .61 13 7.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  520 true 2 wit inspect 38     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect .59 13 8.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    390 true 2 wit inspect 44     980  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    640 10000   - 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-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    81 10000   - 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-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    58 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 43 error (2) 0 wit inspect .018 4.9
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 48 error (2) 0 wit inspect .018 4.8
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 5.0
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 10000   - 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-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    220 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 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 .18 11 1.9 false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 3.4  220 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 .16 11 1.9 false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 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 .16 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 11     640  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  280 true 2 wit inspect 21     1100  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  280 true 2 wit inspect 27     2400  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  280 true 2 wit inspect 46     3700  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  290 true 2 wit inspect 64     5600  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  280 out of memory 0 wit inspect 93     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  270 true 2 wit inspect 7.5   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 9.4   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .16 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  280 true 2 wit inspect 6.7   390  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  280 true 2 wit inspect 11     490  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  290 true 2 wit inspect 13     510  
ntdrivers/cdaudio_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 1.0  36 12   false(unreach-call) 1 wit inspect 56    1400 true -32 wit inspect 15     530   unknown 0 wit inspect 4.2  310 error (2) 0 wit inspect 1.6    22    - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c unknown 0 wit inspect .59 29 8.0 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 0 wit inspect .92 43 11   error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect .50 32 5.0 false(unreach-call) 1 wit inspect 8.2  300 true -32 wit inspect 8.7   420   unknown 0 wit inspect 4.4  260 error (2) 0 wit inspect .91   19    - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c unknown 0 wit inspect 1.7  120 18   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect .97 35 13   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .024 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 0 wit inspect .80 40 8.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c unknown 0 wit inspect 2.2  57 30   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .023 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unknown 0 wit inspect .90 43 12   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .021 4.8
ntdrivers/parport_true-unreach-call.i.cil.c unknown 0 wit inspect 1.6  120 19   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .021 4.8
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect .36 12 3.5 error (invalid witness file) 0 wit inspect .54 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 .0028 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c unknown 0 wit inspect .33 12 4.4 error (invalid witness file) 0 wit inspect .49 44 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c unknown 0 wit inspect .36 12 4.1 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0027 .29 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect .34 12 4.0 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect .47 12 6.5 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 49 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 .50 12 5.5 error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .027 4.9 error (invalid witness file) 0 wit inspect .67 49 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 .50 12 5.6 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect .48 12 5.9 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .84 50 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c unknown 0 wit inspect .51 13 5.9 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 51 error (invalid witness file) 0 wit inspect .0030 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c unknown 0 wit inspect .50 12 5.0 error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c unknown 0 wit inspect .49 12 5.9 error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c unknown 0 wit inspect .52 12 5.5 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c unknown 0 wit inspect .55 12 5.5 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c unknown 0 wit inspect .48 12 5.8 error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0034 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c unknown 0 wit inspect .48 12 6.5 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c unknown 0 wit inspect .52 12 5.4 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .89 49 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 .48 12 5.4 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0032 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c unknown 0 wit inspect .52 12 5.7 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .017 5.0 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c unknown 0 wit inspect .48 13 6.2 error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect .33 12 4.3 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect .36 12 4.8 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c unknown 0 wit inspect .36 12 4.1 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c unknown 0 wit inspect .35 12 4.0 - 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_srvr.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect .49 12 5.6 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 4.8
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect .48 12 5.7 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.9
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c unknown 0 wit inspect .52 13 6.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 4.8
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c unknown 0 wit inspect .53 12 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c unknown 0 wit inspect .51 12 5.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 4.8
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c unknown 0 wit inspect .51 12 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c unknown 0 wit inspect .50 13 5.8 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 44 error (2) 0 wit inspect .022 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c unknown 0 wit inspect .50 12 5.5 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .022 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c unknown 0 wit inspect .50 12 5.5 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c unknown 0 wit inspect .49 12 6.4 - 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
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c unknown 0 wit inspect .48 12 5.7 - 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/s3_srvr.blast.15_true-unreach-call.i.cil.c unknown 0 wit inspect .50 12 5.9 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 4.8
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c unknown 0 wit inspect .50 13 5.7 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 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 62 8100   3600 92000 42 20 270 9200 42 -607 120   6100 42 0 76 5500 42 -510 14   380 52 40 590 15000 52 40 790 32000
    correct results 41 62 13   560 160 20 20 260 8200 1 1 4.7 310 0 2 2 1.2 37 20 40 140 6600 20 40 700 25000
        correct true 21 42 5.8 250 69 0 0 0 0 20 40 140 6600 20 40 700 25000
        correct false 20 20 7.3 310 88 20 20 260 8200 1 1 4.7 310 0 2 2 1.2 37 0 0
    incorrect results 0 0 19 -608 120   5700 0 16 -512 11   300 0 0
        incorrect true 0 0 19 -608 120   5700 0 16 -512 11   300 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 62 20 -607 0 -510 40 40
Run set symbiotic.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-ControlFlow