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 1 7.4  15 92   1 14   910 -32 6.3 260 1 .66 18 -
ntdrivers/floppy_false-valid-deref.i.cil.c 1 130    6100 1600   1 7.9 460 0 5.4 220 0 96    19 -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 7.3  880 100   1 5.0 260 0 4.1 210 0 1.0  19 -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .55 29 6.4 - - - 2 9.1 370
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .53 28 5.7 - - - 2 9.6 370
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .38 19 4.6 - - - 2 7.6 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .63 20 6.7 - - - 2 5.0 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .61 20 8.3 - - - 2 8.1 310
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.3  30 17   - - - 2 11   340
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.4  29 19   - - - 2 7.9 340
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .26 11 3.2 - - - 2 6.7 250
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .30 14 4.3 - - - 2 8.5 290
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .32 14 4.0 - - - 2 7.6 280
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.5 - - - 2 6.2 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.3 - - - 2 5.1 240
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .20 11 2.2 - - - 2 5.9 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.7 - - - 2 5.8 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.4 - - - 2 6.5 240
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.9 - - - 2 6.0 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 2 .22 11 2.2 - - - 2 5.2 230
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .20 11 2.4 - - - 2 5.3 250
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .19 11 2.0 - - - 2 4.5 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .19 11 2.3 - - - 2 4.9 220
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .21 11 2.5 - - - 2 5.6 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .21 11 2.6 - - - 2 6.3 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .21 11 2.2 - - - 2 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