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 CProver witness2test 0.1 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-12-02 23:08:57 CET 2017-12-03 00:45:11 CET 2017-12-03 01:25:52 CET 2017-12-03 01:32:11 CET 2017-12-03 00:52:42 CET
Run set symbiotic.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-Other
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-02_2308.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-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.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
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 1 wit inspect 7.4  15 92   false(valid-deref) 1 wit inspect 14   910 true -32 wit inspect 6.3 260 false(valid-deref) 1 wit inspect .66 18 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 130    6100 1600   false(valid-deref) 1 wit inspect 7.9 460 unknown 0 wit inspect 5.4 220 timeout 0 wit inspect 96    19 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 7.3  880 100   false(valid-deref) 1 wit inspect 5.0 260 unknown 0 wit inspect 4.1 210 error (2) 0 wit inspect 1.0  19 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .55 29 6.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1 370
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53 28 5.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6 370
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .38 19 4.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .63 20 6.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .61 20 8.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1 310
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.3  30 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 11   340
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.4  29 19   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9 340
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .26 11 3.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7 250
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .30 14 4.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5 290
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .32 14 4.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6 280
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 240
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .20 11 2.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5 240
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22 11 2.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2 230
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .20 11 2.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 250
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .19 11 2.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .19 11 2.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 220
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21 11 2.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21 11 2.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21 11 2.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7 230
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
total 26 49 150   7400 1900 3 3 27 1600 3 -32 16   690 3 1 98    56 23 46 150 6200
    correct results 26 49 150   7400 1900 3 3 27 1600 0 1 1 .66 18 23 46 150 6200
        correct true 23 46 9.0 360 110 0 0 0 23 46 150 6200
        correct false 3 3 150   7000 1800 3 3 27 1600 0 1 1 .66 18 0
    incorrect results 0 0 1 -32 6.3 260 0 0
        incorrect true 0 0 1 -32 6.3 260 0 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 49 3 -32 1 46
Run set symbiotic.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-Other