Tool CPAchecker 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-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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 26   990 200 1 18    730 -32 12     440   0 4.0  220 0 .71   19    - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 43   2000 340 1 20    490 1 12     500   0 3.5  210 0 .61   19    - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 45   1900 380 1 28    680 1 12     470   0 3.8  220 0 .67   19    - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 16   640 120 -32 4.3  270 1 7.5   330   0 3.6  220 -32 .69   19    - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c -16 26   810 210 - - - - 2 30    840 2 28     520  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c -16 10   480 90 - - - - 0 900    2000 2 11     400  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 86   3800 1100 - - - - 2 8.3  370 2 62     910  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 200   4000 2300 - - - - 2 9.4  370 2 79     980  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 11   500 95 - - - - 2 4.2  260 2 15     510  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 15   620 120 - - - - 2 6.8  270 2 19     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 42   1600 350 1 39    1900 1 9.8   370   0 3.5  220 0 .57   19    - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 110   4200 1300 1 38    1900 1 10     370   0 3.8  220 0 .63   19    - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 110   4200 1100 1 37    1900 1 11     410   0 3.8  210 0 .57   19    - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 110   4200 1200 1 37    1900 1 9.3   370   0 3.8  210 0 .57   19    - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 240   4500 2600 1 5.3  270 1 8.3   320   0 3.8  220 0 .57   19    - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 1 210   3800 2500 -32 5.0  270 1 9.4   440   0 3.8  220 -32 .70   20    - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 400   4700 5100 -32 5.0  270 -32 9.4   400   0 3.8  210 -32 .75   20    - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 73   3700 730 -32 4.8  270 1 7.8   360   0 3.9  220 -32 .72   20    - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 310   5200 3600 1 5.8  270 1 11     400   0 3.7  220 0 .58   19    - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 27   1300 240 1 5.1  280 1 9.7   360   0 3.8  220 0 .61   19    - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 25   1300 200 1 5.4  280 1 10     370   0 4.0  220 0 .60   19    - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 71   3800 710 -32 4.7  280 1 7.4   310   0 3.4  210 -32 .67   18    - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 54   3300 530 - - - - 2 14    410 2 29     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 39   2600 370 - - - - 2 14    400 2 35     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 44   2600 310 - - - - 2 12    430 2 33     1200  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 39   2600 360 - - - - 2 14    400 2 32     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 2 41   2600 410 - - - - 0 910    5000 2 30     910  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 9.9 450 84 - - - - 2 8.4  300 2 7.7   310  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 5.2 300 45 - - - - 2 4.7  280 2 6.4   260  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 2 120   3500 1300 - - - - 0 910    4800 2 48     1100  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 2 67   3200 740 - - - - 0 900    4700 2 38     1100  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 2 82   3400 950 - - - - 0 910    5000 2 37     960  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 2 67   3800 650 - - - - 0 910    6000 2 36     920  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 2 92   3900 1100 - - - - 0 910    4500 2 41     980  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 2 45   2400 380 - - - - 0 900    4600 2 30     1200  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 3.2 280 28 1 3.3  260 1 6.2   270   0 2.9  210 -32 .59   19    - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 3.1 270 30 1 3.4  270 1 6.1   270   0 3.2  210 -32 .60   19    - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 120   4700 1300 - - - - 0 5.1  270 2 19     700  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 310   6800 3600 - - - - 0 4.8  270 2 19     1100  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 920   13000 10000 - - - - 0 5.1  280 2 24     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 910   11000 12000 - - - - 0 .67 43 0 .031 4.9
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 910   10000 11000 - - - - 0 .50 43 0 .022 5.0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 910   10000 9900 - - - - 0 .65 41 0 .018 4.9
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 10   460 67 - - - - 0 5.5  270 2 7.9   270  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 13   620 93 - - - - 0 5.6  270 2 8.8   310  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 23   1300 150 - - - - 0 4.6  270 2 10     390  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 32   2400 310 - - - - 0 5.4  270 2 12     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 53   4000 540 - - - - 0 4.8  270 2 13     510  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 900   4800 11000 0 .51 43 0 .023 4.9 0 .85 47 0 .0012 .35 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 34   1200 280 0 92    2100 -32 14     470   0 5.4  280 0 96      20    - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 24   760 180 -32 7.0  280 -32 24     580   0 6.1  300 0 96      20    - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 28   1000 200 -32 5.9  270 -32 11     440   0 4.8  270 0 .98   19    - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 10   470 80 -32 7.1  300 0 78     930   0 6.7  300 0 1.6    22    - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c -16 33   1200 260 - - - - 2 39    740 2 24     540  
ntdrivers/diskperf_true-unreach-call.i.cil.c -16 40   1500 330 - - - - 0 8.8  400 2 14     490  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 1 150   3900 1700 - - - - 0 890    7000 0 960     5500  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 2 300   4100 3500 - - - - 0 900    3400 2 760     6700  
ntdrivers/parport_true-unreach-call.i.cil.c -16 17   610 140 - - - - 0 8.8  350 2 38     750  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 900   2600 13000 0 .51 41 0 .048 4.8 0 .88 48 0 .0037 .31 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 900   3600 12000 0 .56 44 0 .018 4.8 0 .85 47 0 .0019 .30 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 900   3400 13000 0 .55 43 0 .019 5.0 0 .86 49 0 .0017 .28 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 900   2500 11000 0 .56 44 0 .018 5.0 0 .81 49 0 .0039 .34 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 12   550 100 -32 5.2  260 -32 7.9   330   0 4.1  270 0 .83   19    - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 12   470 100 -32 5.2  270 -32 8.5   330   0 4.1  260 0 .79   19    - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 11   470 100 -32 5.2  270 -32 8.6   340   0 4.2  260 0 .78   19    - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 11   480 83 -32 5.2  270 -32 8.1   330   0 4.1  270 0 .81   19    - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 16   660 130 -32 5.3  260 0 97     820   0 4.3  260 0 .80   20    - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 21   650 170 -32 5.1  260 0 97     820   0 4.4  260 0 .83   20    - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 140   3800 1700 -32 5.9  270 0 96     1600   0 4.6  270 0 .81   21    - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 18   620 140 -32 5.2  270 0 97     800   0 4.1  260 0 .82   20    - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 84   3700 910 -32 5.7  280 0 96     1900   0 4.5  270 0 .79   20    - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 94   3800 900 -32 5.6  270 0 96     800   0 4.3  260 0 .77   19    - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 14   560 94 -32 5.6  260 0 96     880   0 4.4  260 0 .80   20    - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 20   680 160 -32 5.7  280 0 97     810   0 4.1  260 0 .83   20    - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 14   590 110 -32 5.1  260 0 96     850   0 4.2  230 0 .80   20    - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900   4100 13000 0 .57 45 0 .053 4.9 0 .89 49 0 .0040 .29 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 13   600 100 -32 5.4  260 0 96     810   0 4.1  260 0 .81   20    - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 900   3800 12000 - - - - 0 .53 43 0 .017 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 900   3800 11000 - - - - 0 .56 41 0 .018 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 900   3100 12000 - - - - 0 .52 43 0 .032 4.9
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 900   3200 11000 - - - - 0 .53 41 0 .025 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 1 370   4000 5400 - - - - 0 900    1700 0 960     6600  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 1 86   3500 940 - - - - 0 900    2100 0 900     5200  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 1 860   4800 12000 - - - - 0 900    1800 0 960     6600  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c -16 120   3100 1200 - - - - 0 12    370 2 8.0   330  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 1 850   4300 11000 - - - - 0 900    1800 0 600     7000  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c -16 100   3500 930 - - - - 0 12    440 2 8.7   340  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 1 400   3900 5500 - - - - 0 900    2000 0 470     7000  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c -16 97   3800 1100 - - - - 0 12    450 2 7.9   360  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 1 480   4700 5500 - - - - 0 900    1700 0 490     7000  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 1 160   3900 1700 - - - - 0 900    1700 0 820     7000  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 1 570   5000 6500 - - - - 0 900    2000 0 430     7000  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900   4200 11000 - - - - 0 .52 43 0 .020 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 1 820   4900 9400 - - - - 0 900    2100 0 560     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 -51 23000 280000 280000 42 -691 460 20000 42 -272 1300 21000 42 0 150 9000 42 -224 220   700 52 24 17000 73000 52 68 8700 97000
    correct results 42 67 3300 110000 36000 13 13 250 11000 16 16 150 5900 0 0 12 24 170 5100 34 68 1600 31000
        correct true 25 50 1900 68000 20000 0 0 0 0 12 24 170 5100 34 68 1600 31000
        correct false 17 17 1500 44000 16000 13 13 250 11000 16 16 150 5900 0 0 0 0
    correct-unconfimed results 29 10 5800 69000 70000 0 0 0 0 0 0
        correct-unconfirmed true 10 10 4800 43000 59000 0 0 0 0 0 0
        correct-unconfirmed false 19 0 980 26000 11000 0 0 0 0 0 0
    incorrect results 8 -128 440 15000 4200 22 -704 120 5900 9 -288 100 3700 0 7 -224 4.7 130 0 0
        incorrect true 0 22 -704 120 5900 9 -288 100 3700 0 7 -224 4.7 130 0 0
        incorrect false 8 -128 440 15000 4200 0 0 0 0 0 0
score (94 tasks, max score: 146) -51 -691 -272 0 -224 24 68
Run set interpchecker.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow