Tool ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-14 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]]
Run set sv-comp17.MemSafety-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
loop-acceleration/array3_false-valid-deref.i 0 900   760   12000 1600 2.3 0   .52 .35 11 40 7.0 3.7 130 330
ntdrivers/floppy_false-valid-deref.i.cil.c 0 7.3 1.9 48 340 2.5 0   .51 .34 13 40 7.0 3.7 140 310
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 0 5.3 1.7 46 310 2.5 0   .52 .33 12 40 6.9 3.6 130 300
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 8.0 2.4 66 460 3.3 0   36 21   660 2400 11   6.0 170 410
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 8.7 2.5 64 460 3.3 0   40 22   600 2200 11   6.0 170 430
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 7.1 2.1 52 360 2.9 0   210 120   1800 7000 9.7 5.2 150 340
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 7.1 2.2 57 350 2.9 0   44 27   760 2700 9.8 5.2 150 330
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 7.4 2.2 52 360 2.9 0   42 26   720 2600 9.8 5.2 180 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 8.1 2.3 57 410 3.1 0   66 41   740 3600 11   5.7 150 360
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 8.1 2.3 61 430 3.1 0   74 45   1000 3400 10   5.6 200 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.3 1.9 46 320 2.7 0   11 5.5 170 380 8.1 4.4 150 320
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.8 2.1 52 330 2.8 0   23 12   370 960 9.4 5.0 150 330
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.9 2.1 53 330 2.8 0   21 11   360 1100 9.5 5.1 190 320
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.1 1.9 48 330 2.6 0   910 810   16000 7000 7.7 4.1 160 320
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.6 1.8 41 320 2.6 0   780 660   14000 7000 7.3 3.9 130 320
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.3 1.7 46 340 2.6 0   730 610   7900 7000 7.2 3.9 130 320
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.2 1.8 53 330 2.6 0   640 550   11000 7000 8.7 4.7 100 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 2 6.7 1.9 53 360 2.6 0   630 550   8200 7000 7.5 4.0 110 310
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.3 1.9 46 340 2.6 0   960 850   19000 6700 6.7 3.7 99 320
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 2 6.0 1.8 51 330 2.6 0   910 830   14000 6000 7.8 4.1 140 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.8 1.8 44 310 2.6 0   960 860   12000 6500 7.5 4.0 150 310
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.5 1.7 43 310 2.6 0   830 740   10000 7000 6.7 3.7 130 310
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.3 1.8 47 330 2.6 0   910 810   14000 6700 7.2 3.8 140 320
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.5 1.8 38 320 2.6 0   910 810   12000 6500 7.8 4.1 150 320
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.3 1.8 43 320 2.6 0   910 820   15000 6500 7.3 3.9 150 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 5.8 1.8 46 340 2.6 0   920 820   14000 6700 6.7 3.7 140 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 26 46 1100 810 13000 10000 71 0   26 1.6 1.0 36 120   26 21 11 400 950   26 12000 10000 170000 110000 26 200 110 3400 7600
    correct results 23 46 150 46 1200 8100 63 0   0 0   0   0 0   0 0 0 0 0   9 12000 10000 170000 110000 23 200 110 3400 7600
        correct true 23 46 150 46 1200 8100 63 0   0 0   0   0 0   0 0 0 0 0   9 12000 10000 170000 110000 23 200 110 3400 7600
        correct false 0
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (26 tasks, max score: 49) 46
Run set sv-comp17.MemSafety-Other