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* [apollon024; apollon065; apollon077; apollon078] [apollon077; apollon078; apollon093] [apollon077; apollon078] [apollon073; apollon077; apollon078; apollon091; apollon099; apollon124]
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: 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 00:00:31 CET 2017-12-02 01:15:07 CET 2017-12-02 01:40:08 CET 2017-12-02 01:42:26 CET 2017-12-02 01:17:53 CET
Run set esbmc-incr.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Other
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0000.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-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.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 69    380 790   true -32 wit inspect 8.8  720 timeout 0 wit inspect 97     4700   true -32 wit inspect .95   23    - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect 17    510 200   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .0022 .30 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 16    370 210   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .57 44 6.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6   370  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .55 44 8.1 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8   370  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900    1200 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
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.9   300  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .19 31 2.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   300  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31 33 3.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0   340  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .32 34 4.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5   350  
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.5   250  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .17 31 2.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5   300  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .15 30 1.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   290  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2100 8900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2200 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2300 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2300 8600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2500 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2400 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2500 7100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2500 8000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1600 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1800 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1900 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2000 9000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    2000 9000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 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
total 26 18 13000   31000 130000 3 -32 9.7 810 3 0 97 4700 3 -32 .95 24 23 18 67 2900
    correct results 9 18 2.6 310 33 0 0 0 9 18 66 2900
        correct true 9 18 2.6 310 33 0 0 0 9 18 66 2900
        correct false 0 0 0 0 0
    correct-unconfimed results 1 0 69   380 790 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 69   380 790 0 0 0 0
    incorrect results 0 1 -32 8.8 720 0 1 -32 .95 23 0
        incorrect true 0 1 -32 8.8 720 0 1 -32 .95 23 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 18 -32 0 -32 18
Run set esbmc-incr.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Other