Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon077; apollon078; apollon081; apollon164] [apollon052; apollon077; apollon078; apollon160] [apollon077; apollon078] [apollon040; apollon066; apollon077; apollon078; apollon139; apollon161]
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: [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-02 11:31:00 CET 2017-12-02 13:19:03 CET 2017-12-02 13:40:51 CET 2017-12-02 13:42:37 CET 2017-12-02 13:21:13 CET
Run set esbmc-kind.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Other
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1131.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/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1131.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) 0 wit inspect 72     370 620    true -32 wit inspect 8.5  690 timeout 0 wit inspect 97     4800   true -32 wit inspect .92   23    - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c timeout 0 wit inspect 900     1100 12000    error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 16     370 210    error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .54  44 6.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4 370
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .55  44 6.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8 380
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .28  31 3.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .23  31 2.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .20  31 2.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4 300
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31  33 4.3  - 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 .34  33 4.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5 340
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .13  29 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4 260
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .18  30 2.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9 290
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .17  30 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5 290
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13  27 .96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .10  27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 230
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .10  27 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5 240
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  27 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15  27 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  27 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2 230
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .10  27 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 220
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .088 27 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6 220
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .091 27 .75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2 220
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .098 27 .99 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 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 46 990   2500 13000 3 -32 9.7 780 3 0 97 4800 3 -32 .93 24 23 46 140 6200
    correct results 23 46 4.4 690 49 0 0 0 23 46 140 6200
        correct true 23 46 4.4 690 49 0 0 0 23 46 140 6200
        correct false 0 0 0 0 0
    correct-unconfimed results 1 0 72   370 620 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 72   370 620 0 0 0 0
    incorrect results 0 1 -32 8.5 690 0 1 -32 .92 23 0
        incorrect true 0 1 -32 8.5 690 0 1 -32 .92 23 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 46 -32 0 -32 46
Run set esbmc-kind.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Other