Tool ULTIMATE Kojak 0.1.23-3204b741 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-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 0 900   5400 13000 0 .55 42 0 .022 4.9 0 1.1  47 0 .0017 .26 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900   5100 11000 0 .52 43 0 .025 5.0 0 .66 50 0 .0015 .23 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 630   4300 9800 1 4.8  280 1 11     430   0 5.6  270 -32 .86   20    - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 45   1000 460 1 4.2  270 1 10     380   0 4.9  220 -32 .70   19    - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900   5500 12000 - - - - 0 .58 44 0 .020 4.8
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900   4000 12000 - - - - 0 .65 42 0 .018 4.9
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900   5300 12000 - - - - 0 .56 44 0 .018 4.8
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900   3900 12000 - - - - 0 .60 47 0 .019 5.0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 32   840 310 - - - - 2 5.5  270 -16 16     510  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 41   990 390 - - - - 2 6.7  270 2 25     580  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 350   4800 5500 -32 5.8  260 1 8.7   370   0 4.5  210 -32 .88   19    - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 210   4300 2400 -32 6.1  270 1 8.9   370   0 5.1  230 -32 .84   19    - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 250   4100 3000 -32 6.2  270 1 7.7   380   0 5.0  220 -32 .67   20    - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 200   4200 2400 -32 4.2  270 1 8.2   370   0 4.0  220 -32 .89   19    - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 7.8 400 61 -32 5.2  270 1 6.9   330   0 5.0  220 -32 .67   19    - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 900   6400 12000 0 .54 42 0 .018 4.9 0 1.1  49 0 .0017 .26 - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 900   6100 12000 0 .52 43 0 .023 4.8 0 1.1  47 0 .0016 .30 - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 0 900   6300 12000 0 .55 43 0 .023 4.9 0 .98 49 0 .0015 .35 - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 23   720 190 -32 6.9  270 1 8.1   350   0 5.5  240 -32 .67   19    - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 77   2000 880 -32 6.6  270 1 8.1   390   0 4.0  220 -32 .83   20    - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 69   1600 700 -32 6.1  270 1 5.6   400   0 4.8  240 -32 .88   20    - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 7.1 390 51 1 3.7  260 1 7.2   320   0 2.5  210 -32 .78   19    - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 0 900   6400 12000 - - - - 0 .69 41 0 .019 4.9
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 900   6100 12000 - - - - 0 .55 42 0 .018 4.8
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 0 900   6200 12000 - - - - 0 .66 42 0 .019 5.0
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 0 900   6300 13000 - - - - 0 .56 43 0 .019 4.9
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 900   6400 12000 - - - - 0 .72 43 0 .019 4.9
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 53   1500 660 - - - - 2 8.4  370 2 40     1000  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 15   590 130 - - - - 2 6.2  280 2 12     440  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 900   6300 12000 - - - - 0 .64 41 0 .019 4.8
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 900   6500 12000 - - - - 0 .68 43 0 .019 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 900   6300 11000 - - - - 0 .55 43 0 .020 4.9
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 900   6300 12000 - - - - 0 .59 41 0 .020 4.9
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 900   6400 14000 - - - - 0 .56 41 0 .019 5.0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 900   6200 12000 - - - - 0 .70 43 0 .024 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 5.8 320 46 -32 3.7  260 1 6.6   270   0 3.7  210 -32 .61   19    - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 5.4 290 44 -32 2.5  260 1 6.8   280   0 3.2  210 -32 .67   19    - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 31   890 390 - - - - 2 6.5  280 2 15     660  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 39   1100 500 - - - - 2 6.3  280 2 21     1000  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 48   1800 560 - - - - 2 5.6  290 2 31     1800  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 60   1500 720 - - - - 2 6.7  280 2 34     3400  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 77   1600 910 - - - - 2 6.6  290 2 69     5800  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 95   2800 1300 - - - - 2 7.0  290 0 98     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 8.8 500 82 - - - - 2 4.3  270 2 7.6   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 12   580 100 - - - - 2 4.6  280 2 8.2   310  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 18   680 180 - - - - 2 5.7  280 2 9.8   380  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 20   760 170 - - - - 2 5.7  280 2 11     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 25   860 290 - - - - 2 5.4  280 2 14     510  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 900   4900 13000 0 .55 43 0 .022 4.8 0 1.1  50 0 .0013 .35 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 1 60   840 610 0 92    2100 1 13     480   0 6.6  280 0 96      19    - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 900   1500 8000 0 .55 43 0 .018 4.8 0 1.1  50 0 .0016 .27 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 900   4400 11000 0 .54 41 0 .018 5.0 0 1.1  47 0 .0036 .34 - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 900   1300 10000 0 .39 43 0 .018 4.9 0 .89 49 0 .0015 .27 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 900   4400 13000 - - - - 0 .58 41 0 .019 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 900   4900 10000 - - - - 0 .55 44 0 .017 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 900   2100 8900 - - - - 0 .59 44 0 .019 5.0
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 900   1700 9200 - - - - 0 .55 42 0 .019 4.8
ntdrivers/parport_true-unreach-call.i.cil.c 0 900   4700 13000 - - - - 0 .68 43 0 .019 4.8
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 390   3400 4900 0 .53 43 0 .018 4.9 0 1.0  47 0 .0015 .27 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 410   3500 4900 0 .55 45 0 .025 4.9 0 .68 50 0 .0014 .29 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 320   2600 3900 0 .55 41 0 .024 4.9 0 1.1  47 0 .0017 .26 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 350   2900 4700 0 .56 43 0 .025 4.8 0 1.1  49 0 .0012 .32 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 540   3900 7800 0 .50 41 0 .018 4.8 0 1.1  49 0 .0013 .27 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 550   4700 9100 0 .54 43 0 .025 5.0 0 .99 47 0 .0015 .27 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 460   4800 6700 0 .53 42 0 .024 4.8 0 .85 50 0 .0014 .35 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 480   3800 6400 0 .68 43 0 .019 4.8 0 .87 51 0 .0015 .32 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 900   2900 11000 0 .62 44 0 .033 4.8 0 1.1  50 0 .0017 .31 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 900   5500 12000 0 .55 41 0 .019 4.9 0 .87 49 0 .0017 .27 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 900   4400 15000 0 .56 43 0 .046 4.8 0 1.1  49 0 .0015 .29 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 900   5500 11000 0 .53 41 0 .024 4.8 0 .93 51 0 .0015 .27 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 900   5300 12000 0 .41 41 0 .019 4.8 0 .90 49 0 .0018 .29 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 900   5000 13000 0 .59 44 0 .024 4.8 0 .99 50 0 .0022 .29 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 900   3400 15000 0 .64 41 0 .017 4.8 0 1.1  49 0 .0013 .27 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 900   5500 14000 0 .55 46 0 .024 4.8 0 1.1  49 0 .0015 .34 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 900   3700 13000 0 .52 41 0 .021 4.8 0 1.1  47 0 .0016 .26 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900   4800 13000 0 .57 44 0 .024 4.8 0 1.0  50 0 .0012 .29 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 900   3900 13000 0 .70 41 0 .019 4.8 0 .82 47 0 .0016 .26 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 900   5400 13000 - - - - 0 .56 43 0 .020 4.8
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 900   5400 13000 - - - - 0 .52 42 0 .019 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 900   4700 13000 - - - - 0 .64 44 0 .021 5.0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 900   5300 14000 - - - - 0 .70 43 0 .019 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900   5500 13000 - - - - 0 .39 44 0 .019 4.8
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900   5500 12000 - - - - 0 .59 41 0 .019 4.9
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900   5500 13000 - - - - 0 .63 41 0 .019 4.8
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900   5100 12000 - - - - 0 .61 42 0 .019 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900   5500 12000 - - - - 0 .71 43 0 .020 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900   5500 14000 - - - - 0 .68 43 0 .019 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900   5500 13000 - - - - 0 .54 41 0 .020 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900   5500 13000 - - - - 0 .55 43 0 .019 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900   5500 14000 - - - - 0 .71 43 0 .018 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900   5500 15000 - - - - 0 .65 41 0 .022 5.0
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900   5500 13000 - - - - 0 .57 43 0 .018 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900   5500 12000 - - - - 0 .68 42 0 .019 4.8
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900   5500 12000 - - - - 0 .65 44 0 .018 4.8
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 44 57000 370000 780000 42 -317 170 6800 42 14 120 5300 42 0 92 4500 42 -416 110   280 52 30 110 5900 52 10 410 24000
    correct results 29 44 2500 46000 33000 3 3 13 810 14 14 120 5100 0 0 15 30 91 4300 13 26 300 17000
        correct true 15 30 570 17000 6700 0 0 0 0 15 30 91 4300 13 26 300 17000
        correct false 14 14 1900 29000 26000 3 3 13 810 14 14 120 5100 0 0 0 0
    incorrect results 0 10 -320 53 2700 0 0 13 -416 10   250 0 1 -16 16 510
        incorrect true 0 10 -320 53 2700 0 0 13 -416 10   250 0 0
        incorrect false 0 0 0 0 0 0 1 -16 16 510
score (94 tasks, max score: 146) 44 -317 14 0 -416 30 10
Run set ukojak.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-ControlFlow