Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker skink symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
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
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-01 19:00:34 CET 2017-12-01 22:03:39 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET
Run set 2ls.sv-comp18.ReachSafety-ControlFlow cbmc.sv-comp18.ReachSafety-ControlFlow cpa-bam-bnb.sv-comp18.ReachSafety-ControlFlow cpa-bam-slicing.sv-comp18.ReachSafety-ControlFlow cpa-seq.sv-comp18.ReachSafety-ControlFlow depthk.sv-comp18.ReachSafety-ControlFlow esbmc-incr.sv-comp18.ReachSafety-ControlFlow esbmc-kind.sv-comp18.ReachSafety-ControlFlow interpchecker.sv-comp18.ReachSafety-ControlFlow skink.sv-comp18.ReachSafety-ControlFlow symbiotic.sv-comp18.ReachSafety-ControlFlow uautomizer.sv-comp18.ReachSafety-ControlFlow ukojak.sv-comp18.ReachSafety-ControlFlow utaipan.sv-comp18.ReachSafety-ControlFlow veriabs.sv-comp18.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1.3  380 19    1 1.4  160 15   1 12   480 87 1 9.2 450 85 1 8.8 340 77 1 3.3  88 46   1 1.0  47 12   1 .98  47 12    1 27   1000 210 1 88   1600 590 0 .39 16 4.7 1 54   1300 430 1 900   5400 13000 0 58   1300 440 1 200 830 2100 0
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c .38 65 3.2  1 .48 41 5.5 1 35   1600 270 1 15   650 120 0 6.9 300 53 1 1.6  94 23   1 .76 33 7.8 1 .76  33 6.9  1 46   1500 390 1 52   960 530 0 .26 13 3.7 1 33   940 260 1 900   5100 11000 0 33   950 270 1 270 370 3400 1
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c .54 130 6.2  1 .76 60 10   1 38   1800 320 0 17   690 140 0 8.1 330 65 1 2.6  100 32   1 1.0  36 9.6 1 1.0   36 9.0  1 41   2200 360 1 50   1100 430 0 .38 14 4.5 1 48   1200 400 1 630   4300 9800 1 50   1300 430 1 270 390 2900 1
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c .28 41 2.2  1 .39 38 4.5 1 13   510 86 0 8.5 450 73 1 5.8 300 47 1 1.2  63 15   1 .49 32 4.3 1 .53  32 4.3  1 17   630 140 1 28   930 260 0 .24 13 2.9 1 16   660 120 1 45   1000 460 1 16   640 130 1 260 340 3000 1
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 1.4  410 15    2 2.9  160 31   2 42   2000 350 2 22   950 180 2 8.3 330 62 2 18    350 190   2 .64 45 8.6 2 .64  45 7.2  2 23   820 200 -16 94   1500 570 0 .42 16 5.7 2 100   2400 980 2 900   5500 12000 0 900   3900 12000 0 200 840 1400 0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c .53 110 5.0  2 870    4500 3700   0 53   3000 510 2 17   710 130 2 100   1300 1300 2 140    100 1700   0 900    990 9400   0 .32  31 3.7  2 10   470 79 -16 53   1200 410 0 .35 13 3.7 2 66   1700 570 2 900   4000 12000 0 600   4600 6800 2 890 670 8500 0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c .36 71 4.7  2 .84 42 8.7 2 27   1500 220 1 14   650 120 2 7.4 310 70 2 10    350 89   2 .23 31 2.9 2 .22  31 2.9  2 84   3700 940 2 51   970 500 0 .29 13 3.0 2 69   1800 650 2 900   5300 12000 0 900   4600 12000 0 280 510 2700 2
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c .58 140 5.9  2 1.4  60 15   2 36   1900 280 1 15   670 120 1 8.0 330 66 2 13    370 120   2 .38 34 4.8 2 .36  34 4.6  2 190   3900 2300 2 49   1100 410 0 .38 14 5.6 2 71   1800 730 2 900   3900 12000 0 900   4600 12000 0 280 610 2900 2
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c .18 27 1.6  2 .52 35 5.2 2 7.0 380 64 2 6.0 320 45 2 4.9 280 40 2 5.3  270 47   2 .13 28 1.5 2 .12  29 1.2  2 11   480 89 2 29   800 300 0 .19 11 2.4 2 17   750 150 2 32   840 310 2 16   720 140 2 260 350 2500 2
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c .27 47 2.6  2 .63 36 9.3 2 8.8 470 63 2 6.7 400 52 2 6.3 290 49 2 7.1  290 75   2 .19 30 1.7 2 .15  30 1.7  2 17   640 130 2 27   820 230 0 .27 12 2.4 2 17   660 130 2 41   990 390 2 17   620 130 2 270 450 3700 2
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 9.6  170 69    1 2.0  87 24   1 15   530 110 1 9.7 470 77 1 6.4 300 47 1 20    92 320   1 2.8  64 27   1 2.1   56 27    1 39   1500 320 1 67   750 720 0 .29 12 3.1 1 10   550 80 1 350   4800 5500 1 10   570 83 1 58 440 670 1
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 10    180 91    1 2.1  87 23   1 14   520 110 1 8.6 460 66 1 6.7 300 52 1 20    85 260   1 2.8  65 25   1 2.3   56 24    1 110   4200 1200 1 44   720 440 0 .28 12 3.4 1 11   560 87 1 210   4300 2400 1 10   550 73 1 61 450 610 1
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 15    230 140    0 2.4  100 30   1 15   550 120 1 9.6 490 79 1 6.1 300 46 1 24    95 390   0 3.6  75 40   1 2.8   65 27    1 110   4200 1100 1 53   720 560 0 .32 12 3.5 1 15   660 120 1 250   4100 3000 1 15   650 120 1 62 490 650 1
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 9.1  180 80    1 2.1  87 24   1 13   530 93 1 9.2 460 70 1 6.3 300 49 1 21    85 290   1 3.0  65 33   1 2.4   57 25    1 100   4200 1300 1 72   750 750 0 .28 12 3.9 1 11   560 93 1 200   4200 2400 1 14   610 120 1 60 450 630 1
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c .30 42 2.9  1 .31 35 3.0 1 45   1900 330 1 48   2100 380 1 3.8 280 35 1 4.0  87 49   1 .35 31 2.9 1 .63  31 6.8  1 240   4500 2500 1 110   820 1400 0 .26 12 2.6 1 9.3 480 83 1 7.8 400 61 1 9.3 470 73 1 92 720 1100 1
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 14    230 110    1 14    330 170   1 18   600 140 1 48   2200 350 0 100   800 1400 1 24    88 330   1 3.8  71 38   1 4.8   86 61    1 210   3700 3000 1 9.9 500 93 0 .39 14 5.4 1 23   780 180 1 900   6400 12000 0 39   4300 370 1 360 910 4300 1
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 16    230 120    1 3.5  150 41   1 240   6600 2000 1 70   2900 520 1 160   860 1800 1 42    98 620   1 4.1  75 40   1 3.6   66 36    1 420   4700 4900 0 11   640 90 0 1.1  23 14   1 23   820 180 1 900   6100 12000 0 710   4900 8400 1 240 1000 3500 1
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 13    170 96    1 3.3  140 37   1 900   4600 9500 0 28   990 180 1 5.4 290 44 1 16    94 200   1 2.5  51 22   1 2.4   44 19    1 75   3700 860 1 150   1100 1800 0 .31 13 3.5 1 20   730 160 1 900   6300 12000 0 21   720 170 1 120 920 1300 1
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 4.9  89 37    1 .32 35 3.1 1 74   3400 600 1 66   3100 520 1 8.8 380 70 1 14    90 170   1 1.3  34 15   1 1.2   31 15    1 310   5200 3600 1 15   650 130 0 .23 12 3.4 1 16   640 120 1 23   720 190 1 16   640 130 1 120 900 1200 1
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 13    170 100    1 3.1  140 38   1 8.5 410 70 1 6.6 310 53 1 5.9 290 45 1 21    320 280   1 1.9  50 14   1 1.7   44 16    1 27   1300 240 1 14   640 120 0 .28 12 3.0 1 14   620 110 1 77   2000 880 1 15   630 130 1 110 840 1300 1
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 8.9  150 77    1 3.0  130 35   1 7.7 420 60 1 6.8 320 59 1 5.5 290 45 1 10    89 120   1 2.1  49 21   1 1.7   42 19    1 27   1200 240 1 15   660 110 0 .29 12 3.1 1 16   660 130 1 69   1600 700 1 16   660 130 1 110 830 1400 1
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c .28 43 2.8  1 .32 37 2.8 1 4.4 300 38 1 4.6 290 42 1 3.3 260 29 1 14    92 180   1 .33 31 3.5 1 1.1   31 11    1 71   3800 830 1 14   660 120 0 .25 12 2.6 1 6.5 330 53 1 7.1 390 51 1 6.2 320 50 1 120 940 1300 1
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 9.0  250 82    2 25    380 270   2 22   1000 170 2 31   1200 250 2 13   710 120 2 150    1300 1800   2 12    180 130   2 14     190 160    2 53   3200 510 2 67   730 760 0 .60 13 7.2 2 29   1300 250 2 900   6400 12000 0 440   5300 5300 2 95 640 1000 1
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 11    250 95    2 26    390 260   2 10   480 88 2 29   1200 200 2 13   720 120 2 150    1300 1900   2 12    180 130   2 14     200 210    2 39   2400 330 2 46   720 520 0 .60 13 7.1 2 35   1500 290 2 900   6100 12000 0 500   5400 6500 2 94 660 950 1
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 16    320 140    2 30    460 420   2 9.9 470 84 2 28   1200 210 2 14   730 140 2 180    1300 2000   2 14    210 150   2 17     240 180    2 43   2300 350 2 47   720 490 0 .61 13 7.3 2 34   1400 240 2 900   6200 12000 0 550   5500 6500 2 100 700 1100 1
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 9.9  260 86    2 26    390 300   2 9.7 480 76 2 33   1300 230 2 13   720 120 2 160    1300 2300   2 12    180 140   2 15     200 170    2 37   2400 340 2 33   700 370 0 .59 13 8.1 2 31   1300 250 2 900   6300 13000 0 440   5400 5700 2 96 640 1200 1
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 900    8200 12000    0 870    1100 4900   0 14   510 98 2 49   2300 360 2 14   730 140 1 890    470 10000   0 900    2400 8000   0 900     2400 11000    0 41   2300 350 2 14   650 110 0 900    640 10000   0 24   1200 190 1 900   6400 12000 0 900   5400 12000 0 900 1400 5100 0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c .61 39 9.0  2 870    1100 3600   0 4.4 310 40 2 4.0 280 36 2 3.1 250 26 2 370    110 4800   0 900    1900 9700   0 900     1900 10000    0 8.3 460 75 2 31   690 310 0 900    81 10000   0 7.4 370 59 2 53   1500 660 2 7.5 370 56 2 900 2800 5400 0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c .39 29 4.8  2 870    2700 5100   0 3.5 280 34 2 3.3 270 29 2 2.6 250 24 2 120    77 1600   0 900    2300 8900   0 900     2300 8300    0 5.3 290 37 2 96   720 1000 0 900    58 11000   0 6.0 300 54 2 15   590 130 2 5.7 290 52 2 860 1800 4500 0
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 900    7800 10000    0 870    1200 5400   0 9.1 460 74 2 25   1000 190 2 14   730 120 1 44    2300 470   2 900    2300 10000   0 900     2300 8200    0 110   3400 1300 2 15   650 130 0 900    220 9800   0 56   2200 500 2 900   6300 12000 0 900   5400 11000 0 900 1500 5400 0
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 900    7800 9700    0 870    1200 4300   0 12   530 97 2 45   1800 330 2 14   730 140 1 890    460 10000   0 900    2300 9100   0 900     2300 8600    0 68   3000 740 2 16   640 140 0 900    220 10000   0 52   2100 480 2 900   6500 12000 0 500   4700 5900 2 900 1500 5300 0
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 900    7800 10000    0 870    1200 5200   0 9.0 470 79 2 21   1000 160 2 14   730 150 1 890    460 14000   0 900    2300 8100   0 900     2300 9400    0 82   3300 1000 2 16   640 150 0 900    220 10000   0 49   2200 430 2 900   6300 11000 0 200   4900 2400 2 900 1500 5600 0
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 900    7800 10000    0 870    1200 4700   0 18   690 160 2 250   7400 1500 2 81   2300 1100 1 890    450 13000   0 900    2300 9800   0 900     2200 7700    0 66   3800 680 2 20   670 160 0 900    220 10000   0 34   1300 290 1 900   6300 12000 0 900   5400 10000 0 900 1700 7200 0
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 900    7900 12000    0 870    1200 6400   0 13   540 110 2 41   1700 300 2 46   1300 460 1 890    470 11000   0 900    2400 11000   0 900     2400 8100    0 87   3800 850 2 18   660 180 0 900    220 10000   0 71   2600 650 2 900   6400 14000 0 240   4900 3300 2 900 1600 5200 0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 900    7800 9400    0 870    1200 4700   0 14   490 110 2 69   2900 470 2 14   740 140 1 49    2300 590   2 900    2300 8800   0 900     2200 8000    0 44   3000 390 2 16   700 130 0 900    220 9600   0 55   2300 580 2 900   6200 12000 0 900   5400 12000 0 900 1600 5600 0
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c .14 26 1.3  1 .31 33 3.0 1 4.8 300 44 1 4.5 300 39 1 3.3 270 32 1 .48 79 6.1 1 .79 29 6.0 1 .76  29 6.6  1 3.2 270 30 1 6.0 330 58 0 .18 11 1.9 1 5.8 280 50 1 5.8 320 46 1 6.3 280 49 1 27 290 230 1
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c .15 28 1.2  1 .33 36 3.5 1 4.8 300 46 1 4.3 300 31 1 3.8 270 34 1 .50 79 6.5 1 .82 29 6.2 1 .86  29 7.0  1 3.2 270 30 1 5.7 320 53 0 .16 11 1.9 1 6.0 290 50 1 5.4 290 44 1 6.1 290 49 1 29 280 270 1
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c .14 24 1.1  2 870    3300 6400   0 3.3 280 32 2 3.2 280 31 2 15   740 120 2 30    1300 300   2 900    2100 8000   0 .099 27 1.1  2 120   4700 1400 2 4.1 260 42 2 .16 11 1.5 2 18   850 150 2 31   890 390 2 20   850 150 2 18 310 170 2
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c .14 27 .98 2 870    4000 5600   0 3.5 280 29 2 3.3 270 34 2 44   1200 470 2 89    2200 1200   2 900    2300 8200   0 .11  27 1.1  2 310   6900 3700 2 4.3 270 43 2 .13 11 1.5 2 25   1600 200 2 39   1100 500 2 26   1400 180 2 19 320 150 2
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c .15 27 1.0  2 870    4800 7300   0 3.4 280 33 2 3.3 270 27 2 150   1300 1900 2 160    2300 2000   2 900    2300 7100   0 .12  27 1.4  2 940   13000 11000 0 4.4 270 41 2 .14 11 1.5 2 38   2600 330 2 48   1800 560 2 37   3000 320 2 20 310 170 2
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c .14 26 1.0  2 870    5500 6300   0 3.3 280 32 2 3.3 270 31 2 150   1200 1800 2 160    2300 1900   2 900    2400 7800   0 .12  27 1.4  2 910   11000 11000 0 4.2 270 44 2 .13 11 1.5 2 65   4900 560 2 60   1500 720 2 51   4600 450 2 21 340 180 2
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c .15 26 1.2  2 870    6200 5700   0 3.4 270 30 2 3.4 270 34 2 150   1200 1900 2 160    2200 1800   2 900    2500 8400   0 .14  27 1.4  2 910   10000 11000 0 4.3 280 35 2 .13 11 1.8 2 120   6500 1000 2 77   1600 910 2 130   6100 1000 2 21 300 200 2
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c .15 26 1.1  2 870    6900 6300   0 3.4 270 32 2 3.3 270 31 2 150   1200 1700 2 160    2200 2100   2 900    2500 7400   0 .14  27 1.3  2 910   10000 10000 0 4.4 290 43 2 .14 11 1.5 2 290   8700 2100 2 95   2800 1300 2 290   8800 2000 2 24 370 220 2
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c .13 23 .82 2 870    5900 7800   0 2.9 280 27 2 3.0 270 26 2 3.1 250 26 2 4.3  260 44   2 900    1700 8100   0 .12  27 .70 2 9.0 460 79 2 4.3 260 40 2 .13 11 1.6 2 6.6 320 49 2 8.8 500 82 2 9.1 390 81 2 14 290 120 2
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c .14 23 .86 2 870    7900 6300   0 3.0 270 31 2 3.0 270 26 2 3.5 260 27 2 4.9  270 50   2 900    1800 8000   0 .10  27 1.0  2 12   630 98 2 4.2 310 44 2 .13 11 1.5 2 7.4 380 67 2 12   580 100 2 7.3 380 62 2 15 320 120 2
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c .12 24 .95 2 870    1900 5600   0 3.0 280 29 2 3.0 270 28 2 4.3 270 35 2 6.3  300 62   2 900    1900 7500   0 .11  27 1.1  2 22   1300 170 2 4.0 260 41 2 .16 11 1.4 2 8.6 510 66 2 18   680 180 2 9.2 520 69 2 15 300 120 2
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c .12 24 .82 2 870    2300 5600   0 3.1 280 31 2 3.2 280 32 2 6.0 290 47 2 9.5  450 80   2 900    2000 7700   0 .12  27 1.1  2 32   2100 290 2 4.1 260 38 2 .14 11 1.4 2 11   570 97 2 20   760 170 2 11   590 86 2 17 320 160 2
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c .11 24 1.0  2 870    2800 5100   0 3.2 270 29 2 3.3 280 30 2 8.4 430 68 2 14    720 140   2 900    2100 7200   0 .13  27 .84 2 54   4000 560 2 4.0 260 36 2 .13 11 1.7 2 14   730 120 2 25   860 290 2 14   670 120 2 17 290 130 2
ntdrivers/cdaudio_false-unreach-call.i.cil.c .56 63 4.3  0 100    5100 1300   0 900   4300 12000 0 21   730 150 0 54   1800 580 1 890    350 11000   0 900    5800 14000   0 1.5   290 18    0 900   4900 9000 0 69   1700 380 0 1.0  36 12   1 900   3100 9800 0 900   4900 13000 0 900   5300 12000 0 74 360 570 0
ntdrivers/diskperf_false-unreach-call.i.cil.c .60 44 5.3  0 1.7  120 17   1 22   890 150 1 13   510 110 0 15   510 150 1 480    170 6900   0 1.1  87 12   1 1.0   88 12    0 28   1100 240 0 59   1400 290 0 .59 29 8.0 0 16   720 130 1 60   840 610 1 20   750 160 1 55 320 430 0
ntdrivers/floppy_false-unreach-call.i.cil.c 2.2  59 19    0 3.5  170 38   0 32   1300 220 0 24   940 180 0 11   470 100 1 590    830 7000   0 13    460 170   0 900     1100 11000    0 22   710 180 0 32   1100 170 0 .92 43 11   0 82   3700 790 1 900   1500 8000 0 900   6300 11000 0 80 360 640 0
ntdrivers/kbfiltr_false-unreach-call.i.cil.c .41 36 3.7  0 1.5  73 15   0 16   700 120 1 12   480 90 0 12   460 110 1 890    540 9700   0 .65 72 8.7 0 .63  73 9.1  0 28   1100 230 0 20   760 120 0 .50 32 5.0 1 900   2200 6600 0 900   4400 11000 0 900   4700 10000 0 37 280 290 0
ntdrivers/parport_false-unreach-call.i.cil.c 3.0  100 25    0 14    790 150   1 35   1400 280 0 23   970 170 0 11   470 96 1 590    960 7900   0 7.3  350 87   0 28     490 310    0 10   470 80 0 340   1700 1700 0 1.7  120 18   0 100   1300 790 0 900   1300 10000 0 150   1400 1400 0 520 2500 5000 0
ntdrivers/cdaudio_true-unreach-call.i.cil.c .53 64 6.1  0 39    410 470   2 900   4200 12000 0 48   1900 360 2 12   480 110 2 900    350 11000   0 .77 280 8.4 0 .87  280 10    0 38   1100 320 -16 53   1500 260 0 .97 35 13   0 150   3300 1700 2 900   4400 13000 0 900   4800 10000 0 78 370 610 0
ntdrivers/diskperf_true-unreach-call.i.cil.c .60 46 6.1  0 880    7500 5000   0 30   1500 260 2 16   700 120 2 99   1900 1300 2 640    170 8400   0 .51 83 6.7 0 .31  82 4.4  0 44   1600 370 -16 83   1700 390 0 .80 40 8.4 0 160   4700 1600 2 900   4900 10000 0 900   6300 13000 0 740 2300 6400 0
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 820    2800 4200    0 870    7500 7100   0 900   4300 11000 0 34   1400 280 1 81   2000 780 2 890    14000 13000   0 900    7200 8300   0 900     430 11000    0 150   3900 1800 1 5.0 350 50 0 2.2  57 30   0 600   7500 6500 2 900   2100 8900 0 900   6100 9500 0 150 1300 1300 0
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 2.3  61 20    0 870    4400 5800   0 38   1500 290 1 35   1400 280 2 39   920 360 2 890    1300 8700   0 900    8000 8200   0 900     1000 11000    0 290   4100 3800 2 32   1200 180 0 .90 43 12   0 600   6900 6500 2 900   1700 9200 0 900   6300 12000 0 79 390 670 0
ntdrivers/parport_true-unreach-call.i.cil.c 3.1  100 32    0 880    5200 5700   0 110   4400 940 1 39   1400 330 2 120   2700 1200 2 890    2000 11000   0 900    5700 9300   0 33     660 420    2 16   630 120 -16 340   1700 1500 0 1.6  120 19   0 320   4900 3800 2 900   4700 13000 0 710   4800 8200 2 530 2500 3800 0
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c .78 180 8.0  0 15    470 170   1 14   530 100 0 13   530 110 1 61   2500 580 1 890    1600 8200   0 14    650 150   1 19     790 190    1 900   3000 13000 0 9.6 540 85 0 .36 12 3.5 0 240   1600 2600 1 390   3400 4900 0 180   990 1800 1 720 1600 6000 0
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c .80 180 9.0  0 5.4  210 58   1 13   490 110 1 10   500 94 1 63   3300 600 1 890    1600 8500   0 15    650 140   1 11     510 140    1 900   3300 12000 0 9.8 540 87 0 .33 12 4.4 0 82   1200 690 1 410   3500 4900 0 70   810 680 1 900 9700 9300 0
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c .81 180 9.2  0 5.3  210 57   1 14   510 89 1 11   490 85 1 25   1400 230 1 890    1600 11000   0 15    650 150   1 11     510 130    1 900   3100 13000 0 9.5 550 85 0 .36 12 4.1 0 76   1100 720 1 320   2600 3900 0 70   840 650 1 900 9700 9200 0
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c .81 180 8.1  0 5.3  210 60   1 13   490 94 1 11   500 86 1 61   2500 580 1 890    1600 10000   0 15    650 190   1 12     510 110    1 900   3300 12000 0 10   560 90 0 .34 12 4.0 0 82   1000 800 1 350   2900 4700 0 67   770 790 1 900 9700 9900 0
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c .85 210 9.1  0 6.7  270 67   1 7.6 400 69 0 7.8 370 71 0 34   1600 370 0 340    1000 4600   0 9.5  460 110   0 6.6   340 68    0 13   480 98 0 12   700 95 0 .47 12 6.5 0 64   1600 650 1 540   3900 7800 0 45   630 460 1 900 2100 9300 0
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c .89 210 11    0 6.6  250 76   1 7.5 400 67 0 7.2 360 64 0 22   1000 210 0 440    1000 5400   0 10    470 120   0 7.4   340 81    0 14   480 99 0 12   680 100 0 .50 12 5.5 0 62   1700 580 1 550   4700 9100 0 32   600 280 1 900 2000 9300 0
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c .89 210 11    0 6.6  250 76   1 7.6 410 60 0 7.8 370 65 0 26   1400 220 0 460    1000 5200   0 10    470 140   0 7.2   340 94    0 13   490 95 0 11   680 95 0 .50 12 5.6 0 64   1600 580 1 460   4800 6700 0 31   580 270 1 900 2100 8400 0
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c .87 210 11    0 6.5  260 74   1 7.5 410 63 0 7.6 370 65 0 22   980 190 0 350    1000 3600   0 10    470 110   0 7.2   340 93    0 12   480 98 0 11   670 93 0 .48 12 5.9 0 64   1700 560 1 480   3800 6400 0 32   580 280 1 900 2000 8400 0
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c .92 220 10    0 6.7  260 82   1 9.9 480 81 0 17   620 130 0 43   1300 340 0 890    1200 9100   0 21    780 250   0 16     610 180    0 14   630 110 0 12   690 97 0 .51 13 5.9 0 900   5200 12000 0 900   2900 11000 0 900   4800 10000 0 900 2100 9800 0
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c .91 210 11    0 6.6  260 91   1 8.9 500 76 0 13   520 110 0 81   3700 860 0 890    1700 9100   0 21    790 210   0 16     620 170    0 18   660 140 0 11   670 89 0 .50 12 5.0 0 900   2500 10000 0 900   5500 12000 0 560   4900 6300 1 900 1800 7800 0
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c .89 210 13    0 19    510 220   0 10   470 76 0 34   1000 290 0 110   2700 870 0 890    1500 9100   0 59    1600 720   0 49     1400 660    0 150   3800 1400 0 12   680 110 0 .49 12 5.9 0 900   5300 13000 0 900   4400 15000 0 900   5500 11000 0 900 1900 8000 0
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c .90 210 11    0 6.6  260 100   1 8.6 500 77 0 13   500 100 0 79   3700 790 0 890    1700 7700   0 20    790 250   0 16     620 210    0 19   640 160 0 11   670 94 0 .52 12 5.5 0 900   2400 12000 0 900   5500 11000 0 890   4800 11000 1 900 2100 8700 0
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c .90 210 9.3  0 19    510 250   0 8.8 490 73 0 36   1200 270 0 97   2700 890 0 890    1700 8500   0 59    1600 660   0 48     1400 650    0 78   3400 810 0 11   660 100 0 .55 12 5.5 0 900   5300 11000 0 900   5300 12000 0 900   5200 10000 0 900 2000 7300 0
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c .88 210 8.5  0 6.8  260 75   0 9.6 500 83 0 9.3 470 78 0 30   1500 260 1 700    1300 7000   0 11    480 130   0 15     620 200    0 88   3800 930 0 12   670 96 0 .48 12 5.8 0 98   1800 830 1 900   5000 13000 0 120   4600 1500 1 900 2100 9300 0
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c .90 210 11    0 6.6  260 77   1 9.6 500 72 0 17   650 150 0 44   1400 350 0 890    1300 9400   0 21    780 240   0 15     610 200    0 14   550 110 0 12   760 99 0 .48 12 6.5 0 900   4600 11000 0 900   3400 15000 0 900   4800 11000 0 900 2100 7200 0
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c .93 210 10    0 6.6  260 76   1 8.4 500 72 0 13   510 110 0 91   3700 850 0 840    1600 8600   0 21    790 230   0 15     620 180    0 18   670 130 0 12   680 91 0 .52 12 5.4 0 900   3700 11000 0 900   5500 14000 0 900   5100 9600 0 900 1800 11000 0
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c .92 220 8.8  0 6.7  260 69   1 8.9 490 78 0 17   700 120 0 39   1200 320 0 890    1300 9300   0 21    780 220   0 15     610 160    0 13   580 91 0 12   670 100 0 .48 12 5.4 0 900   4800 11000 0 900   3700 13000 0 900   4800 11000 0 900 2100 7300 0
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c .89 220 10    0 20    510 230   0 9.4 480 71 0 33   1000 280 0 110   2900 1100 0 890    1500 8400   0 61    1600 720   0 48     1400 720    0 900   4100 11000 0 12   670 100 0 .52 12 5.7 0 900   5300 13000 0 900   4800 13000 0 900   5400 11000 0 900 2400 8200 0
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c .90 220 11    0 6.7  260 89   1 9.2 500 69 0 16   650 130 0 42   1100 310 0 890    1300 8800   0 21    780 250   0 16     610 200    0 14   630 120 0 12   680 99 0 .48 13 6.2 0 900   4600 12000 0 900   3900 13000 0 900   4800 11000 0 900 1900 7300 0
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c .79 180 8.7  0 39    650 420   1 14   530 120 -16 36   1200 270 1 170   2800 1800 1 890    1600 12000   0 79    2400 800   1 90     2700 990    1 900   3500 11000 0 10   530 84 0 .33 12 4.3 0 900   4600 9200 0 900   5400 13000 0 400   4700 3900 -16 650 1700 5900 0
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c .78 180 8.3  0 38    600 370   1 15   550 110 -16 50   1800 440 1 220   2800 2300 1 890    1600 9000   0 92    2500 1100   1 110     2800 1600    1 900   3700 13000 0 9.4 560 83 0 .36 12 4.8 0 900   4600 8700 0 900   5400 13000 0 900   5300 10000 0 900 9800 8700 0
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c .76 180 9.5  0 38    600 400   1 15   530 140 -16 41   1400 340 1 130   2800 1400 1 890    1600 11000   0 92    2500 1000   1 110     2800 1400    1 900   3600 13000 0 9.6 550 80 0 .36 12 4.1 0 900   4600 9400 0 900   4700 13000 0 900   5200 12000 0 900 9700 8400 0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c .78 180 7.4  0 38    600 500   1 14   530 110 -16 42   1500 330 1 160   2800 1700 1 890    1600 9500   0 92    2500 1100   1 110     2800 1200    1 900   3400 11000 0 9.7 650 84 0 .35 12 4.0 0 900   4600 11000 0 900   5300 14000 0 500   4800 5600 -16 900 9800 9000 0
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c .89 210 11    0 870    1700 4600   0 8.7 500 64 -16 18   660 130 1 150   4100 1400 1 890    1700 8700   0 900    15000 9700   0 900     15000 9700    0 350   4000 3900 1 11   680 92 0 .49 12 5.6 0 900   5400 11000 0 900   5500 13000 0 900   6300 11000 0 900 2000 8000 0
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c .86 210 11    0 870    1700 5800   0 8.2 430 75 -16 47   1700 420 1 50   2600 500 1 890    1700 12000   0 900    15000 10000   0 900     15000 11000    0 88   3700 860 1 12   680 94 0 .48 12 5.7 0 900   5200 10000 0 900   5500 12000 0 900   5900 12000 0 900 2100 11000 0
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c .94 220 11    0 870    1700 5000   0 17   600 130 -16 45   1400 330 1 290   4400 2800 1 890    1500 9300   0 900    14000 10000   0 900     14000 9300    0 860   4900 11000 1 12   690 94 0 .52 13 6.4 0 900   5500 12000 0 900   5500 13000 0 900   6100 11000 0 900 1800 9000 0
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c .90 210 10    0 870    1700 4900   0 9.5 490 73 -16 29   940 220 1 130   4100 1100 1 890    1600 7500   0 900    15000 11000   0 900     15000 9400    0 110   3500 1000 -16 11   670 99 0 .53 12 6.2 0 900   5900 11000 0 900   5100 12000 0 900   5800 10000 0 900 2000 8800 0
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c .88 210 10    0 870    1700 4200   0 12   510 86 -16 32   920 270 1 140   3900 1300 1 890    1700 9000   0 900    14000 9500   0 900     14000 11000    0 830   4200 10000 1 12   670 100 0 .51 12 5.4 0 900   6400 12000 0 900   5500 12000 0 900   6500 10000 0 900 2100 11000 0
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c .85 210 9.6  0 870    1700 4900   0 9.5 510 81 -16 28   960 230 1 120   4100 1100 1 890    1700 12000   0 900    15000 9900   0 900     14000 9400    0 99   3600 1100 -16 12   680 100 0 .51 12 6.2 0 900   5400 13000 0 900   5500 14000 0 900   6000 12000 0 900 1900 7700 0
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c .91 210 9.8  0 870    1700 4200   0 10   520 77 -16 22   700 160 1 130   2800 1400 1 890    1700 9700   0 900    14000 9100   0 900     15000 10000    0 400   3900 5500 1 12   680 100 0 .50 13 5.8 0 900   6600 13000 0 900   5500 13000 0 900   6300 11000 0 900 1800 8200 0
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c .87 210 8.9  0 870    1700 4100   0 9.5 490 78 -16 35   1100 270 1 110   4000 1100 1 890    1700 11000   0 900    15000 12000   0 900     14000 9100    0 99   3800 1000 -16 12   670 84 0 .50 12 5.5 0 900   5300 10000 0 900   5500 13000 0 900   6100 10000 0 900 2000 9600 0
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c .88 210 11    0 870    1700 4700   0 13   510 110 -16 40   1100 280 1 250   4300 2400 1 890    1600 8400   0 900    14000 8900   0 900     14000 8400    0 480   4800 5600 1 12   670 100 0 .50 12 5.5 0 900   8900 8800 0 900   5500 14000 0 900   6200 11000 0 900 2000 12000 0
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c .85 210 12    0 870    1700 7200   0 9.3 500 74 -16 110   3700 1200 1 110   3900 1100 1 890    1700 8700   0 900    15000 12000   0 900     15000 8100    0 160   3900 1800 1 11   670 84 0 .49 12 6.4 0 900   6500 9800 0 900   5500 15000 0 900   6000 11000 0 900 2100 8600 0
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c .90 220 10    0 870    1700 5000   0 15   580 120 -16 55   1900 560 1 200   4200 1700 1 890    1500 8300   0 900    14000 11000   0 900     14000 11000    0 580   5100 7600 1 12   690 100 0 .48 12 5.7 0 900   6900 11000 0 900   5500 13000 0 900   6500 11000 0 900 1700 9800 0
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c .90 220 10    0 870    1700 4600   0 14   520 110 -16 38   1000 280 1 150   3900 1400 1 890    1700 9500   0 900    15000 11000   0 900     14000 9400    0 900   4100 12000 0 11   670 91 0 .50 12 5.9 0 900   6000 11000 0 900   5500 12000 0 900   6300 13000 0 900 2000 8200 0
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c .93 220 9.6  0 870    1700 4500   0 15   600 110 -16 40   1300 340 1 230   4300 2200 1 890    1500 8100   0 900    14000 9300   0 900     14000 9900    0 830   4900 9700 1 12   680 100 0 .50 13 5.7 0 900   7400 10000 0 900   5500 12000 0 900   6300 8400 0 900 2600 8400 0
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 94 7300 71000 79000 63 94 34000 130000 210000 59 94 5200 87000 57000 -190 94 2400 92000 19000 104 94 5700 140000 58000 108 94 45000 100000 500000 61 94 35000 290000 360000 45 94 23000 240000 250000 70 94 23000 280000 280000 -51 94 3000 69000 24000 22 94 8100   3600 92000 62 94 31000 260000 360000 97 94 57000 370000 780000 44 94 42000 330000 510000 46 94 48000 170000 440000 51
    correct results 40 150 4600 1300 63 45 310 8900 3600 55 49 920 39000 7500 78 52 1200 50000 8900 85 56 1900 44000 21000 84 39 1800 27000 22000 61 32 150 4500 1500 41 44 180 5100 2100 66 42 3300 110000 37000 67 11 46 3000 450 22 41 13   560 160 62 62 4500 110000 43000 95 29 2500 46000 33000 44 54 8000 120000 91000 78 32 3700 16000 41000 47
        correct true 23 52 2200 460 46 10 150 2400 1800 20 29 330 17000 2800 58 33 860 35000 6300 66 28 1200 23000 14000 56 22 1600 26000 19000 44 9 52 920 570 18 22 96 2000 1200 44 25 1800 67000 21000 50 11 46 3000 450 22 21 5.8 250 69 42 33 3200 82000 32000 66 15 570 17000 6700 30 24 4800 75000 56000 48 15 1300 5400 14000 30
        correct false 17 100 2300 810 17 35 160 6600 1900 35 20 590 21000 4700 20 19 340 15000 2700 19 28 700 21000 7200 28 17 220 1700 2900 17 23 94 3500 970 23 22 85 3200 900 22 17 1500 43000 16000 17 0 20 7.3 310 88 20 29 1300 30000 12000 29 14 1900 29000 26000 14 30 3200 41000 35000 30 17 2400 11000 28000 17
    correct-unconfimed results 1 15 230 140 0 11 330 9600 3800 4 4 210 9200 1700 4 42 1200 42000 9800 19 38 3800 98000 37000 24 10 4800 9000 57000 0 21 750 23000 8700 4 21 740 22000 9300 4 29 5700 69000 68000 10 2 12 660 110 0 0 2 58 2500 480 2 0 0 4 380 2600 4200 4
        correct-unconfirmed true 0 4 150 2500 1700 4 4 210 9200 1700 4 19 750 25000 6500 19 24 2900 69000 29000 24 0 4 350 9800 4000 4 4 410 11000 5100 4 10 4700 43000 58000 10 0 0 2 58 2500 480 2 0 0 4 380 2600 4200 4
        correct-unconfirmed false 1 15 230 140 0 7 170 7100 2100 0 0 23 420 16000 3300 0 14 840 29000 7700 0 10 4800 9000 57000 0 17 400 14000 4600 0 17 330 11000 4200 0 19 980 25000 10000 0 2 12 660 110 0 0 0 0 0 0
    incorrect results 0 0 17 210 8900 1700 -272 0 0 0 0 0 8 440 16000 4100 -128 0 0 0 0 2 900 9500 9500 -32 0
        incorrect true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 17 210 8900 1700 -272 0 0 0 0 0 8 440 16000 4100 -128 0 0 0 0 2 900 9500 9500 -32 0
score (94 tasks, max score: 146) 63 59 -190 104 108 61 45 70 -51 22 62 97 44 46 51
Run set 2ls.sv-comp18.ReachSafety-ControlFlow cbmc.sv-comp18.ReachSafety-ControlFlow cpa-bam-bnb.sv-comp18.ReachSafety-ControlFlow cpa-bam-slicing.sv-comp18.ReachSafety-ControlFlow cpa-seq.sv-comp18.ReachSafety-ControlFlow depthk.sv-comp18.ReachSafety-ControlFlow esbmc-incr.sv-comp18.ReachSafety-ControlFlow esbmc-kind.sv-comp18.ReachSafety-ControlFlow interpchecker.sv-comp18.ReachSafety-ControlFlow skink.sv-comp18.ReachSafety-ControlFlow symbiotic.sv-comp18.ReachSafety-ControlFlow uautomizer.sv-comp18.ReachSafety-ControlFlow ukojak.sv-comp18.ReachSafety-ControlFlow utaipan.sv-comp18.ReachSafety-ControlFlow veriabs.sv-comp18.ReachSafety-ControlFlow