Tool ULTIMATE Automizer 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]
Date of execution 2017-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.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/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.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 54   1300 430 -32 7.4  270 1 13     470   0 4.9  260 -32 .84   20    - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 33   940 260 -32 6.8  270 1 9.2   390   0 5.4  240 -32 .86   20    - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 48   1200 400 -32 6.6  260 1 6.8   440   0 5.5  220 -32 .95   20    - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 16   660 120 -32 6.4  260 1 7.8   360   0 4.3  220 -32 .93   19    - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 100   2400 980 - - - - 2 15    410 2 100     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 66   1700 570 - - - - 0 400    7000 2 62     880  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 69   1800 650 - - - - 2 8.1  330 2 69     890  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 71   1800 730 - - - - 2 11    360 2 80     960  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 17   750 150 - - - - 2 5.5  270 2 17     500  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 17   660 130 - - - - 2 5.3  260 2 17     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 10   550 80 -32 5.5  260 1 7.8   370   0 3.9  210 -32 .75   19    - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 11   560 87 -32 6.2  260 1 5.5   370   0 3.9  210 -32 .80   19    - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 15   660 120 -32 5.7  270 1 8.2   380   0 3.9  210 -32 .90   20    - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 11   560 93 -32 6.6  270 1 8.2   370   0 4.4  210 -32 .78   19    - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 9.3 480 83 -32 5.7  260 1 9.2   340   0 5.0  220 -32 .83   19    - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 1 23   780 180 -32 8.0  270 1 13     470   0 6.0  230 -32 .87   20    - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 1 23   820 180 -32 7.6  280 1 9.8   430   0 5.2  220 -32 .82   20    - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 20   730 160 -32 6.0  270 1 10     390   0 5.3  220 -32 .87   20    - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 16   640 120 -32 7.2  260 1 5.9   350   0 4.9  220 -32 .69   19    - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 14   620 110 -32 6.2  270 1 9.4   390   0 4.0  220 -32 .72   20    - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 16   660 130 -32 6.8  260 1 9.7   390   0 4.4  230 -32 .72   20    - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 6.5 330 53 1 4.0  270 1 7.0   320   0 4.5  210 -32 .86   19    - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 29   1300 250 - - - - 2 13    520 2 33     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 35   1500 290 - - - - 2 15    510 2 23     1100  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 34   1400 240 - - - - 2 15    420 2 34     1200  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 31   1300 250 - - - - 2 11    400 2 34     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 1 24   1200 190 - - - - 0 910    5100 -16 16     510  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 7.4 370 59 - - - - 2 8.2  320 2 20     480  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 6.0 300 54 - - - - 2 6.6  280 2 9.9   370  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 2 56   2200 500 - - - - 0 910    5000 2 45     1100  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 2 52   2100 480 - - - - 0 900    4700 2 48     1100  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 2 49   2200 430 - - - - 0 910    4900 2 47     880  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 1 34   1300 290 - - - - 0 910    4800 -16 26     630  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 2 71   2600 650 - - - - 0 900    4800 2 52     1100  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 2 55   2300 580 - - - - 0 900    4900 2 45     1100  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 5.8 280 50 -32 3.5  260 1 7.6   290   0 3.4  210 -32 .71   19    - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 6.0 290 50 -32 3.7  260 1 5.0   280   0 3.7  210 -32 .84   19    - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 18   850 150 - - - - 2 6.4  280 2 18     720  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 25   1600 200 - - - - 2 7.2  290 2 21     1000  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 38   2600 330 - - - - 2 5.7  290 2 27     2300  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 65   4900 560 - - - - 2 5.8  290 2 45     3500  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 120   6500 1000 - - - - 2 7.1  290 2 60     5600  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 290   8700 2100 - - - - 2 7.5  290 0 110     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.6 320 49 - - - - 2 4.5  280 2 7.6   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 7.4 380 67 - - - - 2 3.9  280 2 8.6   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 8.6 510 66 - - - - 2 5.7  280 2 10     390  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 11   570 97 - - - - 2 6.4  280 2 11     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 14   730 120 - - - - 2 5.3  280 2 15     520  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 900   3100 9800 0 .54 41 0 .023 5.0 0 1.1  49 0 .0018 .30 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 1 16   720 130 0 92    2100 1 13     490   0 5.5  280 0 96      19    - -
ntdrivers/floppy_false-unreach-call.i.cil.c 1 82   3700 790 -32 12    420 1 29     1300   0 6.7  290 0 96      20    - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 900   2200 6600 0 .56 41 0 .020 4.9 0 .76 50 0 .0016 .28 - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 100   1300 790 0 .68 44 0 .020 5.0 0 1.1  49 0 .0017 .27 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 2 150   3300 1700 - - - - 2 26    640 2 150     1900  
ntdrivers/diskperf_true-unreach-call.i.cil.c 2 160   4700 1600 - - - - 0 13    360 2 160     4700  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 2 600   7500 6500 - - - - 0 910    6900 2 530     6900  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 2 600   6900 6500 - - - - 0 900    3400 2 740     6700  
ntdrivers/parport_true-unreach-call.i.cil.c 2 320   4900 3800 - - - - 0 22    420 2 240     4400  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 1 240   1600 2600 -32 6.7  260 1 29     530   0 5.4  220 0 .90   20    - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 82   1200 690 -32 6.1  270 1 28     520   0 4.4  220 0 1.0    19    - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 76   1100 720 -32 6.0  270 1 30     530   0 4.2  220 0 .91   19    - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 82   1000 800 -32 6.4  260 1 32     530   0 3.5  220 0 .75   19    - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 1 64   1600 650 -32 7.0  260 1 27     490   0 5.0  270 0 1.0    20    - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 1 62   1700 580 -32 4.3  260 1 27     490   0 4.5  220 0 .85   20    - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 1 64   1600 580 -32 6.3  260 1 18     490   0 4.4  220 0 1.1    20    - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 1 64   1700 560 -32 7.1  260 1 26     480   0 5.0  220 0 1.1    20    - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 900   5200 12000 0 .68 41 0 .019 5.0 0 1.1  49 0 .0020 .29 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 900   2500 10000 0 .54 42 0 .019 4.8 0 1.1  49 0 .0018 .31 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 900   5300 13000 0 .51 41 0 .024 4.9 0 1.1  49 0 .0014 .31 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 900   2400 12000 0 .69 41 0 .021 4.9 0 1.0  47 0 .0014 .31 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 900   5300 11000 0 .68 41 0 .018 4.9 0 1.1  49 0 .0015 .27 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 1 98   1800 830 -32 7.1  260 1 73     650   0 4.4  220 0 .91   20    - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 900   4600 11000 0 .52 41 0 .024 4.8 0 .84 49 0 .0018 .27 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 900   3700 11000 0 .52 44 0 .022 4.8 0 1.1  48 0 .0016 .29 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 900   4800 11000 0 .54 41 0 .020 4.8 0 1.1  49 0 .0015 .26 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900   5300 13000 0 .53 43 0 .020 4.9 0 .84 47 0 .0011 .26 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 900   4600 12000 0 .52 41 0 .023 4.9 0 .95 47 0 .0016 .26 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 900   4600 9200 - - - - 0 .52 41 0 .019 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 900   4600 8700 - - - - 0 .67 43 0 .018 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 900   4600 9400 - - - - 0 .60 41 0 .019 4.9
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 900   4600 11000 - - - - 0 .53 43 0 .018 5.0
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900   5400 11000 - - - - 0 .58 44 0 .019 4.9
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900   5200 10000 - - - - 0 .61 47 0 .025 5.0
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900   5500 12000 - - - - 0 .67 41 0 .019 5.0
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900   5900 11000 - - - - 0 .50 42 0 .020 4.9
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900   6400 12000 - - - - 0 .61 43 0 .018 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900   5400 13000 - - - - 0 .69 42 0 .018 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900   6600 13000 - - - - 0 .67 43 0 .019 5.0
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900   5300 10000 - - - - 0 .55 41 0 .019 4.9
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900   8900 8800 - - - - 0 .66 43 0 .021 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900   6500 9800 - - - - 0 .57 41 0 .017 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900   6900 11000 - - - - 0 .55 42 0 .018 5.0
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900   6000 11000 - - - - 0 .62 44 0 .020 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900   7400 10000 - - - - 0 .66 43 0 .021 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 97 31000 260000 360000 42 -863 280   10000 42 29 490 13000 42 0 150 7200 42 -576 220 570 52 46 8800 61000 52 32 2900 64000
    correct results 62 95 4500 110000 43000 1 1 4.0 270 29 29 490 13000 0 0 23 46 210 7800 32 64 2800 55000
        correct true 33 66 3200 82000 32000 0 0 0 0 23 46 210 7800 32 64 2800 55000
        correct false 29 29 1300 30000 12000 1 1 4.0 270 29 29 490 13000 0 0 0 0
    correct-unconfimed results 2 2 58 2500 480 0 0 0 0 0 0
        correct-unconfirmed true 2 2 58 2500 480 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 27 -864 180   7300 0 0 18 -576 15 350 0 2 -32 42 1100
        incorrect true 0 27 -864 180   7300 0 0 18 -576 15 350 0 0
        incorrect false 0 0 0 0 0 0 2 -32 42 1100
score (94 tasks, max score: 146) 97 -863 29 0 -576 46 32
Run set uautomizer.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-ControlFlow