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-05 07:52:24 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 false(unreach-call) 1.3  380 19    1 false(unreach-call) 1.4  160 15   1 false(unreach-call) 12   480 87 1 false(unreach-call) 9.2 450 85 1 false(unreach-call) 8.8 340 77 1 false(unreach-call) 3.3  88 46   1 false(unreach-call) 1.0  47 12   1 false(unreach-call) .98  47 12    1 false(unreach-call) 26   990 200 1 unknown 88   1600 590 0 false(unreach-call) .39 16 4.7 1 false(unreach-call) 54   1300 430 1 timeout 900   5400 13000 0 false(unreach-call) 58   1300 440 1 error 200 830 2100 0
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) .38 65 3.2  1 false(unreach-call) .48 41 5.5 1 false(unreach-call) 35   1600 270 1 false(unreach-call) 15   650 120 0 false(unreach-call) 6.9 300 53 1 false(unreach-call) 1.6  94 23   1 false(unreach-call) .76 33 7.8 1 false(unreach-call) .76  33 6.9  1 false(unreach-call) 43   2000 340 1 unknown 52   960 530 0 false(unreach-call) .26 13 3.7 1 false(unreach-call) 33   940 260 1 timeout 900   5100 11000 0 false(unreach-call) 33   950 270 1 false(unreach-call) 270 370 3400 1
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) .54 130 6.2  1 false(unreach-call) .76 60 10   1 witness invalid (false(unreach-call)) 38   1800 320 0 false(unreach-call) 17   690 140 0 false(unreach-call) 8.1 330 65 1 false(unreach-call) 2.6  100 32   1 false(unreach-call) 1.0  36 9.6 1 false(unreach-call) 1.0   36 9.0  1 false(unreach-call) 45   1900 380 1 unknown 50   1100 430 0 false(unreach-call) .38 14 4.5 1 false(unreach-call) 48   1200 400 1 false(unreach-call) 630   4300 9800 1 false(unreach-call) 50   1300 430 1 false(unreach-call) 270 390 2900 1
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) .28 41 2.2  1 false(unreach-call) .39 38 4.5 1 witness invalid (false(unreach-call)) 13   510 86 0 false(unreach-call) 8.5 450 73 1 false(unreach-call) 5.8 300 47 1 false(unreach-call) 1.2  63 15   1 false(unreach-call) .49 32 4.3 1 false(unreach-call) .53  32 4.3  1 false(unreach-call) 16   640 120 1 unknown 28   930 260 0 false(unreach-call) .24 13 2.9 1 false(unreach-call) 16   660 120 1 false(unreach-call) 45   1000 460 1 false(unreach-call) 16   640 130 1 false(unreach-call) 260 340 3000 1
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.4  410 15    2 true 2.9  160 31   2 true 42   2000 350 2 true 22   950 180 2 true 8.3 330 62 2 true 18    350 190   2 true .64 45 8.6 2 true .64  45 7.2  2 false(unreach-call) 26   810 210 -16 unknown 94   1500 570 0 true .42 16 5.7 2 true 100   2400 980 2 timeout 900   5500 12000 0 timeout 900   3900 12000 0 error 200 840 1400 0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .53 110 5.0  2 error (42) 870    4500 3700   0 true 53   3000 510 2 true 17   710 130 2 true 100   1300 1300 2 unknown 140    100 1700   0 timeout 900    990 9400   0 true .32  31 3.7  2 false(unreach-call) 10   480 90 -16 unknown 53   1200 410 0 true .35 13 3.7 2 true 66   1700 570 2 timeout 900   4000 12000 0 true 600   4600 6800 2 unknown 890 670 8500 0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .36 71 4.7  2 true .84 42 8.7 2 true 27   1500 220 1 true 14   650 120 2 true 7.4 310 70 2 true 10    350 89   2 true .23 31 2.9 2 true .22  31 2.9  2 true 86   3800 1100 2 unknown 51   970 500 0 true .29 13 3.0 2 true 69   1800 650 2 timeout 900   5300 12000 0 timeout 900   4600 12000 0 true 280 510 2700 2
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .58 140 5.9  2 true 1.4  60 15   2 true 36   1900 280 1 true 15   670 120 1 true 8.0 330 66 2 true 13    370 120   2 true .38 34 4.8 2 true .36  34 4.6  2 true 200   4000 2300 2 unknown 49   1100 410 0 true .38 14 5.6 2 true 71   1800 730 2 timeout 900   3900 12000 0 timeout 900   4600 12000 0 true 280 610 2900 2
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .18 27 1.6  2 true .52 35 5.2 2 true 7.0 380 64 2 true 6.0 320 45 2 true 4.9 280 40 2 true 5.3  270 47   2 true .13 28 1.5 2 true .12  29 1.2  2 true 11   500 95 2 unknown 29   800 300 0 true .19 11 2.4 2 true 17   750 150 2 true 32   840 310 2 true 16   720 140 2 true 260 350 2500 2
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .27 47 2.6  2 true .63 36 9.3 2 true 8.8 470 63 2 true 6.7 400 52 2 true 6.3 290 49 2 true 7.1  290 75   2 true .19 30 1.7 2 true .15  30 1.7  2 true 15   620 120 2 unknown 27   820 230 0 true .27 12 2.4 2 true 17   660 130 2 true 41   990 390 2 true 17   620 130 2 true 270 450 3700 2
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 9.6  170 69    1 false(unreach-call) 2.0  87 24   1 false(unreach-call) 15   530 110 1 false(unreach-call) 9.7 470 77 1 false(unreach-call) 6.4 300 47 1 false(unreach-call) 20    92 320   1 false(unreach-call) 2.8  64 27   1 false(unreach-call) 2.1   56 27    1 false(unreach-call) 42   1600 350 1 unknown 67   750 720 0 false(unreach-call) .29 12 3.1 1 false(unreach-call) 10   550 80 1 false(unreach-call) 350   4800 5500 1 false(unreach-call) 10   570 83 1 false(unreach-call) 58 440 670 1
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 10    180 91    1 false(unreach-call) 2.1  87 23   1 false(unreach-call) 14   520 110 1 false(unreach-call) 8.6 460 66 1 false(unreach-call) 6.7 300 52 1 false(unreach-call) 20    85 260   1 false(unreach-call) 2.8  65 25   1 false(unreach-call) 2.3   56 24    1 false(unreach-call) 110   4200 1300 1 unknown 44   720 440 0 false(unreach-call) .28 12 3.4 1 false(unreach-call) 11   560 87 1 false(unreach-call) 210   4300 2400 1 false(unreach-call) 10   550 73 1 false(unreach-call) 61 450 610 1
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 15    230 140    0 false(unreach-call) 2.4  100 30   1 false(unreach-call) 15   550 120 1 false(unreach-call) 9.6 490 79 1 false(unreach-call) 6.1 300 46 1 false(unreach-call) 24    95 390   0 false(unreach-call) 3.6  75 40   1 false(unreach-call) 2.8   65 27    1 false(unreach-call) 110   4200 1100 1 unknown 53   720 560 0 false(unreach-call) .32 12 3.5 1 false(unreach-call) 15   660 120 1 false(unreach-call) 250   4100 3000 1 false(unreach-call) 15   650 120 1 false(unreach-call) 62 490 650 1
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 9.1  180 80    1 false(unreach-call) 2.1  87 24   1 false(unreach-call) 13   530 93 1 false(unreach-call) 9.2 460 70 1 false(unreach-call) 6.3 300 49 1 false(unreach-call) 21    85 290   1 false(unreach-call) 3.0  65 33   1 false(unreach-call) 2.4   57 25    1 false(unreach-call) 110   4200 1200 1 unknown 72   750 750 0 false(unreach-call) .28 12 3.9 1 false(unreach-call) 11   560 93 1 false(unreach-call) 200   4200 2400 1 false(unreach-call) 14   610 120 1 false(unreach-call) 60 450 630 1
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) .30 42 2.9  1 false(unreach-call) .31 35 3.0 1 false(unreach-call) 45   1900 330 1 false(unreach-call) 48   2100 380 1 false(unreach-call) 3.8 280 35 1 false(unreach-call) 4.0  87 49   1 false(unreach-call) .35 31 2.9 1 false(unreach-call) .63  31 6.8  1 false(unreach-call) 240   4500 2600 1 unknown 110   820 1400 0 false(unreach-call) .26 12 2.6 1 false(unreach-call) 9.3 480 83 1 false(unreach-call) 7.8 400 61 1 false(unreach-call) 9.3 470 73 1 false(unreach-call) 92 720 1100 1
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 14    230 110    1 false(unreach-call) 14    330 170   1 false(unreach-call) 18   600 140 1 false(unreach-call) 48   2200 350 0 false(unreach-call) 100   800 1400 1 false(unreach-call) 24    88 330   1 false(unreach-call) 3.8  71 38   1 false(unreach-call) 4.8   86 61    1 false(unreach-call) 210   3800 2500 1 unknown 9.9 500 93 0 false(unreach-call) .39 14 5.4 1 false(unreach-call) 23   780 180 1 timeout 900   6400 12000 0 false(unreach-call) 39   4300 370 1 false(unreach-call) 360 910 4300 1
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 16    230 120    1 false(unreach-call) 3.5  150 41   1 false(unreach-call) 240   6600 2000 1 false(unreach-call) 70   2900 520 1 false(unreach-call) 160   860 1800 1 false(unreach-call) 42    98 620   1 false(unreach-call) 4.1  75 40   1 false(unreach-call) 3.6   66 36    1 false(unreach-call) 400   4700 5100 0 unknown 11   640 90 0 false(unreach-call) 1.1  23 14   1 false(unreach-call) 23   820 180 1 timeout 900   6100 12000 0 false(unreach-call) 710   4900 8400 1 false(unreach-call) 240 1000 3500 1
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 13    170 96    1 false(unreach-call) 3.3  140 37   1 timeout 900   4600 9500 0 false(unreach-call) 28   990 180 1 false(unreach-call) 5.4 290 44 1 false(unreach-call) 16    94 200   1 false(unreach-call) 2.5  51 22   1 false(unreach-call) 2.4   44 19    1 false(unreach-call) 73   3700 730 1 unknown 150   1100 1800 0 false(unreach-call) .31 13 3.5 1 false(unreach-call) 20   730 160 1 timeout 900   6300 12000 0 false(unreach-call) 21   720 170 1 false(unreach-call) 120 920 1300 1
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 4.9  89 37    1 false(unreach-call) .32 35 3.1 1 false(unreach-call) 74   3400 600 1 false(unreach-call) 66   3100 520 1 false(unreach-call) 8.8 380 70 1 false(unreach-call) 14    90 170   1 false(unreach-call) 1.3  34 15   1 false(unreach-call) 1.2   31 15    1 false(unreach-call) 310   5200 3600 1 unknown 15   650 130 0 false(unreach-call) .23 12 3.4 1 false(unreach-call) 16   640 120 1 false(unreach-call) 23   720 190 1 false(unreach-call) 16   640 130 1 false(unreach-call) 120 900 1200 1
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 13    170 100    1 false(unreach-call) 3.1  140 38   1 false(unreach-call) 8.5 410 70 1 false(unreach-call) 6.6 310 53 1 false(unreach-call) 5.9 290 45 1 false(unreach-call) 21    320 280   1 false(unreach-call) 1.9  50 14   1 false(unreach-call) 1.7   44 16    1 false(unreach-call) 27   1300 240 1 unknown 14   640 120 0 false(unreach-call) .28 12 3.0 1 false(unreach-call) 14   620 110 1 false(unreach-call) 77   2000 880 1 false(unreach-call) 15   630 130 1 false(unreach-call) 110 840 1300 1
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 8.9  150 77    1 false(unreach-call) 3.0  130 35   1 false(unreach-call) 7.7 420 60 1 false(unreach-call) 6.8 320 59 1 false(unreach-call) 5.5 290 45 1 false(unreach-call) 10    89 120   1 false(unreach-call) 2.1  49 21   1 false(unreach-call) 1.7   42 19    1 false(unreach-call) 25   1300 200 1 unknown 15   660 110 0 false(unreach-call) .29 12 3.1 1 false(unreach-call) 16   660 130 1 false(unreach-call) 69   1600 700 1 false(unreach-call) 16   660 130 1 false(unreach-call) 110 830 1400 1
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) .28 43 2.8  1 false(unreach-call) .32 37 2.8 1 false(unreach-call) 4.4 300 38 1 false(unreach-call) 4.6 290 42 1 false(unreach-call) 3.3 260 29 1 false(unreach-call) 14    92 180   1 false(unreach-call) .33 31 3.5 1 false(unreach-call) 1.1   31 11    1 false(unreach-call) 71   3800 710 1 unknown 14   660 120 0 false(unreach-call) .25 12 2.6 1 false(unreach-call) 6.5 330 53 1 false(unreach-call) 7.1 390 51 1 false(unreach-call) 6.2 320 50 1 false(unreach-call) 120 940 1300 1
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 9.0  250 82    2 true 25    380 270   2 true 22   1000 170 2 true 31   1200 250 2 true 13   710 120 2 true 150    1300 1800   2 true 12    180 130   2 true 14     190 160    2 true 54   3300 530 2 unknown 67   730 760 0 true .60 13 7.2 2 true 29   1300 250 2 timeout 900   6400 12000 0 true 440   5300 5300 2 true 95 640 1000 1
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 11    250 95    2 true 26    390 260   2 true 10   480 88 2 true 29   1200 200 2 true 13   720 120 2 true 150    1300 1900   2 true 12    180 130   2 true 14     200 210    2 true 39   2600 370 2 unknown 46   720 520 0 true .60 13 7.1 2 true 35   1500 290 2 timeout 900   6100 12000 0 true 500   5400 6500 2 true 94 660 950 1
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 16    320 140    2 true 30    460 420   2 true 9.9 470 84 2 true 28   1200 210 2 true 14   730 140 2 true 180    1300 2000   2 true 14    210 150   2 true 17     240 180    2 true 44   2600 310 2 unknown 47   720 490 0 true .61 13 7.3 2 true 34   1400 240 2 timeout 900   6200 12000 0 true 550   5500 6500 2 true 100 700 1100 1
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 9.9  260 86    2 true 26    390 300   2 true 9.7 480 76 2 true 33   1300 230 2 true 13   720 120 2 true 160    1300 2300   2 true 12    180 140   2 true 15     200 170    2 true 39   2600 360 2 unknown 33   700 370 0 true .59 13 8.1 2 true 31   1300 250 2 timeout 900   6300 13000 0 true 440   5400 5700 2 true 96 640 1200 1
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 900    8200 12000    0 error (42) 870    1100 4900   0 true 14   510 98 2 true 49   2300 360 2 true 14   730 140 1 unknown 890    470 10000   0 timeout 900    2400 8000   0 timeout 900     2400 11000    0 true 41   2600 410 2 unknown 14   650 110 0 timeout (timeout) 900    640 10000   0 true 24   1200 190 1 timeout 900   6400 12000 0 timeout 900   5400 12000 0 timeout 900 1400 5100 0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true .61 39 9.0  2 error (42) 870    1100 3600   0 true 4.4 310 40 2 true 4.0 280 36 2 true 3.1 250 26 2 unknown 370    110 4800   0 timeout 900    1900 9700   0 timeout 900     1900 10000    0 true 9.9 450 84 2 unknown 31   690 310 0 timeout (timeout) 900    81 10000   0 true 7.4 370 59 2 true 53   1500 660 2 true 7.5 370 56 2 timeout 900 2800 5400 0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .39 29 4.8  2 error (42) 870    2700 5100   0 true 3.5 280 34 2 true 3.3 270 29 2 true 2.6 250 24 2 unknown 120    77 1600   0 timeout 900    2300 8900   0 timeout 900     2300 8300    0 true 5.2 300 45 2 unknown 96   720 1000 0 timeout (timeout) 900    58 11000   0 true 6.0 300 54 2 true 15   590 130 2 true 5.7 290 52 2 unknown 860 1800 4500 0
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 900    7800 10000    0 error (42) 870    1200 5400   0 true 9.1 460 74 2 true 25   1000 190 2 true 14   730 120 1 true 44    2300 470   2 timeout 900    2300 10000   0 timeout 900     2300 8200    0 true 120   3500 1300 2 unknown 15   650 130 0 timeout (timeout) 900    220 9800   0 true 56   2200 500 2 timeout 900   6300 12000 0 timeout 900   5400 11000 0 timeout 900 1500 5400 0
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 900    7800 9700    0 error (42) 870    1200 4300   0 true 12   530 97 2 true 45   1800 330 2 true 14   730 140 1 unknown 890    460 10000   0 timeout 900    2300 9100   0 timeout 900     2300 8600    0 true 67   3200 740 2 unknown 16   640 140 0 timeout (timeout) 900    220 10000   0 true 52   2100 480 2 timeout 900   6500 12000 0 true 500   4700 5900 2 timeout 900 1500 5300 0
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 900    7800 10000    0 error (42) 870    1200 5200   0 true 9.0 470 79 2 true 21   1000 160 2 true 14   730 150 1 unknown 890    460 14000   0 timeout 900    2300 8100   0 timeout 900     2300 9400    0 true 82   3400 950 2 unknown 16   640 150 0 timeout (timeout) 900    220 10000   0 true 49   2200 430 2 timeout 900   6300 11000 0 true 200   4900 2400 2 timeout 900 1500 5600 0
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 900    7800 10000    0 error (42) 870    1200 4700   0 true 18   690 160 2 true 250   7400 1500 2 true 81   2300 1100 1 unknown 890    450 13000   0 timeout 900    2300 9800   0 timeout 900     2200 7700    0 true 67   3800 650 2 unknown 20   670 160 0 timeout (timeout) 900    220 10000   0 true 34   1300 290 1 timeout 900   6300 12000 0 timeout 900   5400 10000 0 timeout 900 1700 7200 0
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 900    7900 12000    0 error (42) 870    1200 6400   0 true 13   540 110 2 true 41   1700 300 2 true 46   1300 460 1 unknown 890    470 11000   0 timeout 900    2400 11000   0 timeout 900     2400 8100    0 true 92   3900 1100 2 unknown 18   660 180 0 timeout (timeout) 900    220 10000   0 true 71   2600 650 2 timeout 900   6400 14000 0 true 240   4900 3300 2 timeout 900 1600 5200 0
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 900    7800 9400    0 error (42) 870    1200 4700   0 true 14   490 110 2 true 69   2900 470 2 true 14   740 140 1 true 49    2300 590   2 timeout 900    2300 8800   0 timeout 900     2200 8000    0 true 45   2400 380 2 unknown 16   700 130 0 timeout (timeout) 900    220 9600   0 true 55   2300 580 2 timeout 900   6200 12000 0 timeout 900   5400 12000 0 timeout 900 1600 5600 0
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) .14 26 1.3  1 false(unreach-call) .31 33 3.0 1 false(unreach-call) 4.8 300 44 1 false(unreach-call) 4.5 300 39 1 false(unreach-call) 3.3 270 32 1 false(unreach-call) .48 79 6.1 1 false(unreach-call) .79 29 6.0 1 false(unreach-call) .76  29 6.6  1 false(unreach-call) 3.2 280 28 1 false(unreach-call) 6.0 330 58 0 false(unreach-call) .18 11 1.9 1 false(unreach-call) 5.8 280 50 1 false(unreach-call) 5.8 320 46 1 false(unreach-call) 6.3 280 49 1 false(unreach-call) 27 290 230 1
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) .15 28 1.2  1 false(unreach-call) .33 36 3.5 1 false(unreach-call) 4.8 300 46 1 false(unreach-call) 4.3 300 31 1 false(unreach-call) 3.8 270 34 1 false(unreach-call) .50 79 6.5 1 false(unreach-call) .82 29 6.2 1 false(unreach-call) .86  29 7.0  1 false(unreach-call) 3.1 270 30 1 false(unreach-call) 5.7 320 53 0 false(unreach-call) .16 11 1.9 1 false(unreach-call) 6.0 290 50 1 false(unreach-call) 5.4 290 44 1 false(unreach-call) 6.1 290 49 1 false(unreach-call) 29 280 270 1
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true .14 24 1.1  2 error (42) 870    3300 6400   0 true 3.3 280 32 2 true 3.2 280 31 2 true 15   740 120 2 true 30    1300 300   2 timeout 900    2100 8000   0 true .099 27 1.1  2 true 120   4700 1300 2 true 4.1 260 42 2 true .16 11 1.5 2 true 18   850 150 2 true 31   890 390 2 true 20   850 150 2 true 18 310 170 2
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true .14 27 .98 2 error (42) 870    4000 5600   0 true 3.5 280 29 2 true 3.3 270 34 2 true 44   1200 470 2 true 89    2200 1200   2 timeout 900    2300 8200   0 true .11  27 1.1  2 true 310   6800 3600 2 true 4.3 270 43 2 true .13 11 1.5 2 true 25   1600 200 2 true 39   1100 500 2 true 26   1400 180 2 true 19 320 150 2
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true .15 27 1.0  2 error (42) 870    4800 7300   0 true 3.4 280 33 2 true 3.3 270 27 2 true 150   1300 1900 2 true 160    2300 2000   2 timeout 900    2300 7100   0 true .12  27 1.4  2 timeout (true) 920   13000 10000 0 true 4.4 270 41 2 true .14 11 1.5 2 true 38   2600 330 2 true 48   1800 560 2 true 37   3000 320 2 true 20 310 170 2
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true .14 26 1.0  2 error (42) 870    5500 6300   0 true 3.3 280 32 2 true 3.3 270 31 2 true 150   1200 1800 2 true 160    2300 1900   2 timeout 900    2400 7800   0 true .12  27 1.4  2 timeout 910   11000 12000 0 true 4.2 270 44 2 true .13 11 1.5 2 true 65   4900 560 2 true 60   1500 720 2 true 51   4600 450 2 true 21 340 180 2
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true .15 26 1.2  2 error (42) 870    6200 5700   0 true 3.4 270 30 2 true 3.4 270 34 2 true 150   1200 1900 2 true 160    2200 1800   2 timeout 900    2500 8400   0 true .14  27 1.4  2 timeout 910   10000 11000 0 true 4.3 280 35 2 true .13 11 1.8 2 true 120   6500 1000 2 true 77   1600 910 2 true 130   6100 1000 2 true 21 300 200 2
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true .15 26 1.1  2 error (42) 870    6900 6300   0 true 3.4 270 32 2 true 3.3 270 31 2 true 150   1200 1700 2 true 160    2200 2100   2 timeout 900    2500 7400   0 true .14  27 1.3  2 timeout 910   10000 9900 0 true 4.4 290 43 2 true .14 11 1.5 2 true 290   8700 2100 2 true 95   2800 1300 2 true 290   8800 2000 2 true 24 370 220 2
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true .13 23 .82 2 error (42) 870    5900 7800   0 true 2.9 280 27 2 true 3.0 270 26 2 true 3.1 250 26 2 true 4.3  260 44   2 timeout 900    1700 8100   0 true .12  27 .70 2 true 10   460 67 2 true 4.3 260 40 2 true .13 11 1.6 2 true 6.6 320 49 2 true 8.8 500 82 2 true 9.1 390 81 2 true 14 290 120 2
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true .14 23 .86 2 error (42) 870    7900 6300   0 true 3.0 270 31 2 true 3.0 270 26 2 true 3.5 260 27 2 true 4.9  270 50   2 timeout 900    1800 8000   0 true .10  27 1.0  2 true 13   620 93 2 true 4.2 310 44 2 true .13 11 1.5 2 true 7.4 380 67 2 true 12   580 100 2 true 7.3 380 62 2 true 15 320 120 2
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true .12 24 .95 2 error (42) 870    1900 5600   0 true 3.0 280 29 2 true 3.0 270 28 2 true 4.3 270 35 2 true 6.3  300 62   2 timeout 900    1900 7500   0 true .11  27 1.1  2 true 23   1300 150 2 true 4.0 260 41 2 true .16 11 1.4 2 true 8.6 510 66 2 true 18   680 180 2 true 9.2 520 69 2 true 15 300 120 2
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true .12 24 .82 2 error (42) 870    2300 5600   0 true 3.1 280 31 2 true 3.2 280 32 2 true 6.0 290 47 2 true 9.5  450 80   2 timeout 900    2000 7700   0 true .12  27 1.1  2 true 32   2400 310 2 true 4.1 260 38 2 true .14 11 1.4 2 true 11   570 97 2 true 20   760 170 2 true 11   590 86 2 true 17 320 160 2
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true .11 24 1.0  2 error (42) 870    2800 5100   0 true 3.2 270 29 2 true 3.3 280 30 2 true 8.4 430 68 2 true 14    720 140   2 timeout 900    2100 7200   0 true .13  27 .84 2 true 53   4000 540 2 true 4.0 260 36 2 true .13 11 1.7 2 true 14   730 120 2 true 25   860 290 2 true 14   670 120 2 true 17 290 130 2
ntdrivers/cdaudio_false-unreach-call.i.cil.c error (6) .56 63 4.3  0 false(unreach-call) 100    5100 1300   0 timeout 900   4300 12000 0 false(unreach-call) 21   730 150 0 false(unreach-call) 54   1800 580 1 unknown 890    350 11000   0 timeout 900    5800 14000   0 unknown 1.5   290 18    0 timeout 900   4800 11000 0 unknown 69   1700 380 0 false(unreach-call) 1.0  36 12   1 timeout 900   3100 9800 0 timeout 900   4900 13000 0 timeout 900   5300 12000 0 unknown 74 360 570 0
ntdrivers/diskperf_false-unreach-call.i.cil.c error (134) .60 44 5.3  0 false(unreach-call) 1.7  120 17   1 false(unreach-call) 22   890 150 1 false(unreach-call) 13   510 110 0 false(unreach-call) 15   510 150 1 false(unreach-call) 480    170 6900   0 false(unreach-call) 1.1  87 12   1 false(unreach-call) 1.0   88 12    0 false(unreach-call) 34   1200 280 0 unknown 59   1400 290 0 unknown .59 29 8.0 0 false(unreach-call) 16   720 130 1 false(unreach-call) 60   840 610 1 false(unreach-call) 20   750 160 1 unknown 55 320 430 0
ntdrivers/floppy_false-unreach-call.i.cil.c error (134) 2.2  59 19    0 false(unreach-call) 3.5  170 38   0 witness invalid (false(unreach-call)) 32   1300 220 0 false(unreach-call) 24   940 180 0 false(unreach-call) 11   470 100 1 false(unreach-call) 590    830 7000   0 false(unreach-call) 13    460 170   0 timeout 900     1100 11000    0 false(unreach-call) 24   760 180 0 unknown 32   1100 170 0 unknown .92 43 11   0 false(unreach-call) 82   3700 790 1 timeout 900   1500 8000 0 timeout 900   6300 11000 0 unknown 80 360 640 0
ntdrivers/kbfiltr_false-unreach-call.i.cil.c error (134) .41 36 3.7  0 false(unreach-call) 1.5  73 15   0 false(unreach-call) 16   700 120 1 false(unreach-call) 12   480 90 0 false(unreach-call) 12   460 110 1 unknown 890    540 9700   0 unknown .65 72 8.7 0 unknown .63  73 9.1  0 false(unreach-call) 28   1000 200 0 unknown 20   760 120 0 false(unreach-call) .50 32 5.0 1 timeout 900   2200 6600 0 timeout 900   4400 11000 0 timeout 900   4700 10000 0 unknown 37 280 290 0
ntdrivers/parport_false-unreach-call.i.cil.c error (5) 3.0  100 25    0 false(unreach-call) 14    790 150   1 witness invalid (false(unreach-call)) 35   1400 280 0 false(unreach-call) 23   970 170 0 false(unreach-call) 11   470 96 1 false(unreach-call) 590    960 7900   0 false(unreach-call) 7.3  350 87   0 false(unreach-call) 28     490 310    0 false(unreach-call) 10   470 80 0 unknown 340   1700 1700 0 unknown 1.7  120 18   0 unknown 100   1300 790 0 timeout 900   1300 10000 0 unknown 150   1400 1400 0 unknown 520 2500 5000 0
ntdrivers/cdaudio_true-unreach-call.i.cil.c error (6) .53 64 6.1  0 true 39    410 470   2 timeout 900   4200 12000 0 true 48   1900 360 2 true 12   480 110 2 unknown 900    350 11000   0 unknown .77 280 8.4 0 unknown .87  280 10    0 false(unreach-call) 33   1200 260 -16 unknown 53   1500 260 0 unknown .97 35 13   0 true 150   3300 1700 2 timeout 900   4400 13000 0 timeout 900   4800 10000 0 unknown 78 370 610 0
ntdrivers/diskperf_true-unreach-call.i.cil.c error (134) .60 46 6.1  0 error (42) 880    7500 5000   0 true 30   1500 260 2 true 16   700 120 2 true 99   1900 1300 2 unknown 640    170 8400   0 unknown .51 83 6.7 0 unknown .31  82 4.4  0 false(unreach-call) 40   1500 330 -16 unknown 83   1700 390 0 unknown .80 40 8.4 0 true 160   4700 1600 2 timeout 900   4900 10000 0 timeout 900   6300 13000 0 unknown 740 2300 6400 0
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c error (5) 820    2800 4200    0 error (42) 870    7500 7100   0 timeout 900   4300 11000 0 true 34   1400 280 1 true 81   2000 780 2 unknown 890    14000 13000   0 timeout 900    7200 8300   0 timeout 900     430 11000    0 true 150   3900 1700 1 unknown 5.0 350 50 0 unknown 2.2  57 30   0 true 600   7500 6500 2 timeout 900   2100 8900 0 timeout 900   6100 9500 0 unknown 150 1300 1300 0
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c error (134) 2.3  61 20    0 error (42) 870    4400 5800   0 true 38   1500 290 1 true 35   1400 280 2 true 39   920 360 2 unknown 890    1300 8700   0 timeout 900    8000 8200   0 timeout 900     1000 11000    0 true 300   4100 3500 2 unknown 32   1200 180 0 unknown .90 43 12   0 true 600   6900 6500 2 timeout 900   1700 9200 0 timeout 900   6300 12000 0 unknown 79 390 670 0
ntdrivers/parport_true-unreach-call.i.cil.c error (5) 3.1  100 32    0 error (42) 880    5200 5700   0 true 110   4400 940 1 true 39   1400 330 2 true 120   2700 1200 2 unknown 890    2000 11000   0 timeout 900    5700 9300   0 true 33     660 420    2 false(unreach-call) 17   610 140 -16 unknown 340   1700 1500 0 unknown 1.6  120 19   0 true 320   4900 3800 2 timeout 900   4700 13000 0 true 710   4800 8200 2 unknown 530 2500 3800 0
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error (134) .78 180 8.0  0 false(unreach-call) 15    470 170   1 witness invalid (false(unreach-call)) 14   530 100 0 false(unreach-call) 13   530 110 1 false(unreach-call) 61   2500 580 1 unknown 890    1600 8200   0 false(unreach-call) 14    650 150   1 false(unreach-call) 19     790 190    1 timeout 900   2600 13000 0 unknown 9.6 540 85 0 unknown .36 12 3.5 0 false(unreach-call) 240   1600 2600 1 error (7) 390   3400 4900 0 false(unreach-call) 180   990 1800 1 unknown 720 1600 6000 0
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error (134) .80 180 9.0  0 false(unreach-call) 5.4  210 58   1 false(unreach-call) 13   490 110 1 false(unreach-call) 10   500 94 1 false(unreach-call) 63   3300 600 1 unknown 890    1600 8500   0 false(unreach-call) 15    650 140   1 false(unreach-call) 11     510 140    1 timeout 900   3600 12000 0 unknown 9.8 540 87 0 unknown .33 12 4.4 0 false(unreach-call) 82   1200 690 1 error (7) 410   3500 4900 0 false(unreach-call) 70   810 680 1 timeout 900 9700 9300 0
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error (134) .81 180 9.2  0 false(unreach-call) 5.3  210 57   1 false(unreach-call) 14   510 89 1 false(unreach-call) 11   490 85 1 false(unreach-call) 25   1400 230 1 unknown 890    1600 11000   0 false(unreach-call) 15    650 150   1 false(unreach-call) 11     510 130    1 timeout 900   3400 13000 0 unknown 9.5 550 85 0 unknown .36 12 4.1 0 false(unreach-call) 76   1100 720 1 error (7) 320   2600 3900 0 false(unreach-call) 70   840 650 1 timeout 900 9700 9200 0
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error (134) .81 180 8.1  0 false(unreach-call) 5.3  210 60   1 false(unreach-call) 13   490 94 1 false(unreach-call) 11   500 86 1 false(unreach-call) 61   2500 580 1 unknown 890    1600 10000   0 false(unreach-call) 15    650 190   1 false(unreach-call) 12     510 110    1 timeout 900   2500 11000 0 unknown 10   560 90 0 unknown .34 12 4.0 0 false(unreach-call) 82   1000 800 1 error (7) 350   2900 4700 0 false(unreach-call) 67   770 790 1 timeout 900 9700 9900 0
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error (134) .85 210 9.1  0 false(unreach-call) 6.7  270 67   1 witness invalid (false(unreach-call)) 7.6 400 69 0 false(unreach-call) 7.8 370 71 0 false(unreach-call) 34   1600 370 0 false(unreach-call) 340    1000 4600   0 false(unreach-call) 9.5  460 110   0 false(unreach-call) 6.6   340 68    0 false(unreach-call) 12   550 100 0 unknown 12   700 95 0 unknown .47 12 6.5 0 false(unreach-call) 64   1600 650 1 error (7) 540   3900 7800 0 false(unreach-call) 45   630 460 1 timeout 900 2100 9300 0
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error (134) .89 210 11    0 false(unreach-call) 6.6  250 76   1 witness invalid (false(unreach-call)) 7.5 400 67 0 false(unreach-call) 7.2 360 64 0 false(unreach-call) 22   1000 210 0 false(unreach-call) 440    1000 5400   0 false(unreach-call) 10    470 120   0 false(unreach-call) 7.4   340 81    0 false(unreach-call) 12   470 100 0 unknown 12   680 100 0 unknown .50 12 5.5 0 false(unreach-call) 62   1700 580 1 error (7) 550   4700 9100 0 false(unreach-call) 32   600 280 1 timeout 900 2000 9300 0
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error (134) .89 210 11    0 false(unreach-call) 6.6  250 76   1 witness invalid (false(unreach-call)) 7.6 410 60 0 false(unreach-call) 7.8 370 65 0 false(unreach-call) 26   1400 220 0 false(unreach-call) 460    1000 5200   0 false(unreach-call) 10    470 140   0 false(unreach-call) 7.2   340 94    0 false(unreach-call) 11   470 100 0 unknown 11   680 95 0 unknown .50 12 5.6 0 false(unreach-call) 64   1600 580 1 error (7) 460   4800 6700 0 false(unreach-call) 31   580 270 1 timeout 900 2100 8400 0
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error (134) .87 210 11    0 false(unreach-call) 6.5  260 74   1 witness invalid (false(unreach-call)) 7.5 410 63 0 false(unreach-call) 7.6 370 65 0 false(unreach-call) 22   980 190 0 false(unreach-call) 350    1000 3600   0 false(unreach-call) 10    470 110   0 false(unreach-call) 7.2   340 93    0 false(unreach-call) 11   480 83 0 unknown 11   670 93 0 unknown .48 12 5.9 0 false(unreach-call) 64   1700 560 1 error (7) 480   3800 6400 0 false(unreach-call) 32   580 280 1 timeout 900 2000 8400 0
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c error (134) .92 220 10    0 false(unreach-call) 6.7  260 82   1 witness invalid (false(unreach-call)) 9.9 480 81 0 false(unreach-call) 17   620 130 0 false(unreach-call) 43   1300 340 0 unknown 890    1200 9100   0 false(unreach-call) 21    780 250   0 false(unreach-call) 16     610 180    0 false(unreach-call) 16   660 130 0 unknown 12   690 97 0 unknown .51 13 5.9 0 timeout 900   5200 12000 0 timeout 900   2900 11000 0 timeout 900   4800 10000 0 timeout 900 2100 9800 0
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c error (134) .91 210 11    0 false(unreach-call) 6.6  260 91   1 witness invalid (false(unreach-call)) 8.9 500 76 0 false(unreach-call) 13   520 110 0 false(unreach-call) 81   3700 860 0 unknown 890    1700 9100   0 false(unreach-call) 21    790 210   0 false(unreach-call) 16     620 170    0 false(unreach-call) 21   650 170 0 unknown 11   670 89 0 unknown .50 12 5.0 0 timeout 900   2500 10000 0 timeout 900   5500 12000 0 false(unreach-call) 560   4900 6300 1 timeout 900 1800 7800 0
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c error (134) .89 210 13    0 false(unreach-call) 19    510 220   0 witness invalid (false(unreach-call)) 10   470 76 0 false(unreach-call) 34   1000 290 0 false(unreach-call) 110   2700 870 0 unknown 890    1500 9100   0 false(unreach-call) 59    1600 720   0 false(unreach-call) 49     1400 660    0 false(unreach-call) 140   3800 1700 0 unknown 12   680 110 0 unknown .49 12 5.9 0 timeout 900   5300 13000 0 timeout 900   4400 15000 0 timeout 900   5500 11000 0 timeout 900 1900 8000 0
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c error (134) .90 210 11    0 false(unreach-call) 6.6  260 100   1 witness invalid (false(unreach-call)) 8.6 500 77 0 false(unreach-call) 13   500 100 0 false(unreach-call) 79   3700 790 0 unknown 890    1700 7700   0 false(unreach-call) 20    790 250   0 false(unreach-call) 16     620 210    0 false(unreach-call) 18   620 140 0 unknown 11   670 94 0 unknown .52 12 5.5 0 timeout 900   2400 12000 0 timeout 900   5500 11000 0 false(unreach-call) 890   4800 11000 1 timeout 900 2100 8700 0
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c error (134) .90 210 9.3  0 false(unreach-call) 19    510 250   0 witness invalid (false(unreach-call)) 8.8 490 73 0 false(unreach-call) 36   1200 270 0 false(unreach-call) 97   2700 890 0 unknown 890    1700 8500   0 false(unreach-call) 59    1600 660   0 false(unreach-call) 48     1400 650    0 false(unreach-call) 84   3700 910 0 unknown 11   660 100 0 unknown .55 12 5.5 0 timeout 900   5300 11000 0 timeout 900   5300 12000 0 timeout 900   5200 10000 0 timeout 900 2000 7300 0
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error (134) .88 210 8.5  0 false(unreach-call) 6.8  260 75   0 witness invalid (false(unreach-call)) 9.6 500 83 0 false(unreach-call) 9.3 470 78 0 false(unreach-call) 30   1500 260 1 false(unreach-call) 700    1300 7000   0 false(unreach-call) 11    480 130   0 false(unreach-call) 15     620 200    0 false(unreach-call) 94   3800 900 0 unknown 12   670 96 0 unknown .48 12 5.8 0 false(unreach-call) 98   1800 830 1 timeout 900   5000 13000 0 false(unreach-call) 120   4600 1500 1 timeout 900 2100 9300 0
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c error (134) .90 210 11    0 false(unreach-call) 6.6  260 77   1 witness invalid (false(unreach-call)) 9.6 500 72 0 false(unreach-call) 17   650 150 0 false(unreach-call) 44   1400 350 0 unknown 890    1300 9400   0 false(unreach-call) 21    780 240   0 false(unreach-call) 15     610 200    0 false(unreach-call) 14   560 94 0 unknown 12   760 99 0 unknown .48 12 6.5 0 timeout 900   4600 11000 0 timeout 900   3400 15000 0 timeout 900   4800 11000 0 timeout 900 2100 7200 0
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c error (134) .93 210 10    0 false(unreach-call) 6.6  260 76   1 witness invalid (false(unreach-call)) 8.4 500 72 0 false(unreach-call) 13   510 110 0 false(unreach-call) 91   3700 850 0 false(unreach-call) 840    1600 8600   0 false(unreach-call) 21    790 230   0 false(unreach-call) 15     620 180    0 false(unreach-call) 20   680 160 0 unknown 12   680 91 0 unknown .52 12 5.4 0 timeout 900   3700 11000 0 timeout 900   5500 14000 0 timeout 900   5100 9600 0 timeout 900 1800 11000 0
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c error (134) .92 220 8.8  0 false(unreach-call) 6.7  260 69   1 witness invalid (false(unreach-call)) 8.9 490 78 0 false(unreach-call) 17   700 120 0 false(unreach-call) 39   1200 320 0 unknown 890    1300 9300   0 false(unreach-call) 21    780 220   0 false(unreach-call) 15     610 160    0 false(unreach-call) 14   590 110 0 unknown 12   670 100 0 unknown .48 12 5.4 0 timeout 900   4800 11000 0 timeout 900   3700 13000 0 timeout 900   4800 11000 0 timeout 900 2100 7300 0
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c error (134) .89 220 10    0 false(unreach-call) 20    510 230   0 witness invalid (false(unreach-call)) 9.4 480 71 0 false(unreach-call) 33   1000 280 0 false(unreach-call) 110   2900 1100 0 unknown 890    1500 8400   0 false(unreach-call) 61    1600 720   0 false(unreach-call) 48     1400 720    0 timeout 900   4100 13000 0 unknown 12   670 100 0 unknown .52 12 5.7 0 timeout 900   5300 13000 0 timeout 900   4800 13000 0 timeout 900   5400 11000 0 timeout 900 2400 8200 0
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c error (134) .90 220 11    0 false(unreach-call) 6.7  260 89   1 witness invalid (false(unreach-call)) 9.2 500 69 0 false(unreach-call) 16   650 130 0 false(unreach-call) 42   1100 310 0 unknown 890    1300 8800   0 false(unreach-call) 21    780 250   0 false(unreach-call) 16     610 200    0 false(unreach-call) 13   600 100 0 unknown 12   680 99 0 unknown .48 13 6.2 0 timeout 900   4600 12000 0 timeout 900   3900 13000 0 timeout 900   4800 11000 0 timeout 900 1900 7300 0
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c error (134) .79 180 8.7  0 true 39    650 420   1 false(unreach-call) 14   530 120 -16 true 36   1200 270 1 true 170   2800 1800 1 unknown 890    1600 12000   0 true 79    2400 800   1 true 90     2700 990    1 timeout 900   3800 12000 0 unknown 10   530 84 0 unknown .33 12 4.3 0 timeout 900   4600 9200 0 timeout 900   5400 13000 0 false(unreach-call) 400   4700 3900 -16 unknown 650 1700 5900 0
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c error (134) .78 180 8.3  0 true 38    600 370   1 false(unreach-call) 15   550 110 -16 true 50   1800 440 1 true 220   2800 2300 1 unknown 890    1600 9000   0 true 92    2500 1100   1 true 110     2800 1600    1 timeout 900   3800 11000 0 unknown 9.4 560 83 0 unknown .36 12 4.8 0 timeout 900   4600 8700 0 timeout 900   5400 13000 0 timeout 900   5300 10000 0 timeout 900 9800 8700 0
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c error (134) .76 180 9.5  0 true 38    600 400   1 false(unreach-call) 15   530 140 -16 true 41   1400 340 1 true 130   2800 1400 1 unknown 890    1600 11000   0 true 92    2500 1000   1 true 110     2800 1400    1 timeout 900   3100 12000 0 unknown 9.6 550 80 0 unknown .36 12 4.1 0 timeout 900   4600 9400 0 timeout 900   4700 13000 0 timeout 900   5200 12000 0 timeout 900 9700 8400 0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c error (134) .78 180 7.4  0 true 38    600 500   1 false(unreach-call) 14   530 110 -16 true 42   1500 330 1 true 160   2800 1700 1 unknown 890    1600 9500   0 true 92    2500 1100   1 true 110     2800 1200    1 timeout 900   3200 11000 0 unknown 9.7 650 84 0 unknown .35 12 4.0 0 timeout 900   4600 11000 0 timeout 900   5300 14000 0 false(unreach-call) 500   4800 5600 -16 timeout 900 9800 9000 0
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c error (134) .89 210 11    0 error (42) 870    1700 4600   0 false(unreach-call) 8.7 500 64 -16 true 18   660 130 1 true 150   4100 1400 1 unknown 890    1700 8700   0 timeout 900    15000 9700   0 timeout 900     15000 9700    0 true 370   4000 5400 1 unknown 11   680 92 0 unknown .49 12 5.6 0 timeout 900   5400 11000 0 timeout 900   5500 13000 0 timeout 900   6300 11000 0 timeout 900 2000 8000 0
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c error (134) .86 210 11    0 error (42) 870    1700 5800   0 false(unreach-call) 8.2 430 75 -16 true 47   1700 420 1 true 50   2600 500 1 unknown 890    1700 12000   0 timeout 900    15000 10000   0 timeout 900     15000 11000    0 true 86   3500 940 1 unknown 12   680 94 0 unknown .48 12 5.7 0 timeout 900   5200 10000 0 timeout 900   5500 12000 0 timeout 900   5900 12000 0 timeout 900 2100 11000 0
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c error (134) .94 220 11    0 error (42) 870    1700 5000   0 false(unreach-call) 17   600 130 -16 true 45   1400 330 1 true 290   4400 2800 1 unknown 890    1500 9300   0 timeout 900    14000 10000   0 timeout 900     14000 9300    0 true 860   4800 12000 1 unknown 12   690 94 0 unknown .52 13 6.4 0 timeout 900   5500 12000 0 timeout 900   5500 13000 0 timeout 900   6100 11000 0 timeout 900 1800 9000 0
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c error (134) .90 210 10    0 error (42) 870    1700 4900   0 false(unreach-call) 9.5 490 73 -16 true 29   940 220 1 true 130   4100 1100 1 unknown 890    1600 7500   0 timeout 900    15000 11000   0 timeout 900     15000 9400    0 false(unreach-call) 120   3100 1200 -16 unknown 11   670 99 0 unknown .53 12 6.2 0 timeout 900   5900 11000 0 timeout 900   5100 12000 0 timeout 900   5800 10000 0 timeout 900 2000 8800 0
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c error (134) .88 210 10    0 error (42) 870    1700 4200   0 false(unreach-call) 12   510 86 -16 true 32   920 270 1 true 140   3900 1300 1 unknown 890    1700 9000   0 timeout 900    14000 9500   0 timeout 900     14000 11000    0 true 850   4300 11000 1 unknown 12   670 100 0 unknown .51 12 5.4 0 timeout 900   6400 12000 0 timeout 900   5500 12000 0 timeout 900   6500 10000 0 timeout 900 2100 11000 0
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c error (134) .85 210 9.6  0 error (42) 870    1700 4900   0 false(unreach-call) 9.5 510 81 -16 true 28   960 230 1 true 120   4100 1100 1 unknown 890    1700 12000   0 timeout 900    15000 9900   0 timeout 900     14000 9400    0 false(unreach-call) 100   3500 930 -16 unknown 12   680 100 0 unknown .51 12 6.2 0 timeout 900   5400 13000 0 timeout 900   5500 14000 0 timeout 900   6000 12000 0 timeout 900 1900 7700 0
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c error (134) .91 210 9.8  0 error (42) 870    1700 4200   0 false(unreach-call) 10   520 77 -16 true 22   700 160 1 true 130   2800 1400 1 unknown 890    1700 9700   0 timeout 900    14000 9100   0 timeout 900     15000 10000    0 true 400   3900 5500 1 unknown 12   680 100 0 unknown .50 13 5.8 0 timeout 900   6600 13000 0 timeout 900   5500 13000 0 timeout 900   6300 11000 0 timeout 900 1800 8200 0
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c error (134) .87 210 8.9  0 error (42) 870    1700 4100   0 false(unreach-call) 9.5 490 78 -16 true 35   1100 270 1 true 110   4000 1100 1 unknown 890    1700 11000   0 timeout 900    15000 12000   0 timeout 900     14000 9100    0 false(unreach-call) 97   3800 1100 -16 unknown 12   670 84 0 unknown .50 12 5.5 0 timeout 900   5300 10000 0 timeout 900   5500 13000 0 timeout 900   6100 10000 0 timeout 900 2000 9600 0
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c error (134) .88 210 11    0 error (42) 870    1700 4700   0 false(unreach-call) 13   510 110 -16 true 40   1100 280 1 true 250   4300 2400 1 unknown 890    1600 8400   0 timeout 900    14000 8900   0 timeout 900     14000 8400    0 true 480   4700 5500 1 unknown 12   670 100 0 unknown .50 12 5.5 0 timeout 900   8900 8800 0 timeout 900   5500 14000 0 timeout 900   6200 11000 0 timeout 900 2000 12000 0
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c error (134) .85 210 12    0 error (42) 870    1700 7200   0 false(unreach-call) 9.3 500 74 -16 true 110   3700 1200 1 true 110   3900 1100 1 unknown 890    1700 8700   0 timeout 900    15000 12000   0 timeout 900     15000 8100    0 true 160   3900 1700 1 unknown 11   670 84 0 unknown .49 12 6.4 0 timeout 900   6500 9800 0 timeout 900   5500 15000 0 timeout 900   6000 11000 0 timeout 900 2100 8600 0
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c error (134) .90 220 10    0 error (42) 870    1700 5000   0 false(unreach-call) 15   580 120 -16 true 55   1900 560 1 true 200   4200 1700 1 unknown 890    1500 8300   0 timeout 900    14000 11000   0 timeout 900     14000 11000    0 true 570   5000 6500 1 unknown 12   690 100 0 unknown .48 12 5.7 0 timeout 900   6900 11000 0 timeout 900   5500 13000 0 timeout 900   6500 11000 0 timeout 900 1700 9800 0
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c error (134) .90 220 10    0 error (42) 870    1700 4600   0 false(unreach-call) 14   520 110 -16 true 38   1000 280 1 true 150   3900 1400 1 unknown 890    1700 9500   0 timeout 900    15000 11000   0 timeout 900     14000 9400    0 timeout 900   4200 11000 0 unknown 11   670 91 0 unknown .50 12 5.9 0 timeout 900   6000 11000 0 timeout 900   5500 12000 0 timeout 900   6300 13000 0 timeout 900 2000 8200 0
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c error (134) .93 220 9.6  0 error (42) 870    1700 4500   0 false(unreach-call) 15   600 110 -16 true 40   1300 340 1 true 230   4300 2200 1 unknown 890    1500 8100   0 timeout 900    14000 9300   0 timeout 900     14000 9900    0 true 820   4900 9400 1 unknown 12   680 100 0 unknown .50 13 5.7 0 timeout 900   7400 10000 0 timeout 900   5500 12000 0 timeout 900   6300 8400 0 timeout 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 36000 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 1900 68000 20000 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 44000 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 5800 69000 70000 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 4800 43000 59000 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 26000 11000 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 15000 4200 -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 15000 4200 -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