Tool CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 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] 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-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 9.2 450 85 -32 7.0 270 1 11   460 0 4.9 270 -32 .85 19 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 15   650 120 -32 5.4 280 -32 7.9 340 0 3.9 220 -32 .72 20 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 17   690 140 -32 5.7 260 -32 9.5 390 0 4.2 230 -32 .79 20 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 8.5 450 73 -32 5.4 270 1 7.8 360 0 3.7 220 -32 .68 19 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 22   950 180 - - - - 2 11    410 2 88     1100  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 17   710 130 - - - - 0 370    7000 2 61     930  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 14   650 120 - - - - 2 7.9  370 2 75     880  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 1 15   670 120 - - - - 0 .54 43 0 .019 4.8
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.0 320 45 - - - - 2 6.3  280 2 23     510  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.7 400 52 - - - - 2 5.5  270 2 17     530  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 9.7 470 77 -32 4.9 260 1 8.8 380 0 3.4 210 -32 .68 20 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 8.6 460 66 -32 5.1 270 1 7.4 380 0 3.6 220 -32 .66 20 - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 9.6 490 79 -32 5.4 280 1 9.0 390 0 3.7 220 -32 .67 20 - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 9.2 460 70 -32 4.6 260 1 5.2 370 0 3.4 220 -32 .74 20 - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 48   2100 380 -32 4.8 260 1 7.4 340 0 3.7 220 -32 .69 19 - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 48   2200 350 -32 5.8 270 -32 10   510 0 4.1 230 -32 .70 20 - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 1 70   2900 520 -32 5.5 270 1 10   440 0 4.2 220 -32 .70 20 - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 28   990 180 -32 6.1 260 1 9.3 400 0 3.8 220 -32 .67 20 - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 66   3100 520 -32 4.9 260 1 8.6 360 0 3.7 220 -32 .67 19 - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 6.6 310 53 -32 5.1 270 1 8.4 400 0 3.7 210 -32 .70 20 - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 6.8 320 59 -32 4.9 260 1 5.9 400 0 3.7 220 -32 .66 20 - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 4.6 290 42 -32 6.2 260 1 8.4 350 0 3.7 220 -32 .68 19 - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 31   1200 250 - - - - 2 11    520 2 41     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 29   1200 200 - - - - 2 12    510 2 38     1100  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 28   1200 210 - - - - 2 11    410 2 37     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 33   1300 230 - - - - 2 12    400 2 33     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 2 49   2300 360 - - - - 0 910    5100 2 34     840  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 4.0 280 36 - - - - 2 6.7  290 2 7.8   310  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 3.3 270 29 - - - - 2 4.7  270 2 5.5   270  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 2 25   1000 190 - - - - 0 910    5100 2 50     1000  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 2 45   1800 330 - - - - 0 910    5000 2 50     1100  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 2 21   1000 160 - - - - 0 900    5100 2 44     1000  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 2 250   7400 1500 - - - - 0 910    5400 2 38     980  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 2 41   1700 300 - - - - 0 900    4700 2 52     1000  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 2 69   2900 470 - - - - 0 900    4800 2 56     1100  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 4.5 300 39 -32 3.5 260 1 6.0 280 0 3.2 210 -32 .62 19 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 4.3 300 31 -32 3.5 280 1 6.5 290 0 3.4 210 -32 .61 19 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.2 280 31 - - - - 2 5.8  280 2 17     670  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3 270 34 - - - - 2 5.8  280 2 24     930  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3 270 27 - - - - 2 5.4  280 2 25     1900  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3 270 31 - - - - 2 5.6  290 2 41     3700  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.4 270 34 - - - - 2 6.1  290 2 70     6300  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3 270 31 - - - - 2 6.9  290 0 110     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.0 270 26 - - - - 2 5.8  270 2 7.3   290  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.0 270 26 - - - - 2 5.8  280 2 9.1   330  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.0 270 28 - - - - 2 5.1  280 2 9.5   380  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.2 280 32 - - - - 2 6.0  280 2 12     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3 280 30 - - - - 2 5.2  280 2 13     490  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 21   730 150 -32 14   430 -32 24   540 0 7.1 310 0 1.6  23 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 13   510 110 0 92   2100 -32 13   470 0 3.7 290 0 96    20 - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 24   940 180 -32 13   420 -32 25   580 0 6.4 290 0 96    20 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 12   480 90 -32 7.0 260 -32 12   460 0 4.8 270 0 .98 20 - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 23   970 170 0 7.9 300 -32 30   710 0 6.6 290 0 1.7  23 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 2 48   1900 360 - - - - 2 29    640 0 960     3000  
ntdrivers/diskperf_true-unreach-call.i.cil.c 2 16   700 120 - - - - 0 15    370 2 180     4500  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 1 34   1400 280 - - - - 0 .67 41 0 .018 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 2 35   1400 280 - - - - 0 900    3100 2 760     6700  
ntdrivers/parport_true-unreach-call.i.cil.c 2 39   1400 330 - - - - 0 16    460 2 260     4500  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 1 13   530 110 -32 6.5 260 1 35   560 0 4.0 220 0 .82 20 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 10   500 94 -32 5.6 280 1 32   560 0 4.0 220 0 .80 19 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 11   490 85 -32 5.3 260 1 34   560 0 4.0 220 0 .79 19 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 11   500 86 -32 5.4 270 1 35   560 0 4.7 220 0 .80 19 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 7.8 370 71 -32 5.6 260 -32 9.7 340 0 4.2 260 0 .81 19 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 7.2 360 64 -32 5.8 260 -32 8.7 320 0 4.3 260 0 .78 20 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 7.8 370 65 -32 5.5 260 -32 8.2 330 0 4.1 220 0 1.0  20 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 7.6 370 65 -32 5.6 260 -32 8.8 330 0 4.5 260 0 .81 20 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 17   620 130 -32 6.3 270 -32 8.7 330 0 4.6 220 0 .83 21 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 13   520 110 -32 5.7 270 -32 12   340 0 4.6 270 0 .79 20 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 34   1000 290 -32 6.2 270 -32 8.5 330 0 4.6 220 0 .84 21 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 13   500 100 -32 6.0 270 -32 9.7 360 0 4.5 230 0 .82 20 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 36   1200 270 -32 6.1 260 -32 8.4 330 0 4.6 270 0 .85 21 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 9.3 470 78 -32 5.9 260 -32 8.7 330 0 4.1 220 0 .82 20 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 17   650 150 -32 6.4 270 -32 8.2 330 0 4.6 270 0 .81 21 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 13   510 110 -32 6.4 270 -32 8.8 330 0 4.4 230 0 .84 20 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 17   700 120 -32 7.9 270 -32 8.1 330 0 4.5 230 0 .79 21 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 33   1000 280 -32 6.3 270 -32 8.6 320 0 4.8 270 0 .83 21 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 16   650 130 -32 7.6 270 -32 8.2 330 0 4.2 220 0 .82 21 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 1 36   1200 270 - - - - 0 900    1500 0 960     4600  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 1 50   1800 440 - - - - 0 900    1600 0 960     4600  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 1 41   1400 340 - - - - 0 900    1800 0 960     4600  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 1 42   1500 330 - - - - 0 900    1900 0 960     4600  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 1 18   660 130 - - - - 0 900    1700 0 960     6400  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 1 47   1700 420 - - - - 0 900    1900 0 960     4900  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 1 45   1400 330 - - - - 0 900    1800 0 960     6200  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 1 29   940 220 - - - - 0 900    1800 0 540     7000  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 1 32   920 270 - - - - 0 900    1900 0 550     7000  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 1 28   960 230 - - - - 0 900    1700 0 960     4900  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 1 22   700 160 - - - - 0 900    2100 0 610     7000  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 1 35   1100 270 - - - - 0 900    1800 0 800     7000  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 1 40   1100 280 - - - - 0 900    1800 0 490     7000  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 1 110   3700 1200 - - - - 0 900    1800 0 770     7000  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 1 55   1900 560 - - - - 0 900    2000 0 420     7000  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 1 38   1000 280 - - - - 0 900    1800 0 570     7000  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 1 40   1300 340 - - - - 0 900    2100 0 600     7000  
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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 94 104 2400 92000 19000 42 -1280 340 13000 42 -717 520 17000 42 0 180 9900 42 -576 230 840 52 44 23000 85000 52 62 16000 160000
    correct results 52 85 1200 50000 8900 0 19 19 260 7900 0 0 22 44 180 7500 31 62 2200 47000
        correct true 33 66 860 35000 6300 0 0 0 0 22 44 180 7500 31 62 2200 47000
        correct false 19 19 340 15000 2700 0 19 19 260 7900 0 0 0 0
    correct-unconfimed results 42 19 1200 42000 9800 0 0 0 0 0 0
        correct-unconfirmed true 19 19 750 25000 6500 0 0 0 0 0 0
        correct-unconfirmed false 23 0 420 16000 3300 0 0 0 0 0 0
    incorrect results 0 40 -1280 240 11000 23 -736 260 9000 0 18 -576 12 350 0 0
        incorrect true 0 40 -1280 240 11000 23 -736 260 9000 0 18 -576 12 350 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 104 -1280 -717 0 -576 44 62
Run set cpa-bam-slicing.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-ControlFlow