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 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: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-ProductLines cbmc.sv-comp18.ReachSafety-ProductLines cpa-bam-bnb.sv-comp18.ReachSafety-ProductLines cpa-bam-slicing.sv-comp18.ReachSafety-ProductLines cpa-seq.sv-comp18.ReachSafety-ProductLines depthk.sv-comp18.ReachSafety-ProductLines esbmc-incr.sv-comp18.ReachSafety-ProductLines esbmc-kind.sv-comp18.ReachSafety-ProductLines interpchecker.sv-comp18.ReachSafety-ProductLines symbiotic.sv-comp18.ReachSafety-ProductLines uautomizer.sv-comp18.ReachSafety-ProductLines ukojak.sv-comp18.ReachSafety-ProductLines utaipan.sv-comp18.ReachSafety-ProductLines veriabs.sv-comp18.ReachSafety-ProductLines
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/product-lines/ 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
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 6.0  1200 56    1 false(unreach-call) .45 42 4.5 1 false(unreach-call) 92   4600 710 1 false(unreach-call) 480   9700 3000 1 false(unreach-call) 7.4 310 53 1 false(unreach-call) 480    380 4200   1 false(unreach-call) .20 38 1.9 1 false(unreach-call) .17  39 2.0  1 timeout 900   3900 13000 0 false(unreach-call) .38 18 4.6 1 timeout 900   13000 8000 0 timeout 900   3300 11000 0 timeout 900   4700 12000 0 unknown 380 1200 2800 0
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 9.9  2000 81    1 false(unreach-call) .51 42 4.9 1 false(unreach-call) 130   5700 910 1 timeout 910   11000 5200 0 false(unreach-call) 7.2 310 66 1 false(unreach-call) 480    520 4200   1 false(unreach-call) .17 39 1.6 1 false(unreach-call) .20  39 2.2  1 timeout 900   4200 13000 0 false(unreach-call) .38 19 3.8 1 timeout 910   13000 7300 0 timeout 900   2800 11000 0 timeout 900   4600 9600 0 unknown 400 1400 3800 0
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 6.2  1300 60    1 false(unreach-call) .47 42 4.3 1 false(unreach-call) 93   4800 670 1 timeout 900   11000 4600 0 false(unreach-call) 7.3 320 66 1 false(unreach-call) 480    420 5600   1 false(unreach-call) .19 39 1.7 1 false(unreach-call) .19  39 1.9  1 timeout 910   4300 11000 0 false(unreach-call) .38 19 4.6 1 timeout 900   13000 6100 0 timeout 900   2800 15000 0 timeout 900   4600 12000 0 unknown 400 1200 2800 0
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 11    2100 100    1 false(unreach-call) .47 42 4.6 1 false(unreach-call) 140   6000 980 1 timeout 900   11000 4700 0 false(unreach-call) 7.1 310 57 1 false(unreach-call) 6.3  540 64   1 false(unreach-call) .16 39 1.9 1 false(unreach-call) .18  39 1.9  1 timeout 900   4000 11000 0 false(unreach-call) .39 19 4.9 1 timeout 910   12000 7800 0 timeout 900   2800 12000 0 timeout 900   4700 11000 0 unknown 400 1400 3500 0
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 36    7000 320    1 false(unreach-call) 11    450 110   1 timeout 910   11000 5000 0 timeout 910   11000 5000 0 false(unreach-call) 8.4 360 75 1 false(unreach-call) 530    1400 5600   1 false(unreach-call) 4.7  160 49   1 false(unreach-call) 6.1   200 63    1 timeout 900   4200 12000 0 false(unreach-call) .41 23 6.1 1 timeout 910   13000 6500 0 timeout 900   2500 15000 0 timeout 900   4700 11000 0 timeout 900 5900 6900 0
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 41    850 490    1 false(unreach-call) 1.2  42 13   1 timeout 910   11000 5600 0 timeout 900   11000 4700 0 false(unreach-call) 7.5 330 58 1 false(unreach-call) 490    180 6300   1 false(unreach-call) .23 39 2.4 1 false(unreach-call) 1.4   61 16    1 timeout 960   8100 9500 0 false(unreach-call) .37 18 4.8 1 timeout 900   13000 8800 0 timeout 900   3300 13000 0 timeout 900   5400 11000 0 unknown 210 750 2000 0
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 43    900 360    1 false(unreach-call) 1.2  42 13   1 timeout 910   11000 5200 0 timeout 900   11000 4600 0 false(unreach-call) 7.7 330 64 1 false(unreach-call) 490    200 6900   1 false(unreach-call) .22 39 2.4 1 false(unreach-call) 1.5   63 18    1 timeout 970   9200 9400 0 false(unreach-call) .38 19 4.6 1 timeout 900   14000 6900 0 timeout 900   3200 13000 0 timeout 900   4600 10000 0 unknown 210 770 2000 0
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 43    1200 450    1 false(unreach-call) 1.2  42 12   1 timeout 900   11000 5200 0 timeout 910   11000 5700 0 false(unreach-call) 7.4 330 68 1 false(unreach-call) 500    240 6800   1 false(unreach-call) .22 39 2.1 1 false(unreach-call) 1.9   76 21    1 timeout 970   8900 10000 0 false(unreach-call) .37 19 4.4 1 timeout 900   13000 7400 0 timeout 900   3100 12000 0 timeout 900   4700 11000 0 unknown 210 760 2200 0
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 49    1300 380    1 false(unreach-call) 1.3  43 16   1 timeout 910   11000 5700 0 timeout 900   11000 4300 0 false(unreach-call) 7.6 340 58 1 false(unreach-call) 500    330 5800   1 false(unreach-call) .23 39 2.2 1 false(unreach-call) 2.0   79 27    1 timeout 960   10000 9500 0 false(unreach-call) .37 19 5.1 1 timeout 900   13000 6600 0 timeout 900   3100 11000 0 timeout 900   4600 10000 0 unknown 210 760 2300 0
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 43    890 370    1 false(unreach-call) 1.2  42 14   1 timeout 900   11000 5600 0 timeout 900   11000 4800 0 false(unreach-call) 7.3 320 58 1 false(unreach-call) 490    210 6000   1 false(unreach-call) .20 39 2.2 1 false(unreach-call) 1.6   65 18    1 timeout 970   8100 8600 0 false(unreach-call) .39 19 3.8 1 timeout 910   13000 6000 0 timeout 900   2900 14000 0 timeout 900   8200 10000 0 unknown 210 760 2400 0
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 45    950 560    1 false(unreach-call) 1.2  42 13   1 timeout 910   11000 6100 0 timeout 910   11000 4700 0 false(unreach-call) 7.6 330 59 1 false(unreach-call) 490    210 7200   1 false(unreach-call) .23 39 2.2 1 false(unreach-call) 1.6   68 21    1 timeout 970   9600 8900 0 false(unreach-call) .37 19 4.9 1 timeout 900   12000 7000 0 timeout 900   4600 11000 0 timeout 900   4600 10000 0 unknown 220 780 1900 0
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 53    1200 420    1 false(unreach-call) 1.2  42 12   1 timeout 910   11000 5100 0 timeout 910   11000 4800 0 false(unreach-call) 7.6 330 64 1 false(unreach-call) 500    320 6000   1 false(unreach-call) .24 40 2.3 1 false(unreach-call) 2.0   80 24    1 timeout 960   8200 9600 0 false(unreach-call) .39 20 4.6 1 timeout 900   13000 7200 0 timeout 900   3700 14000 0 timeout 900   4600 11000 0 unknown 210 780 2100 0
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 62    1300 440    1 false(unreach-call) 1.3  43 16   1 timeout 900   11000 6100 0 timeout 910   11000 5000 0 false(unreach-call) 7.8 340 52 1 false(unreach-call) 500    340 5500   1 false(unreach-call) .22 40 3.2 1 false(unreach-call) 2.3   84 28    1 timeout 920   8800 9400 0 false(unreach-call) .38 20 4.5 1 timeout 910   13000 6500 0 timeout 900   3100 12000 0 timeout 900   4600 10000 0 unknown 210 760 2400 0
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 140    3700 1100    1 false(unreach-call) 85    1200 760   1 timeout 900   11000 5700 0 timeout 910   11000 4500 0 false(unreach-call) 9.8 380 83 1 false(unreach-call) 700    790 9100   1 false(unreach-call) 7.3  190 110   1 false(unreach-call) 20     300 220    1 timeout 970   7400 10000 0 false(unreach-call) .44 24 6.5 1 timeout 910   13000 7000 0 timeout 900   4300 13000 0 timeout 900   4400 11000 0 unknown 690 6800 4800 0
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 36    870 380    1 false(unreach-call) 1.2  42 12   1 timeout 910   11000 5800 0 timeout 910   11000 4600 0 false(unreach-call) 7.1 320 59 1 false(unreach-call) 490    190 5100   1 false(unreach-call) .23 39 2.1 1 false(unreach-call) 1.7   68 24    1 timeout 900   3500 13000 0 false(unreach-call) .38 18 4.3 1 timeout 910   14000 5900 0 timeout 900   5400 12000 0 timeout 900   6100 11000 0 unknown 210 850 2500 0
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 37    930 330    1 false(unreach-call) 1.2  42 12   1 timeout 900   11000 5600 0 timeout 910   11000 5000 0 false(unreach-call) 7.9 320 62 1 false(unreach-call) 490    200 5800   1 false(unreach-call) .20 39 2.4 1 false(unreach-call) 1.8   70 21    1 timeout 900   3600 12000 0 false(unreach-call) .36 19 4.9 1 timeout 900   14000 5200 0 timeout 900   5700 12000 0 timeout 900   13000 7600 0 unknown 210 810 2100 0
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1200 540    1 false(unreach-call) 1.2  42 12   1 timeout 910   11000 5700 0 timeout 910   11000 5100 0 false(unreach-call) 7.3 320 61 1 false(unreach-call) 500    240 5700   1 false(unreach-call) .23 39 2.2 1 false(unreach-call) 2.2   83 28    1 timeout 900   3600 11000 0 false(unreach-call) .37 19 4.7 1 timeout 900   13000 6200 0 timeout 900   3400 15000 0 timeout 900   6500 10000 0 unknown 210 790 1900 0
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 44    1300 340    1 false(unreach-call) 1.3  43 13   1 timeout 910   11000 5500 0 timeout 900   11000 4300 0 false(unreach-call) 7.5 330 59 1 false(unreach-call) 500    330 5800   1 false(unreach-call) .21 40 2.2 1 false(unreach-call) 2.4   85 28    1 timeout 900   3800 14000 0 false(unreach-call) .37 20 5.1 1 timeout 900   13000 7800 0 timeout 900   3700 13000 0 timeout 900   4600 11000 0 unknown 210 820 2300 0
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 32    900 310    1 false(unreach-call) 1.2  42 11   1 timeout 910   11000 5300 0 timeout 910   11000 5200 0 false(unreach-call) 7.3 310 57 1 false(unreach-call) 490    200 5800   1 false(unreach-call) .19 39 2.5 1 false(unreach-call) 1.8   71 22    1 timeout 900   3100 11000 0 false(unreach-call) .36 19 4.4 1 timeout 900   14000 5200 0 timeout 900   4700 14000 0 timeout 900   6200 10000 0 unknown 210 760 2000 0
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 36    970 290    1 false(unreach-call) 1.2  42 13   1 timeout 900   11000 5400 0 timeout 910   11000 5300 0 false(unreach-call) 7.7 330 57 1 false(unreach-call) 490    220 6100   1 false(unreach-call) .23 39 2.2 1 false(unreach-call) 1.9   74 22    1 timeout 900   3900 12000 0 false(unreach-call) .38 19 4.9 1 timeout 900   13000 7700 0 timeout 900   4400 13000 0 timeout 900   4700 11000 0 unknown 210 760 2200 0
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 40    1200 380    1 false(unreach-call) 1.2  42 14   1 timeout 910   11000 5600 0 timeout 910   11000 4500 0 false(unreach-call) 7.4 330 58 1 false(unreach-call) 500    320 6000   1 false(unreach-call) .21 40 2.3 1 false(unreach-call) 2.2   86 35    1 timeout 900   3800 13000 0 false(unreach-call) .39 20 5.3 1 timeout 910   14000 6600 0 timeout 900   4800 12000 0 timeout 900   5600 11000 0 unknown 210 840 2600 0
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1300 430    1 false(unreach-call) 1.2  43 14   1 timeout 910   11000 5900 0 timeout 910   11000 4600 0 false(unreach-call) 7.5 330 65 1 false(unreach-call) 500    340 5900   1 false(unreach-call) .24 40 2.3 1 false(unreach-call) 2.5   91 28    1 timeout 900   3700 11000 0 false(unreach-call) .38 20 4.8 1 timeout 900   13000 7100 0 timeout 900   3700 15000 0 timeout 900   4600 11000 0 unknown 210 830 2300 0
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 130    3800 1200    1 false(unreach-call) 48    930 380   1 timeout 900   11000 5500 0 timeout 900   11000 4800 0 false(unreach-call) 9.7 370 85 1 false(unreach-call) 700    730 8800   1 false(unreach-call) 7.4  190 84   1 false(unreach-call) 20     300 210    1 timeout 950   8000 8900 0 false(unreach-call) .45 24 6.1 1 timeout 910   14000 5200 0 timeout 900   1500 16000 0 timeout 900   6500 10000 0 unknown 890 7900 6000 0
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 2.9  580 31    1 false(unreach-call) .65 43 6.4 1 timeout 900   8300 9100 0 timeout 910   11000 5100 0 false(unreach-call) 8.2 350 76 1 false(unreach-call) 480    250 5100   1 false(unreach-call) .20 39 1.9 1 false(unreach-call) .17  39 1.9  1 timeout 940   6500 11000 0 false(unreach-call) .38 19 4.3 1 timeout 900   13000 6300 0 timeout 900   1600 10000 0 timeout 900   5400 10000 0 unknown 220 790 1400 0
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 3.1  620 29    1 false(unreach-call) .61 43 5.7 1 timeout 900   8800 8400 0 timeout 910   11000 6200 0 false(unreach-call) 8.3 350 71 1 false(unreach-call) 480    270 5500   1 false(unreach-call) .17 39 2.0 1 false(unreach-call) .20  39 2.1  1 timeout 940   6700 11000 0 false(unreach-call) .39 20 4.5 1 timeout 910   13000 5900 0 timeout 900   2900 11000 0 timeout 900   5500 11000 0 unknown 210 770 1600 0
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 3.2  660 32    1 false(unreach-call) .66 43 7.3 1 timeout 900   8600 6900 0 timeout 900   11000 4900 0 false(unreach-call) 8.2 350 57 1 false(unreach-call) 480    420 5500   1 false(unreach-call) .21 39 2.0 1 false(unreach-call) .17  39 1.9  1 timeout 940   7300 11000 0 false(unreach-call) .39 20 4.9 1 timeout 910   13000 6500 0 timeout 900   2900 14000 0 timeout 900   4600 11000 0 unknown 210 760 1900 0
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 6.1  1200 61    1 false(unreach-call) .67 43 7.1 1 timeout 900   8700 8600 0 timeout 910   9300 7800 0 false(unreach-call) 8.3 390 72 1 false(unreach-call) 480    390 6100   1 false(unreach-call) .18 39 2.2 1 false(unreach-call) .20  39 1.9  1 timeout 940   6400 12000 0 false(unreach-call) .37 21 4.1 1 timeout 900   13000 6400 0 timeout 900   5400 12000 0 timeout 900   5400 11000 0 unknown 220 770 1400 0
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 5.4  1000 53    1 false(unreach-call) .68 44 6.4 1 timeout 900   9000 7800 0 timeout 900   11000 4800 0 false(unreach-call) 8.8 380 69 1 false(unreach-call) 480    320 5900   1 false(unreach-call) .19 40 2.0 1 false(unreach-call) .23  39 2.1  1 timeout 940   6900 10000 0 false(unreach-call) .37 21 4.9 1 timeout 910   13000 6900 0 timeout 900   2500 12000 0 timeout 900   4600 13000 0 unknown 220 780 1500 0
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 11    2000 99    1 false(unreach-call) .69 44 8.0 1 timeout 900   8600 9100 0 timeout 900   9300 8100 0 false(unreach-call) 8.8 380 74 1 false(unreach-call) 480    540 3800   1 false(unreach-call) .18 40 2.0 1 false(unreach-call) .19  40 2.7  1 timeout 930   6300 10000 0 false(unreach-call) .38 22 5.5 1 timeout 910   14000 6100 0 timeout 900   5400 13000 0 timeout 900   4600 11000 0 unknown 210 770 1400 0
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 3.6  700 34    1 false(unreach-call) .64 43 6.4 1 timeout 900   8700 7800 0 timeout 910   11000 6600 0 false(unreach-call) 8.0 360 64 1 false(unreach-call) 480    430 5200   1 false(unreach-call) .21 39 2.0 1 false(unreach-call) .21  39 1.8  1 timeout 940   7100 11000 0 false(unreach-call) .40 21 4.6 1 timeout 900   13000 5700 0 timeout 900   2900 11000 0 timeout 900   5400 11000 0 unknown 220 760 1500 0
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 6.6  1300 63    1 false(unreach-call) .64 43 7.5 1 timeout 900   8600 7800 0 timeout 900   9800 7900 0 false(unreach-call) 8.2 370 68 1 false(unreach-call) 480    420 5600   1 false(unreach-call) .20 39 1.8 1 false(unreach-call) .23  40 1.6  1 timeout 930   6500 9800 0 false(unreach-call) .38 22 4.5 1 timeout 900   14000 5600 0 timeout 900   5400 14000 0 timeout 900   4600 12000 0 unknown 220 760 1600 0
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 5.5  1100 64    1 false(unreach-call) .68 44 7.2 1 timeout 900   8500 7600 0 timeout 900   11000 5800 0 false(unreach-call) 8.6 370 72 1 false(unreach-call) 480    330 5100   1 false(unreach-call) .18 40 2.1 1 false(unreach-call) .18  40 2.0  1 timeout 940   6700 11000 0 false(unreach-call) .39 22 5.6 1 timeout 910   13000 5600 0 timeout 900   2500 12000 0 timeout 900   4600 10000 0 unknown 210 750 1600 0
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 11    2100 120    1 false(unreach-call) .65 44 8.1 1 timeout 900   8700 9400 0 timeout 910   9900 8400 0 false(unreach-call) 8.2 400 65 1 false(unreach-call) 480    560 4400   1 false(unreach-call) .19 40 2.1 1 false(unreach-call) .22  40 2.1  1 timeout 940   7300 9600 0 false(unreach-call) .41 22 4.7 1 timeout 910   13000 7200 0 timeout 900   5400 14000 0 timeout 900   4600 11000 0 unknown 220 810 1500 0
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 38    7000 400    1 false(unreach-call) 43    950 410   1 timeout 900   8500 8900 0 timeout 910   11000 5300 0 false(unreach-call) 11   480 80 1 false(unreach-call) 610    1400 4500   1 false(unreach-call) 11    260 100   1 false(unreach-call) 12     330 160    1 timeout 910   6500 10000 0 false(unreach-call) .44 26 6.2 1 timeout 910   13000 6600 0 timeout 900   3100 12000 0 timeout 900   4700 12000 0 unknown 810 7900 6400 0
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 39    900 390    1 false(unreach-call) 1.2  44 13   1 timeout 900   11000 5800 0 timeout 910   11000 4900 0 false(unreach-call) 7.5 330 63 1 false(unreach-call) 490    200 5100   1 false(unreach-call) .23 39 2.2 1 false(unreach-call) 1.8   71 22    1 timeout 900   4200 12000 0 false(unreach-call) .36 19 4.6 1 timeout 910   14000 4900 0 timeout 900   4500 15000 0 timeout 910   14000 5000 0 unknown 440 1400 3200 0
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 39    950 400    1 false(unreach-call) 1.3  42 14   1 timeout 900   11000 6200 0 timeout 900   11000 4900 0 false(unreach-call) 7.7 340 72 1 false(unreach-call) 490    220 6000   1 false(unreach-call) .22 39 2.3 1 false(unreach-call) 1.8   77 26    1 timeout 920   5000 14000 0 false(unreach-call) .39 20 4.7 1 timeout 910   14000 5000 0 timeout 900   5200 11000 0 timeout 910   14000 5400 0 unknown 440 1600 3700 0
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 46    1300 360    1 false(unreach-call) 1.2  42 13   1 timeout 910   11000 5900 0 timeout 910   11000 4300 0 false(unreach-call) 7.6 330 60 1 false(unreach-call) 500    320 6800   1 false(unreach-call) .22 39 2.6 1 false(unreach-call) 2.3   88 27    1 timeout 910   4600 13000 0 false(unreach-call) .37 20 4.6 1 timeout 910   14000 5000 0 timeout 900   4900 13000 0 timeout 910   14000 5200 0 unknown 440 1400 2900 0
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 47    1300 340    1 false(unreach-call) 1.3  42 13   1 timeout 900   11000 5300 0 timeout 900   11000 4600 0 false(unreach-call) 7.6 340 62 1 false(unreach-call) 500    340 6300   1 false(unreach-call) .20 40 3.1 1 false(unreach-call) 2.3   91 26    1 timeout 970   6100 11000 0 false(unreach-call) .39 20 4.8 1 timeout 910   14000 5600 0 timeout 900   2600 12000 0 timeout 910   14000 5000 0 unknown 440 1500 3100 0
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 93    3700 870    1 false(unreach-call) 47    930 450   0 timeout 910   11000 5800 0 timeout 900   11000 5500 0 false(unreach-call) 9.5 400 84 1 false(unreach-call) 690    730 7500   1 false(unreach-call) 7.8  190 80   1 false(unreach-call) 20     290 250    1 timeout 970   9000 11000 0 false(unreach-call) .45 24 5.8 1 timeout 910   14000 5200 0 timeout 900   1500 13000 0 timeout 910   14000 4900 0 timeout 900 3100 6700 0
elevator_spec13_product21_true-unreach-call_false-termination.cil.c error (5) 5.4  1000 48    0 error (42) 870    12000 11000   0 timeout 900   8300 7100 0 timeout 900   11000 5100 0 true 5.2 280 44 1 unknown 890    1500 12000   0 timeout 900    1500 12000   0 timeout 900     1500 11000    0 timeout 900   4000 11000 0 timeout (timeout) 900    15000 12000   0 timeout 910   14000 5300 0 timeout 900   2600 15000 0 timeout 900   5400 10000 0 unknown 480 1600 2900 0
elevator_spec13_product22_true-unreach-call_false-termination.cil.c error (5) 11    1900 100    0 error (42) 870    12000 14000   0 timeout 910   11000 7200 0 timeout 910   11000 5700 0 true 5.6 280 52 1 unknown 900    2100 10000   0 timeout 900    1400 11000   0 timeout 900     1400 12000    0 timeout 900   4000 11000 0 timeout (timeout) 900    15000 12000   0 timeout 910   14000 5700 0 timeout 900   2000 14000 0 timeout 900   4700 12000 0 unknown 470 1600 3800 0
elevator_spec13_product23_true-unreach-call_false-termination.cil.c error (5) 5.9  1100 50    0 out of memory 750    15000 10000   0 timeout 900   8100 7400 0 timeout 900   11000 5500 0 true 5.2 280 40 1 unknown 890    660 10000   0 timeout 900    1900 13000   0 timeout 900     1900 11000    0 timeout 900   4000 12000 0 timeout (timeout) 900    15000 13000   0 timeout 910   14000 6000 0 timeout 900   2500 11000 0 timeout 900   4600 11000 0 unknown 460 2100 2500 0
elevator_spec13_product24_true-unreach-call_false-termination.cil.c error (5) 11    2100 98    0 out of memory 760    15000 11000   0 timeout 900   8200 7400 0 timeout 910   11000 5400 0 true 5.3 280 44 1 unknown 890    2400 11000   0 timeout 900    1900 14000   0 timeout 900     1900 11000    0 timeout 900   4100 13000 0 timeout (timeout) 900    15000 12000   0 timeout 910   14000 6300 0 timeout 900   2300 11000 0 timeout 900   4900 11000 0 unknown 460 2000 2700 0
elevator_spec13_product29_true-unreach-call_false-termination.cil.c error (5) 5.6  1100 44    0 error (42) 880    12000 11000   0 timeout 900   8600 8100 0 timeout 900   11000 5800 0 true 5.3 280 43 1 unknown 890    1700 10000   0 timeout 900    1500 11000   0 timeout 900     1500 14000    0 timeout 900   3900 11000 0 timeout (timeout) 900    15000 12000   0 timeout 910   13000 5800 0 timeout 900   2500 11000 0 timeout 900   5400 11000 0 unknown 480 1600 2900 0
elevator_spec13_product30_true-unreach-call_false-termination.cil.c error (5) 11    2000 91    0 error (42) 880    12000 11000   0 timeout 910   11000 7500 0 timeout 910   11000 5300 0 true 5.5 280 43 1 unknown 890    740 11000   0 timeout 900    1400 11000   0 timeout 900     1500 11000    0 timeout 900   4000 12000 0 timeout (timeout) 900    15000 13000   0 timeout 910   14000 5700 0 timeout 900   2200 11000 0 timeout 900   5300 12000 0 unknown 480 1600 3100 0
elevator_spec13_product31_true-unreach-call_false-termination.cil.c error (5) 5.8  1200 60    0 out of memory 750    15000 9700   0 timeout 900   8600 8000 0 timeout 910   11000 4900 0 true 5.4 280 44 1 unknown 900    660 11000   0 timeout 900    1900 13000   0 timeout 900     2000 11000    0 timeout 900   4000 11000 0 timeout (timeout) 900    15000 12000   0 timeout 910   13000 6000 0 timeout 900   2500 13000 0 timeout 900   4700 11000 0 unknown 460 2100 2600 0
elevator_spec13_product32_true-unreach-call_false-termination.cil.c error (5) 11    2200 140    0 out of memory 750    15000 9800   0 timeout 900   8000 7600 0 timeout 910   11000 5300 0 true 5.3 290 42 1 unknown 900    750 12000   0 timeout 900    2000 14000   0 timeout 900     1900 13000    0 timeout 900   4000 14000 0 timeout (timeout) 900    15000 13000   0 timeout 910   14000 6100 0 timeout 900   2300 9900 0 timeout 900   5400 13000 0 unknown 470 2000 3300 0
elevator_spec13_productSimulator_true-unreach-call_false-termination.cil.c error (5) 47    7300 380    0 error (42) 870    460 9900   0 timeout 900   8100 8100 0 timeout 910   11000 4600 0 true 7.2 300 60 1 unknown 900    1400 8500   0 timeout 900    3300 9400   0 timeout 900     3700 7000    0 timeout 900   4400 13000 0 timeout (timeout) 900    15000 11000   0 timeout 900   11000 7800 0 timeout 900   2400 11000 0 timeout 900   5000 10000 0 timeout 900 2500 8000 0
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 20    860 210    2 true 3.3  47 37   1 true 120   5500 870 2 true 99   4000 770 2 true 6.1 290 49 2 true 540    300 6500   2 true .64 36 8.6 2 true 1.6   51 21    2 timeout 900   4000 13000 0 true .37 17 3.9 2 timeout 900   13000 7300 0 timeout 900   3100 12000 0 timeout 900   4600 10000 0 true 120 1000 1300 2
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 20    910 180    2 true 3.3  47 42   1 true 120   5300 830 2 timeout 900   11000 4900 0 true 6.2 290 52 2 true 550    290 7300   2 true .67 37 8.2 2 true 1.7   54 23    2 timeout 900   3700 11000 0 true .37 18 4.7 2 timeout 900   13000 6400 0 timeout 900   1500 14000 0 timeout 900   4600 11000 0 true 120 1000 1100 2
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 24    1000 240    2 true 3.4  47 37   1 true 120   5500 960 2 true 110   4100 680 2 true 5.8 290 51 2 true 550    290 7000   2 true .75 37 8.1 2 true 1.8   52 23    2 timeout 900   4000 13000 0 true .37 17 4.7 2 timeout 900   13000 7700 0 timeout 900   2400 13000 0 timeout 900   4600 12000 0 true 120 1100 1100 2
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 10    1300 100    2 true 3.5  47 44   1 true 190   6500 1200 2 timeout 910   11000 5200 0 true 6.1 290 52 2 true 660    310 7700   2 true 1.1  37 15   2 true 2.3   61 34    2 timeout 900   4000 11000 0 true .36 22 5.0 2 timeout 900   12000 8000 0 timeout 900   2600 12000 0 timeout 900   4600 11000 0 true 160 1300 1600 2
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 24    1100 220    2 true 3.5  47 40   1 true 140   5500 890 2 timeout 910   11000 4900 0 true 6.6 290 53 2 true 550    290 6500   2 true .76 37 9.1 2 true 1.9   54 23    2 timeout 900   3400 12000 0 true .37 18 4.4 2 timeout 910   13000 7500 0 timeout 900   1800 12000 0 timeout 900   4700 12000 0 true 130 1100 1100 2
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 11    1400 110    2 true 3.4  47 44   1 true 180   6500 1100 2 timeout 900   11000 5600 0 true 6.1 290 52 2 true 660    330 7700   2 true 1.1  37 12   2 true 2.4   64 35    2 timeout 900   4000 11000 0 true .36 19 4.5 2 timeout 900   12000 8800 0 timeout 900   2600 11000 0 timeout 900   4600 10000 0 true 160 1300 1500 2
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 28    1000 240    2 true 2.8  45 27   1 timeout 900   11000 5700 0 timeout 910   11000 5000 0 true 5.7 290 51 2 true 520    290 6900   2 true .54 37 6.4 2 true 1.2   46 14    2 timeout 960   8600 9600 0 true .36 17 5.5 2 timeout 900   11000 8300 0 timeout 900   3200 12000 0 timeout 900   4600 10000 0 true 160 1500 1100 2
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 30    1100 300    2 true 3.0  45 34   1 timeout 900   11000 4700 0 timeout 900   11000 4800 0 true 5.7 280 50 2 true 540    290 6500   2 true .62 37 8.7 2 true 1.4   48 19    2 timeout 970   8100 9400 0 true .35 18 4.9 2 timeout 910   13000 6400 0 timeout 900   2500 14000 0 timeout 900   4700 11000 0 true 170 1700 1400 2
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 29    1000 270    2 true 2.8  45 36   1 timeout 910   11000 5300 0 timeout 910   11000 5600 0 true 5.8 290 48 2 true 540    290 6300   2 true .54 37 6.6 2 true 1.3   50 16    2 timeout 960   8400 8800 0 true .35 18 4.2 2 timeout 910   12000 7800 0 timeout 900   2500 13000 0 timeout 900   4600 11000 0 true 170 1700 1400 2
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 31    1100 300    2 true 3.1  45 33   1 timeout 900   11000 5200 0 timeout 910   11000 3900 0 true 6.0 290 47 2 true 550    290 7300   2 true .60 37 6.9 2 true 1.5   51 20    2 timeout 970   8200 9800 0 true .38 18 4.2 2 timeout 900   13000 7100 0 timeout 900   2900 10000 0 timeout 900   4200 9500 0 true 170 1700 1100 2
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 33    1100 300    2 true 2.9  45 30   1 timeout 900   11000 5800 0 timeout 910   11000 5000 0 true 5.8 290 47 2 true 530    290 6300   2 true .51 37 6.9 2 true 1.2   46 13    2 timeout 960   10000 9000 0 true .34 18 5.4 2 timeout 910   11000 9800 0 timeout 900   2100 12000 0 timeout 900   5400 10000 0 true 160 1600 1200 2
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 31    1100 280    2 true 3.1  46 45   1 timeout 910   11000 4500 0 timeout 910   11000 4700 0 true 6.1 290 51 2 true 550    300 7300   2 true .54 37 6.8 2 true 1.3   49 15    2 timeout 970   8300 8700 0 true .36 18 4.5 2 timeout 900   13000 8000 0 timeout 900   2900 11000 0 timeout 900   4500 10000 0 true 170 1700 1200 2
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 39    1500 350    2 true 3.0  45 39   1 timeout 900   11000 4700 0 timeout 900   11000 5100 0 true 6.0 290 49 2 true 570    290 6800   2 true .61 37 7.1 2 true 1.7   56 21    2 timeout 920   8900 10000 0 true .36 18 5.0 2 timeout 900   13000 7400 0 timeout 900   2200 14000 0 timeout 900   4600 9900 0 true 170 1700 1200 2
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 39    1600 420    2 true 3.2  47 39   1 timeout 900   11000 5100 0 timeout 900   11000 5200 0 true 6.4 290 51 2 true 580    300 7300   2 true .70 38 9.7 2 true 1.9   58 27    2 timeout 970   8400 9500 0 true .37 19 4.5 2 timeout 910   13000 6600 0 timeout 900   2700 14000 0 timeout 900   4600 11000 0 true 160 1700 1200 2
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 29    1100 330    2 true 3.0  45 33   1 timeout 900   11000 5200 0 timeout 900   11000 5100 0 true 6.2 290 52 2 true 550    290 8100   2 true .54 37 6.0 2 true 1.4   50 18    2 timeout 960   9400 10000 0 true .36 19 4.9 2 timeout 900   13000 7400 0 timeout 900   3600 13000 0 timeout 900   6200 12000 0 true 160 1700 1200 2
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 34    1200 320    2 true 3.1  46 37   1 timeout 900   11000 5200 0 timeout 910   11000 4800 0 true 5.8 290 43 2 true 550    300 7600   2 true .60 38 7.3 2 true 1.5   52 16    2 timeout 970   8300 9100 0 true .37 19 5.0 2 timeout 910   12000 7800 0 timeout 900   3300 11000 0 timeout 900   4700 11000 0 true 170 1700 1300 2
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 37    1600 350    2 true 3.1  46 39   1 timeout 900   11000 5000 0 timeout 910   11000 4300 0 true 6.0 290 48 1 true 580    290 7200   2 true .54 38 5.9 2 true 1.7   60 21    2 timeout 960   8700 8100 0 true .38 19 5.3 2 timeout 910   14000 5700 0 timeout 900   3000 13000 0 timeout 900   4600 10000 0 true 170 1500 1300 2
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 37    1600 420    2 true 3.3  47 41   1 timeout 900   11000 5100 0 timeout 910   11000 4500 0 true 6.0 300 44 2 true 590    300 7800   2 true .74 38 11   2 true 2.0   61 26    2 timeout 970   8600 9100 0 true .40 20 4.7 2 timeout 910   14000 6900 0 timeout 900   2700 12000 0 timeout 900   4600 12000 0 true 160 1800 1400 2
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 21    710 180    2 true 1.6  42 18   1 timeout 900   11000 5000 0 timeout 900   11000 5900 0 true 5.3 280 43 2 true 440    280 5700   2 true .29 37 3.3 2 true 1.2   52 13    2 timeout 910   3800 12000 0 true .37 17 4.2 2 timeout 900   13000 5100 0 timeout 900   2900 12000 0 timeout 910   13000 6000 0 true 110 980 800 2
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 21    750 220    2 true 1.6  42 22   1 timeout 910   11000 5300 0 timeout 900   11000 5400 0 true 5.6 290 51 2 true 500    280 6200   2 true .30 37 3.4 2 true 1.3   54 14    2 timeout 920   5000 14000 0 true .37 17 4.0 2 timeout 900   13000 5900 0 timeout 900   4500 13000 0 timeout 900   6700 13000 0 true 120 1000 890 2
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 22    750 200    2 true 1.5  42 16   1 timeout 910   11000 5700 0 timeout 900   11000 5600 0 true 5.3 280 42 2 true 500    280 6700   2 true .31 37 3.1 2 true 1.3   56 16    2 timeout 910   3800 13000 0 true .35 18 4.3 2 timeout 900   14000 4700 0 timeout 900   3400 9600 0 timeout 910   13000 5500 0 true 110 1000 720 2
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 22    790 240    2 true 1.7  43 18   1 timeout 900   11000 5500 0 timeout 900   11000 4900 0 true 5.3 290 39 2 true 500    280 5900   2 true .35 37 3.4 2 true 1.4   56 15    2 timeout 920   5000 14000 0 true .36 18 4.5 2 timeout 900   13000 5600 0 timeout 900   3700 12000 0 timeout 900   6300 12000 0 true 120 1100 930 2
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 23    780 260    2 true 1.6  42 16   1 timeout 900   11000 5300 0 timeout 910   11000 5800 0 true 5.8 280 45 2 true 480    270 6400   2 true .30 37 3.0 2 true 1.2   53 15    2 timeout 900   3800 13000 0 true .35 18 4.8 2 timeout 900   14000 5200 0 timeout 900   3200 11000 0 timeout 910   14000 6000 0 true 110 1000 810 2
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 26    830 250    2 true 1.6  43 20   1 timeout 900   11000 5500 0 timeout 910   11000 5000 0 true 5.2 280 50 2 true 500    290 7000   2 true .32 37 3.3 2 true 1.3   55 17    2 timeout 900   3600 11000 0 true .36 18 4.3 2 timeout 910   12000 6300 0 timeout 900   5300 11000 0 timeout 900   5900 11000 0 true 120 1100 790 2
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 24    1100 280    2 true 1.6  43 18   1 timeout 900   11000 5000 0 timeout 910   11000 4700 0 true 5.3 280 45 2 true 510    280 6800   2 true .31 37 3.0 2 true 1.6   59 18    2 timeout 900   3400 11000 0 true .37 18 4.3 2 timeout 910   14000 5600 0 timeout 900   3400 11000 0 timeout 900   8600 8500 0 true 130 1200 1000 2
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 29    1100 240    2 true 1.7  43 16   1 timeout 900   11000 5700 0 timeout 900   11000 5800 0 true 5.5 280 44 2 true 510    280 6300   2 true .32 38 3.5 2 true 1.7   61 19    2 timeout 900   3700 13000 0 true .39 19 3.9 2 timeout 910   13000 6800 0 timeout 900   2400 11000 0 timeout 900   4700 11000 0 true 120 1200 910 2
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 25    810 220    2 true 1.6  42 18   1 timeout 900   11000 5100 0 timeout 900   11000 4500 0 true 5.3 280 40 2 true 500    280 5200   2 true .29 37 3.5 2 true 1.4   56 15    2 timeout 900   3700 11000 0 true .37 18 4.4 2 timeout 910   14000 5000 0 timeout 900   3700 13000 0 timeout 900   13000 5500 0 true 110 1000 860 2
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 27    860 230    2 true 1.7  43 17   1 timeout 900   11000 5900 0 timeout 910   11000 4800 0 true 5.9 290 43 2 true 510    290 6600   2 true .34 37 3.7 2 true 1.5   58 18    2 timeout 900   3100 14000 0 true .38 19 4.4 2 timeout 910   13000 6200 0 timeout 900   3100 14000 0 timeout 900   6200 11000 0 true 120 1100 910 2
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 28    1100 220    2 true 1.7  43 17   1 timeout 900   11000 5100 0 timeout 900   11000 5000 0 true 5.6 280 38 2 true 510    280 6300   2 true .31 38 3.3 2 true 1.7   62 20    2 timeout 900   3700 14000 0 true .39 19 5.1 2 timeout 900   14000 5100 0 timeout 900   3000 14000 0 timeout 900   12000 7500 0 true 130 1200 890 2
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 30    1200 260    2 true 1.8  43 18   1 timeout 900   11000 5100 0 timeout 910   11000 6000 0 true 5.6 280 46 2 true 510    290 5400   2 true .31 38 3.9 2 true 1.8   64 21    2 timeout 900   3700 11000 0 true .40 19 4.5 2 timeout 900   12000 6400 0 timeout 900   5300 13000 0 timeout 900   6000 12000 0 true 130 1300 940 2
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 3.1  630 31    2 true 3.5  47 40   1 timeout 910   9800 7600 0 timeout 910   11000 5300 0 true 5.9 290 48 2 true 490    300 5900   2 true .97 37 11   2 true .81  45 10    2 timeout 940   7000 11000 0 true .38 19 4.2 2 timeout 910   14000 5900 0 timeout 900   2700 10000 0 timeout 900   6500 11000 0 true 93 750 640 2
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 3.3  680 31    2 true 3.5  47 40   1 timeout 910   9400 7500 0 timeout 910   11000 5100 0 true 5.9 290 45 2 true 490    330 6000   2 true .89 37 12   2 true .90  49 9.9  2 timeout 940   6900 10000 0 true .36 20 4.5 2 timeout 900   13000 4800 0 timeout 900   2800 12000 0 timeout 900   13000 5600 0 true 100 770 780 2
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 3.4  730 34    2 true 3.5  47 37   1 timeout 900   9400 8100 0 timeout 910   11000 4900 0 true 6.2 290 50 2 true 490    300 6300   2 true .97 37 11   2 true .87  47 11    2 timeout 970   7200 9800 0 true .39 20 4.2 2 timeout 900   14000 5300 0 timeout 900   1900 10000 0 timeout 900   6600 11000 0 true 95 780 700 2
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 6.4  1400 61    2 true 3.6  47 41   1 timeout 900   9200 8100 0 timeout 900   11000 7700 0 true 6.1 290 53 2 true 490    360 5000   2 true 1.1  37 13   2 true 1.4   60 17    2 timeout 930   7600 10000 0 true .39 20 4.3 2 timeout 900   13000 5900 0 timeout 900   5300 13000 0 timeout 910   13000 6600 0 true 100 860 800 2
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 5.5  1200 50    2 true 3.9  50 42   1 timeout 900   8300 8600 0 timeout 910   11000 6700 0 true 6.2 290 49 2 true 490    610 6300   2 true 1.1  38 15   2 true 1.2   55 13    2 timeout 940   6800 9800 0 true .36 20 4.9 2 timeout 910   13000 4800 0 timeout 900   2600 12000 0 timeout 900   8400 11000 0 true 110 840 780 2
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 11    2300 120    2 true 4.0  49 46   1 timeout 910   9300 7600 0 timeout 910   11000 7600 0 true 6.2 290 55 2 true 500    460 4300   2 true 1.3  38 14   2 true 2.0   75 24    2 timeout 940   6900 9500 0 true .37 21 4.5 2 timeout 910   14000 6200 0 timeout 900   2300 13000 0 timeout 900   9600 8900 0 true 110 1000 790 2
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 3.6  770 34    2 true 3.6  47 44   1 timeout 910   9400 8400 0 timeout 900   11000 6800 0 true 6.0 290 51 2 true 490    330 5900   2 true 1.0  37 13   2 true .93  50 9.8  2 timeout 940   7900 11000 0 true .36 20 4.5 2 timeout 910   14000 6800 0 timeout 900   3300 12000 0 timeout 900   7000 11000 0 true 95 770 700 2
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 6.8  1500 63    2 true 3.6  48 50   1 timeout 910   9200 8900 0 timeout 900   11000 7100 0 true 6.1 290 55 2 true 490    400 5700   2 true 1.1  38 13   2 true 1.6   65 20    2 timeout 940   7000 10000 0 true .39 21 4.4 2 timeout 900   13000 6200 0 timeout 900   5200 14000 0 timeout 900   6400 10000 0 true 110 920 740 2
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 5.7  1200 57    2 true 3.9  50 47   1 timeout 900   8300 7900 0 timeout 900   11000 6200 0 true 6.4 290 48 2 true 490    320 6300   2 true 1.1  38 14   2 true 1.4   58 16    2 timeout 960   7300 12000 0 true .39 21 5.0 2 timeout 910   13000 5300 0 timeout 900   3600 13000 0 timeout 900   8400 9800 0 true 100 830 810 2
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 12    2400 120    2 true 4.0  50 52   1 timeout 900   9300 8200 0 timeout 910   11000 6500 0 true 6.6 290 57 2 true 500    520 5400   2 true 1.2  38 19   2 true 2.2   79 29    2 timeout 940   6900 11000 0 true .38 22 4.6 2 timeout 910   13000 6800 0 timeout 900   5300 11000 0 timeout 900   4600 11000 0 true 110 1000 830 2
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 22    750 220    2 true 1.5  42 18   1 timeout 910   11000 5800 0 timeout 900   11000 5100 0 true 5.4 280 40 2 true 500    280 7400   2 true .29 37 2.9 2 true 1.3   55 16    2 timeout 900   4000 11000 0 true .38 18 4.1 2 timeout 910   13000 5400 0 timeout 900   3500 13000 0 timeout 910   13000 5800 0 true 350 1000 2000 2
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 22    780 190    2 true 1.7  44 17   1 timeout 900   11000 6700 0 timeout 910   11000 5100 0 true 5.6 280 46 2 true 500    280 7300   2 true .35 37 3.5 2 true 1.5   56 17    2 timeout 910   4600 10000 0 true .38 19 4.1 2 timeout 910   14000 5400 0 timeout 900   2800 11000 0 timeout 910   14000 5200 0 true 340 1100 2000 2
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 22    810 320    2 true 1.6  42 19   1 timeout 900   11000 6200 0 timeout 910   11000 5500 0 true 5.3 280 44 2 true 500    280 6200   2 true .31 37 3.5 2 true 1.3   55 16    2 timeout 910   4100 12000 0 true .38 18 4.1 2 timeout 910   14000 5300 0 timeout 900   2900 12000 0 timeout 910   13000 6900 0 true 350 1100 2300 2
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 24    860 210    2 true 1.7  43 18   1 timeout 910   11000 6000 0 timeout 910   11000 5000 0 true 5.6 280 49 2 true 510    290 6100   2 true .37 37 3.9 2 true 1.5   57 19    2 timeout 930   4900 13000 0 true .39 19 4.2 2 timeout 910   14000 5300 0 timeout 900   3200 14000 0 timeout 910   14000 5300 0 true 360 1100 2000 2
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 28    1100 280    2 true 1.7  43 16   1 timeout 900   11000 5100 0 timeout 910   11000 5100 0 true 5.4 290 40 2 true 510    280 6800   2 true .29 38 3.1 2 true 1.7   64 19    2 timeout 910   4500 10000 0 true .36 19 4.2 2 timeout 900   14000 6500 0 timeout 900   3700 11000 0 timeout 910   13000 6000 0 true 350 1200 2200 2
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 33    1200 320    2 true 1.8  43 17   1 timeout 900   11000 6700 0 timeout 910   11000 4300 0 true 5.4 280 51 2 true 510    280 6800   2 true .31 38 3.7 2 true 1.8   65 22    2 timeout 960   7000 11000 0 true .39 20 4.8 2 timeout 910   14000 5300 0 timeout 900   2300 14000 0 timeout 910   14000 5300 0 true 360 1300 2200 2
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 21    290 190    1 false(unreach-call) 3.1  55 25   0 false(unreach-call) 130   5500 1100 1 timeout 900   5300 7000 0 false(unreach-call) 14   510 110 1 false(unreach-call) 490    170 6100   0 false(unreach-call) 2.7  41 24   1 false(unreach-call) 2.8   41 27    1 timeout 900   4800 9600 0 false(unreach-call) .39 15 4.5 1 timeout 900   10000 7300 0 timeout 900   4400 12000 0 timeout 900   6000 11000 0 unknown 500 3800 5500 0
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 37    500 300    1 false(unreach-call) 4.5  64 70   0 timeout 900   11000 5200 0 timeout 900   6600 8700 0 false(unreach-call) 12   490 97 1 false(unreach-call) 500    300 6300   0 false(unreach-call) 3.8  50 44   1 false(unreach-call) 4.3   52 43    1 timeout 900   4800 12000 0 false(unreach-call) .40 17 4.6 1 timeout 900   11000 6900 0 timeout 900   4200 13000 0 timeout 900   5400 12000 0 unknown 530 3900 5900 0
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 26    310 190    1 false(unreach-call) 3.1  56 32   1 false(unreach-call) 210   6600 1500 1 timeout 900   9200 8000 0 false(unreach-call) 14   510 130 1 false(unreach-call) 490    190 4700   0 false(unreach-call) 2.6  43 28   1 false(unreach-call) 3.2   43 34    1 timeout 900   4600 12000 0 false(unreach-call) .39 16 4.7 1 timeout 900   12000 6100 0 timeout 900   6200 11000 0 timeout 910   13000 5700 0 unknown 500 3900 5900 0
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 42    540 550    1 false(unreach-call) 5.0  65 57   0 timeout 910   11000 6300 0 timeout 900   9000 8300 0 false(unreach-call) 14   520 120 1 false(unreach-call) 500    490 5600   0 false(unreach-call) 5.0  54 46   1 false(unreach-call) 4.6   54 46    1 timeout 900   4700 11000 0 false(unreach-call) .42 18 4.8 1 timeout 900   13000 7300 0 timeout 900   5400 13000 0 timeout 910   12000 7500 0 unknown 520 4000 5500 0
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 20    320 210    1 false(unreach-call) 3.4  57 37   0 timeout 910   11000 5200 0 timeout 900   6200 9900 0 false(unreach-call) 15   530 140 1 false(unreach-call) 490    180 5300   0 false(unreach-call) 2.7  43 29   1 false(unreach-call) 3.0   43 30    1 timeout 900   5600 11000 0 false(unreach-call) .41 17 4.6 1 timeout 910   14000 6800 0 timeout 900   4100 12000 0 timeout 900   6200 12000 0 unknown 510 3800 5800 0
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 25    350 210    1 false(unreach-call) 3.6  60 41   0 timeout 910   11000 5900 0 timeout 900   10000 7500 0 false(unreach-call) 14   520 130 1 false(unreach-call) 490    160 4900   0 false(unreach-call) 2.8  45 29   1 false(unreach-call) 3.5   45 37    1 timeout 900   5500 9200 0 false(unreach-call) .42 18 5.3 1 timeout 900   14000 6500 0 timeout 900   5500 12000 0 timeout 900   5400 12000 0 unknown 510 3800 5800 0
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 37    590 430    1 false(unreach-call) 6.0  76 64   0 timeout 900   11000 6100 0 timeout 900   8400 7600 0 false(unreach-call) 15   530 140 1 false(unreach-call) 500    230 6400   0 false(unreach-call) 4.1  56 45   1 false(unreach-call) 4.3   57 59    1 timeout 900   5400 12000 0 false(unreach-call) .40 19 4.8 1 timeout 900   13000 6700 0 timeout 900   4500 12000 0 timeout 900   5800 12000 0 unknown 540 3900 5600 0
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 48    670 450    1 false(unreach-call) 6.4  77 73   1 timeout 910   11000 6000 0 timeout 910   10000 6800 0 false(unreach-call) 18   800 140 1 false(unreach-call) 500    220 4800   0 false(unreach-call) 4.8  58 49   1 false(unreach-call) 5.2   59 54    1 timeout 900   5600 11000 0 false(unreach-call) .45 20 5.0 1 timeout 900   13000 7300 0 timeout 900   5000 11000 0 timeout 900   4800 13000 0 unknown 550 4000 6200 0
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 200    8000 1300    1 error (42) 870    1800 5200   0 timeout 900   11000 8200 0 timeout 900   10000 7600 0 false(unreach-call) 560   6200 6800 1 unknown 890    1600 12000   0 false(unreach-call) 48    440 560   1 false(unreach-call) 65     470 730    1 timeout 910   5900 11000 0 false(unreach-call) 1.2  38 15   1 timeout 900   13000 5000 0 timeout 910   6500 13000 0 timeout 900   4600 11000 0 timeout 900 2500 6300 0
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 19    270 240    1 false(unreach-call) 3.0  56 34   0 timeout 900   11000 5600 0 timeout 900   8200 8800 0 false(unreach-call) 12   480 110 1 false(unreach-call) 490    140 5700   0 false(unreach-call) 2.4  41 23   1 false(unreach-call) 2.5   40 31    1 timeout 900   4300 13000 0 false(unreach-call) .37 15 3.9 1 timeout 900   12000 7300 0 timeout 900   6200 12000 0 timeout 900   6600 9600 0 unknown 500 3800 6100 0
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 41    460 400    1 false(unreach-call) 4.1  63 42   1 timeout 910   11000 6200 0 timeout 900   7400 11000 0 false(unreach-call) 11   430 99 1 false(unreach-call) 490    320 5700   0 false(unreach-call) 4.0  49 45   1 false(unreach-call) 3.4   51 35    1 timeout 900   4500 10000 0 false(unreach-call) .37 17 5.2 1 timeout 900   13000 6800 0 timeout 900   4500 14000 0 timeout 900   5400 12000 0 unknown 510 3900 6800 0
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 21    310 210    1 false(unreach-call) 3.1  56 31   0 false(unreach-call) 580   9900 4200 1 timeout 900   8900 9300 0 false(unreach-call) 12   480 98 1 false(unreach-call) 490    270 6300   0 false(unreach-call) 2.6  43 28   1 false(unreach-call) 3.0   43 30    1 timeout 900   4500 12000 0 false(unreach-call) .39 16 4.5 1 timeout 900   12000 7400 0 timeout 900   3500 13000 0 timeout 900   6000 11000 0 unknown 500 3900 5300 0
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 43    540 370    1 false(unreach-call) 4.9  65 54   1 timeout 900   11000 5400 0 timeout 910   11000 9500 0 false(unreach-call) 13   490 100 1 false(unreach-call) 500    190 5900   0 false(unreach-call) 3.9  53 40   1 false(unreach-call) 4.3   54 62    1 timeout 900   4500 11000 0 false(unreach-call) .38 18 4.4 1 timeout 900   12000 8200 0 timeout 900   3400 14000 0 timeout 900   5300 13000 0 unknown 530 3900 5700 0
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 23    300 190    1 false(unreach-call) 3.2  57 41   0 false(unreach-call) 240   6900 1700 1 timeout 900   6700 12000 0 false(unreach-call) 12   480 100 1 false(unreach-call) 490    200 6200   0 false(unreach-call) 2.6  43 24   1 false(unreach-call) 2.8   43 24    1 timeout 900   4400 12000 0 false(unreach-call) .37 16 4.7 1 timeout 900   11000 8100 0 timeout 900   6300 12000 0 timeout 900   7600 11000 0 unknown 510 3800 5700 0
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 39    520 370    1 false(unreach-call) 5.3  70 62   1 timeout 900   11000 5300 0 timeout 900   8600 11000 0 false(unreach-call) 13   510 100 1 false(unreach-call) 500    210 5400   0 false(unreach-call) 4.6  54 46   1 false(unreach-call) 3.7   55 42    1 timeout 900   4700 9900 0 false(unreach-call) .39 18 5.4 1 timeout 900   14000 6500 0 timeout 900   4500 11000 0 timeout 900   6700 9900 0 unknown 540 3900 5100 0
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 22    350 210    1 false(unreach-call) 3.5  58 38   1 timeout 910   11000 5200 0 timeout 900   8600 8500 0 false(unreach-call) 12   480 110 1 false(unreach-call) 490    180 5600   0 false(unreach-call) 2.8  45 28   1 false(unreach-call) 3.0   45 33    1 timeout 900   4800 11000 0 false(unreach-call) .38 18 5.2 1 timeout 910   14000 6200 0 timeout 900   4400 13000 0 timeout 900   6800 12000 0 unknown 510 3900 5400 0
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 46    640 420    1 false(unreach-call) 6.5  77 77   0 timeout 910   11000 5300 0 timeout 900   10000 8800 0 false(unreach-call) 12   480 99 1 false(unreach-call) 500    310 5100   0 false(unreach-call) 4.3  58 48   1 false(unreach-call) 5.0   59 67    1 timeout 900   4900 10000 0 false(unreach-call) .41 20 5.3 1 timeout 910   13000 7100 0 timeout 900   6000 14000 0 timeout 900   6000 9700 0 unknown 550 3900 6600 0
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 280    8500 1400    1 error (42) 870    2200 5000   0 timeout 910   8600 10000 0 timeout 910   11000 6800 0 false(unreach-call) 550   6300 5500 1 unknown 890    1600 8700   0 false(unreach-call) 56    490 630   1 false(unreach-call) 75     520 830    1 timeout 910   5900 11000 0 false(unreach-call) .72 25 9.0 1 timeout 910   14000 6800 0 timeout 900   6600 11000 0 timeout 900   13000 6200 0 timeout 900 2500 5700 0
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 31    390 290    1 false(unreach-call) 2.8  55 37   0 timeout 900   8000 9100 0 timeout 910   7300 9500 0 false(unreach-call) 14   530 110 1 false(unreach-call) 490    200 5400   0 false(unreach-call) 2.9  39 26   1 false(unreach-call) 3.6   42 35    1 timeout 900   5000 11000 0 false(unreach-call) .39 16 5.4 1 timeout 900   13000 5600 0 timeout 900   6200 12000 0 timeout 900   9900 8600 0 unknown 500 3900 4900 0
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 23    250 180    1 false(unreach-call) 2.8  54 29   0 false(unreach-call) 83   4200 640 1 timeout 900   9800 7600 0 false(unreach-call) 12   450 100 1 false(unreach-call) 490    210 5800   0 false(unreach-call) 2.6  37 29   1 false(unreach-call) 3.5   40 29    1 timeout 900   4900 12000 0 false(unreach-call) .49 17 5.4 1 timeout 910   12000 8000 0 timeout 900   7000 12000 0 timeout 900   5700 12000 0 unknown 510 3800 5800 0
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 23    270 180    1 false(unreach-call) 3.0  54 35   0 timeout 900   11000 5900 0 timeout 900   9900 6700 0 false(unreach-call) 13   480 110 1 false(unreach-call) 490    160 5400   0 false(unreach-call) 2.9  37 27   1 false(unreach-call) 3.6   41 34    1 timeout 900   5600 10000 0 false(unreach-call) .42 15 5.0 1 timeout 910   13000 9400 0 timeout 900   6600 11000 0 timeout 900   5700 12000 0 unknown 500 3800 5200 0
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 41    440 320    1 false(unreach-call) 4.1  61 46   0 false(unreach-call) 430   9500 3300 1 timeout 900   6400 10000 0 false(unreach-call) 14   510 100 1 false(unreach-call) 490    180 6300   0 false(unreach-call) 2.9  45 25   1 false(unreach-call) 4.6   49 42    1 timeout 900   4900 11000 0 false(unreach-call) .44 17 4.8 1 timeout 900   11000 7400 0 timeout 900   6100 13000 0 timeout 900   8400 10000 0 unknown 520 3900 6600 0
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 42    480 350    1 false(unreach-call) 4.6  63 50   1 timeout 910   11000 5600 0 timeout 900   6100 11000 0 false(unreach-call) 17   790 160 1 false(unreach-call) 490    170 5400   0 false(unreach-call) 3.1  46 32   1 false(unreach-call) 4.6   52 44    1 timeout 910   5700 11000 0 false(unreach-call) .40 17 4.7 1 timeout 900   11000 7800 0 timeout 900   6400 13000 0 timeout 900   9200 11000 0 unknown 530 3900 6100 0
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 25    290 210    1 false(unreach-call) 3.1  56 32   1 timeout 900   8200 9200 0 timeout 900   10000 7100 0 false(unreach-call) 12   490 110 1 false(unreach-call) 490    300 5400   0 false(unreach-call) 3.0  39 25   1 false(unreach-call) 3.9   43 36    1 timeout 900   4900 11000 0 false(unreach-call) .45 16 4.9 1 timeout 900   12000 8400 0 timeout 900   6800 10000 0 timeout 900   5500 11000 0 unknown 500 3900 6200 0
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 44    520 400    1 false(unreach-call) 4.9  64 62   1 timeout 910   11000 4700 0 timeout 900   5500 10000 0 false(unreach-call) 14   530 130 1 false(unreach-call) 490    320 5000   0 false(unreach-call) 3.4  48 31   1 false(unreach-call) 5.4   54 55    1 timeout 900   4800 12000 0 false(unreach-call) .43 18 5.3 1 timeout 900   12000 7300 0 timeout 900   6200 13000 0 timeout 900   9700 8000 0 unknown 520 3900 6500 0
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 33    460 280    1 false(unreach-call) 3.3  56 42   1 timeout 900   8200 9500 0 timeout 900   6000 9600 0 false(unreach-call) 17   740 150 1 false(unreach-call) 490    200 5500   0 false(unreach-call) 2.8  41 24   1 false(unreach-call) 3.1   45 44    1 timeout 900   5500 11000 0 false(unreach-call) .43 17 5.2 1 timeout 910   13000 7000 0 timeout 900   6300 12000 0 timeout 900   9300 9600 0 unknown 510 3900 5700 0
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 21    300 240    1 false(unreach-call) 3.2  54 33   1 false(unreach-call) 160   5700 1300 1 timeout 900   8800 9800 0 false(unreach-call) 17   800 150 1 false(unreach-call) 490    210 5600   0 false(unreach-call) 2.6  39 21   1 false(unreach-call) 3.5   43 33    1 timeout 930   5700 12000 0 false(unreach-call) .48 17 6.4 1 timeout 900   11000 7800 0 timeout 900   6400 12000 0 timeout 900   7400 11000 0 unknown 500 3800 5300 0
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 22    310 260    1 false(unreach-call) 3.4  56 41   0 false(unreach-call) 240   6800 1700 1 timeout 900   9400 7900 0 false(unreach-call) 22   900 230 1 false(unreach-call) 490    140 5800   0 false(unreach-call) 2.9  39 25   1 false(unreach-call) 3.6   43 36    1 timeout 910   5900 11000 0 false(unreach-call) .44 17 4.5 1 timeout 900   11000 6900 0 timeout 900   6200 15000 0 timeout 910   10000 9700 0 unknown 510 3800 5400 0
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 39    500 330    1 false(unreach-call) 5.2  67 60   0 timeout 910   8300 9400 0 timeout 900   7200 9200 0 false(unreach-call) 15   540 120 1 false(unreach-call) 490    320 5500   0 false(unreach-call) 2.9  48 31   1 false(unreach-call) 5.0   55 51    1 timeout 900   5500 11000 0 false(unreach-call) .44 18 5.5 1 timeout 900   11000 7400 0 timeout 900   6100 13000 0 timeout 900   10000 10000 0 unknown 530 3900 5700 0
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 25    340 270    1 false(unreach-call) 3.6  56 41   1 false(unreach-call) 320   8000 2400 1 timeout 910   9800 6600 0 false(unreach-call) 19   810 170 1 false(unreach-call) 490    360 6700   0 false(unreach-call) 2.9  41 29   1 false(unreach-call) 4.0   45 37    1 timeout 900   5600 13000 0 false(unreach-call) .48 18 5.0 1 timeout 910   13000 5700 0 timeout 900   6600 12000 0 timeout 900   12000 9000 0 unknown 510 3900 5800 0
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 40    570 340    1 false(unreach-call) 6.0  72 66   0 timeout 910   11000 6500 0 timeout 900   8900 8500 0 false(unreach-call) 16   580 160 1 false(unreach-call) 490    220 5600   0 false(unreach-call) 3.3  49 33   1 false(unreach-call) 4.9   55 48    1 timeout 910   5900 10000 0 false(unreach-call) .43 19 4.9 1 timeout 900   13000 7800 0 timeout 900   6100 13000 0 timeout 900   9800 9100 0 unknown 540 3900 5800 0
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 45    620 360    1 false(unreach-call) 6.4  74 94   0 timeout 900   11000 5600 0 timeout 900   7200 9200 0 false(unreach-call) 16   580 150 1 false(unreach-call) 490    240 6100   0 false(unreach-call) 3.3  52 39   1 false(unreach-call) 6.0   59 57    1 timeout 930   5900 10000 0 false(unreach-call) .47 20 7.1 1 timeout 910   14000 5800 0 timeout 900   6100 14000 0 timeout 900   11000 9000 0 unknown 550 4000 6500 0
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 140    7600 1100    1 false(unreach-call) 130    640 1700   1 timeout 900   8900 8300 0 timeout 900   7800 9900 0 false(unreach-call) 17   730 140 1 false(unreach-call) 620    1600 6400   0 false(unreach-call) 9.8  170 120   1 false(unreach-call) 28     210 300    1 timeout 910   6400 10000 0 false(unreach-call) 1.3  41 15   1 timeout 910   13000 6100 0 timeout 900   6300 11000 0 timeout 900   5100 13000 0 timeout 900 4500 8100 0
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 32    400 280    1 false(unreach-call) 3.1  57 34   1 false(unreach-call) 350   8300 2500 1 timeout 900   8000 8800 0 false(unreach-call) 18   800 160 1 false(unreach-call) 490    350 5700   0 false(unreach-call) 3.6  40 31   1 false(unreach-call) 4.2   43 45    1 timeout 900   4500 14000 0 false(unreach-call) .55 19 6.3 1 timeout 910   13000 5700 0 timeout 900   3500 13000 0 timeout 900   5200 11000 0 unknown 510 3900 5500 0
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 23    260 180    1 false(unreach-call) 3.0  55 34   1 false(unreach-call) 350   7800 2400 1 timeout 900   7000 8800 0 false(unreach-call) 15   540 130 1 false(unreach-call) 490    170 5000   0 false(unreach-call) 3.0  38 37   1 false(unreach-call) 4.0   41 45    1 timeout 900   4300 13000 0 false(unreach-call) .57 20 6.8 1 timeout 900   13000 8800 0 timeout 900   5500 12000 0 timeout 900   6200 11000 0 unknown 500 3800 6200 0
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 19    280 190    1 false(unreach-call) 3.1  57 34   1 false(unreach-call) 320   8200 2500 1 timeout 910   11000 8800 0 false(unreach-call) 18   810 170 1 false(unreach-call) 490    170 5500   0 false(unreach-call) 3.9  38 32   1 false(unreach-call) 4.3   41 38    1 timeout 900   4700 13000 0 false(unreach-call) .43 16 5.2 1 timeout 910   13000 8300 0 timeout 900   3500 13000 0 timeout 900   5400 11000 0 unknown 510 3800 5300 0
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 44    450 370    1 false(unreach-call) 4.4  63 46   0 timeout 910   11000 5500 0 timeout 900   8100 9600 0 false(unreach-call) 14   520 120 1 false(unreach-call) 490    300 6200   0 false(unreach-call) 3.8  46 39   1 false(unreach-call) 5.3   51 49    1 timeout 900   4400 12000 0 false(unreach-call) .58 20 8.1 1 timeout 900   12000 8500 0 timeout 900   2700 12000 0 timeout 900   5400 12000 0 unknown 520 3900 5600 0
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 23    300 200    1 false(unreach-call) 3.2  57 35   1 timeout 910   11000 5100 0 timeout 900   11000 8400 0 false(unreach-call) 16   550 110 1 false(unreach-call) 490    230 4700   0 false(unreach-call) 3.7  40 38   1 false(unreach-call) 4.6   44 42    1 timeout 900   4400 12000 0 false(unreach-call) .44 17 5.8 1 timeout 900   12000 8100 0 timeout 900   4700 12000 0 timeout 900   5900 12000 0 unknown 510 3800 5500 0
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 33    480 330    1 false(unreach-call) 4.9  66 59   1 timeout 910   11000 4800 0 timeout 900   5400 11000 0 false(unreach-call) 17   810 150 1 false(unreach-call) 490    230 5400   0 false(unreach-call) 3.9  47 47   1 false(unreach-call) 5.1   52 54    1 timeout 900   4500 11000 0 false(unreach-call) .43 18 5.1 1 timeout 910   13000 4900 0 timeout 900   4800 12000 0 timeout 900   6200 10000 0 unknown 530 3900 5500 0
email_spec27_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 48    530 360    1 false(unreach-call) 5.3  68 57   0 timeout 900   11000 5400 0 timeout 900   8900 10000 0 false(unreach-call) 14   510 110 1 false(unreach-call) 490    180 5900   0 false(unreach-call) 4.3  49 37   1 false(unreach-call) 6.1   55 62    1 timeout 900   4400 11000 0 false(unreach-call) .47 18 5.6 1 timeout 910   13000 6000 0 timeout 900   3200 14000 0 timeout 900   4600 10000 0 unknown 540 4000 6500 0
email_spec27_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 34    470 310    1 false(unreach-call) 3.4  59 42   0 false(unreach-call) 160   5600 1300 1 timeout 900   9400 8500 0 false(unreach-call) 22   900 220 1 false(unreach-call) 490    330 5400   0 false(unreach-call) 4.4  42 50   1 false(unreach-call) 6.5   46 49    1 timeout 900   4500 11000 0 false(unreach-call) .63 20 8.4 1 timeout 900   12000 8200 0 timeout 900   3500 14000 0 timeout 900   4700 11000 0 unknown 510 3900 5300 0
email_spec27_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 20    290 190    1 false(unreach-call) 3.4  58 36   0 false(unreach-call) 240   6800 1500 1 timeout 910   7500 11000 0 false(unreach-call) 21   880 190 1 false(unreach-call) 490    390 5200   0 false(unreach-call) 4.7  40 41   1 false(unreach-call) 6.0   44 42    1 timeout 900   4400 12000 0 false(unreach-call) .63 22 7.1 1 timeout 910   13000 6700 0 timeout 900   6200 13000 0 timeout 900   6000 11000 0 unknown 510 3800 6300 0
email_spec27_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 23    310 190    1 false(unreach-call) 3.5  58 44   0 false(unreach-call) 200   6600 1600 1 timeout 900   7500 10000 0 false(unreach-call) 27   1500 250 1 false(unreach-call) 490    150 5900   0 false(unreach-call) 4.6  40 38   1 false(unreach-call) 6.2   44 42    1 timeout 900   4500 11000 0 false(unreach-call) .43 17 5.9 1 timeout 900   13000 6900 0 timeout 900   6100 13000 0 timeout 900   6000 10000 0 unknown 510 3800 5400 0
email_spec27_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 40    520 350    1 false(unreach-call) 5.6  72 62   0 false(unreach-call) 520   10000 4200 1 timeout 900   6400 11000 0 false(unreach-call) 16   610 150 1 false(unreach-call) 490    320 5400   0 false(unreach-call) 5.4  50 48   1 false(unreach-call) 6.8   58 70    1 timeout 900   4600 11000 0 false(unreach-call) .65 23 8.6 1 timeout 900   13000 7600 0 timeout 900   5600 14000 0 timeout 900   4600 10000 0 unknown 530 3900 7400 0
email_spec27_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 24    330 240    1 false(unreach-call) 3.7  59 43   0 false(unreach-call) 330   8700 2500 1 timeout 900   9800 8200 0 false(unreach-call) 22   910 200 1 false(unreach-call) 490    150 5700   0 false(unreach-call) 4.7  42 42   1 false(unreach-call) 5.5   46 46    1 timeout 900   5200 10000 0 false(unreach-call) .48 18 6.9 1 timeout 910   13000 6900 0 timeout 900   5500 13000 0 timeout 900   6100 11000 0 unknown 510 3900 5000 0
email_spec27_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 41    590 390    1 false(unreach-call) 6.4  76 71   1 timeout 910   11000 5800 0 timeout 900   7400 8700 0 false(unreach-call) 20   820 160 1 false(unreach-call) 490    230 5500   0 false(unreach-call) 5.0  53 45   1 false(unreach-call) 7.5   60 73    1 timeout 900   4500 13000 0 false(unreach-call) .49 19 5.3 1 timeout 910   11000 6900 0 timeout 900   4900 14000 0 timeout 900   4600 12000 0 unknown 540 3900 6600 0
email_spec27_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 44    640 370    1 false(unreach-call) 6.9  79 80   0 timeout 910   11000 5500 0 timeout 900   8200 8600 0 false(unreach-call) 19   830 190 1 false(unreach-call) 500    220 5700   0 false(unreach-call) 5.2  54 49   1 false(unreach-call) 8.0   65 81    1 timeout 900   5200 12000 0 false(unreach-call) .50 20 5.5 1 timeout 900   13000 6700 0 timeout 900   4500 12000 0 timeout 900   4600 12000 0 unknown 560 3900 5700 0
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 440    11000 2500    1 false(unreach-call) 340    920 2600   0 timeout 900   8400 9100 0 timeout 900   9700 9400 0 false(unreach-call) 22   920 190 1 false(unreach-call) 740    1500 8300   0 false(unreach-call) 15    260 160   1 false(unreach-call) 47     320 500    1 timeout 900   4700 11000 0 false(unreach-call) 1.7  54 21   1 timeout 900   13000 6400 0 timeout 900   6300 11000 0 timeout 900   4700 12000 0 timeout 900 2500 5700 0
email_spec3_product13_false-unreach-call_true-termination.cil.c false(unreach-call) .65 110 5.8  1 false(unreach-call) .84 45 8.4 1 false(unreach-call) 160   5700 1200 1 false(unreach-call) 12   500 110 0 false(unreach-call) 7.5 330 65 1 false(unreach-call) 480    260 5800   0 false(unreach-call) .74 36 6.1 1 false(unreach-call) 1.1   37 13    1 false(unreach-call) 890   8100 10000 1 false(unreach-call) .39 15 4.3 1 timeout 900   13000 7000 0 unknown 75   1200 870 0 timeout 900   6700 11000 0 unknown 500 3800 5500 0
email_spec3_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1.0  210 9.7  1 false(unreach-call) 1.0  50 12   1 false(unreach-call) 540   9600 4600 1 false(unreach-call) 15   650 110 0 false(unreach-call) 7.8 340 59 1 false(unreach-call) 480    220 6700   0 false(unreach-call) .86 37 7.3 1 false(unreach-call) 1.5   40 17    1 timeout 900   5600 12000 0 false(unreach-call) .38 16 4.5 1 timeout 910   13000 6400 0 unknown 84   1200 830 0 timeout 900   6300 12000 0 unknown 510 3900 5300 0
email_spec3_product18_false-unreach-call_true-termination.cil.c false(unreach-call) .73 120 6.7  1 false(unreach-call) .98 48 10   1 false(unreach-call) 150   5600 1200 1 false(unreach-call) 12   500 93 1 false(unreach-call) 7.9 340 61 1 false(unreach-call) 480    410 6200   0 false(unreach-call) .69 36 9.7 1 false(unreach-call) 1.3   38 12    1 timeout 910   5600 11000 0 false(unreach-call) .39 16 4.4 1 timeout 910   13000 7300 0 unknown 82   1200 790 0 timeout 900   6800 10000 0 unknown 510 3800 6000 0
email_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) .76 140 7.9  1 false(unreach-call) .99 49 10   1 false(unreach-call) 150   5600 1200 1 false(unreach-call) 12   500 84 0 false(unreach-call) 7.4 330 62 1 false(unreach-call) 480    140 6200   0 false(unreach-call) .74 36 9.0 1 false(unreach-call) 1.3   38 13    1 timeout 900   5800 9800 0 false(unreach-call) .39 16 4.3 1 timeout 910   8300 9100 0 unknown 85   1200 850 0 timeout 900   6300 10000 0 unknown 510 3800 5700 0
email_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1.1  230 11    1 false(unreach-call) 1.5  60 18   1 false(unreach-call) 570   9700 4800 1 false(unreach-call) 18   640 130 1 false(unreach-call) 7.5 330 69 1 false(unreach-call) 480    200 4600   0 false(unreach-call) .75 37 6.9 1 false(unreach-call) 1.8   45 18    1 timeout 910   5700 10000 0 false(unreach-call) .40 17 4.1 1 timeout 900   9200 8000 0 unknown 79   1100 810 0 timeout 900   6700 10000 0 unknown 530 3900 5400 0
email_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) .80 150 8.3  1 false(unreach-call) 1.1  49 11   1 false(unreach-call) 180   5800 1200 1 false(unreach-call) 12   480 95 1 false(unreach-call) 7.3 330 57 1 false(unreach-call) 480    150 5500   0 false(unreach-call) .76 37 8.6 1 false(unreach-call) 1.3   39 12    1 timeout 950   6800 11000 0 false(unreach-call) .38 17 4.8 1 timeout 910   13000 6900 0 unknown 85   1200 900 0 timeout 900   7100 10000 0 unknown 520 3900 6700 0
email_spec3_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1.3  280 13    1 false(unreach-call) 1.6  60 22   1 false(unreach-call) 670   10000 5100 1 false(unreach-call) 17   670 130 0 false(unreach-call) 7.7 340 60 1 false(unreach-call) 480    170 5600   0 false(unreach-call) .77 37 7.8 1 false(unreach-call) 1.6   46 21    1 timeout 940   6200 11000 0 false(unreach-call) .38 18 4.8 1 timeout 910   14000 7300 0 unknown 87   1200 980 0 timeout 900   5500 11000 0 unknown 540 3900 6100 0
email_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1.4  310 15    1 false(unreach-call) 1.7  60 19   1 false(unreach-call) 600   9700 5000 1 false(unreach-call) 16   640 140 1 false(unreach-call) 7.3 330 60 1 false(unreach-call) 480    220 4600   0 false(unreach-call) .73 38 7.7 1 false(unreach-call) 1.9   49 21    1 timeout 910   6000 9600 0 false(unreach-call) .42 19 4.7 1 timeout 900   13000 7000 0 unknown 85   1100 930 0 timeout 900   5700 12000 0 unknown 540 4000 6900 0
email_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) .77 130 7.2  1 false(unreach-call) .90 47 8.3 1 false(unreach-call) 470   9200 3200 1 false(unreach-call) 12   500 98 0 false(unreach-call) 7.7 340 60 1 false(unreach-call) 480    170 5100   0 false(unreach-call) .80 36 6.7 1 false(unreach-call) 1.2   38 11    1 timeout 910   5600 10000 0 false(unreach-call) .40 16 5.0 1 timeout 900   13000 7800 0 timeout 900   4700 12000 0 timeout 900   5200 12000 0 unknown 500 3800 5400 0
email_spec3_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1.2  270 13    1 false(unreach-call) 1.1  54 13   1 false(unreach-call) 150   5700 1100 1 false(unreach-call) 16   650 120 0 false(unreach-call) 7.9 340 65 1 false(unreach-call) 480    400 5200   0 false(unreach-call) .79 38 8.2 1 false(unreach-call) 1.5   41 14    1 timeout 930   6300 11000 0 false(unreach-call) .40 18 4.9 1 timeout 900   14000 5700 0 timeout 900   4500 12000 0 timeout 900   5000 11000 0 unknown 510 3900 6200 0
email_spec3_product30_false-unreach-call_true-termination.cil.c false(unreach-call) .81 150 7.4  1 false(unreach-call) 1.1  51 13   1 false(unreach-call) 560   11000 3700 1 false(unreach-call) 13   500 100 1 false(unreach-call) 7.9 340 58 1 false(unreach-call) 480    190 5400   0 false(unreach-call) .71 37 8.2 1 false(unreach-call) 1.3   39 13    1 timeout 910   5700 11000 0 false(unreach-call) .41 17 4.5 1 timeout 910   13000 7900 0 timeout 900   4500 11000 0 timeout 900   5800 11000 0 unknown 510 3800 6200 0
email_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) .89 170 9.2  1 false(unreach-call) 1.1  50 13   1 false(unreach-call) 410   8800 2700 1 false(unreach-call) 13   510 100 0 false(unreach-call) 8.0 340 70 1 false(unreach-call) 480    280 4600   0 false(unreach-call) .76 37 8.0 1 false(unreach-call) 1.3   39 13    1 timeout 910   6000 11000 0 false(unreach-call) .40 17 4.5 1 timeout 910   14000 7600 0 timeout 900   4000 14000 0 timeout 900   6000 11000 0 unknown 510 3800 5400 0
email_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1.4  310 12    1 false(unreach-call) 1.8  63 21   1 false(unreach-call) 170   5600 1300 1 false(unreach-call) 16   650 130 1 false(unreach-call) 8.3 350 65 1 false(unreach-call) 480    230 5500   0 false(unreach-call) .73 38 7.3 1 false(unreach-call) 1.9   48 18    1 timeout 960   5900 11000 0 false(unreach-call) .40 19 5.4 1 timeout 910   13000 6100 0 timeout 900   4600 13000 0 timeout 900   4600 9500 0 unknown 540 3900 5700 0
email_spec3_product33_false-unreach-call_true-termination.cil.c false(unreach-call) .93 180 8.5  1 false(unreach-call) 1.2  52 13   1 false(unreach-call) 420   8800 2900 1 false(unreach-call) 13   510 110 1 false(unreach-call) 7.9 340 73 1 false(unreach-call) 480    280 5100   0 false(unreach-call) .73 37 8.9 1 false(unreach-call) 1.3   41 15    1 timeout 910   6000 11000 0 false(unreach-call) .42 18 4.8 1 timeout 900   12000 7100 0 timeout 900   4400 13000 0 timeout 900   6100 11000 0 unknown 520 3900 5800 0
email_spec3_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1.6  380 17    1 false(unreach-call) 2.1  68 26   1 false(unreach-call) 170   5600 1300 1 false(unreach-call) 19   630 120 0 false(unreach-call) 8.0 340 69 1 false(unreach-call) 480    200 5000   0 false(unreach-call) .73 38 7.8 1 false(unreach-call) 1.7   50 19    1 timeout 910   5900 10000 0 false(unreach-call) .40 20 4.6 1 timeout 910   13000 7500 0 timeout 900   4900 14000 0 timeout 900   4600 11000 0 unknown 550 3900 5700 0
email_spec3_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1.8  410 18    1 false(unreach-call) 2.2  69 30   1 false(unreach-call) 180   5800 1400 1 false(unreach-call) 17   660 150 1 false(unreach-call) 8.3 350 74 1 false(unreach-call) 480    220 6600   0 false(unreach-call) .76 38 8.7 1 false(unreach-call) 2.0   52 20    1 timeout 910   6000 12000 0 false(unreach-call) .41 21 5.7 1 timeout 910   13000 6700 0 timeout 900   4300 12000 0 timeout 900   4700 10000 0 unknown 560 3900 6900 0
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 56    7900 400    1 false(unreach-call) 47    670 390   0 false(unreach-call) 780   11000 4300 1 false(unreach-call) 20   690 140 0 false(unreach-call) 8.0 350 72 1 false(unreach-call) 510    1600 5400   0 false(unreach-call) 2.9  45 26   1 false(unreach-call) 7.8   180 84    1 timeout 900   6400 11000 0 false(unreach-call) .60 25 7.8 1 timeout 900   9900 9700 0 timeout 900   5000 12000 0 timeout 900   4600 12000 0 timeout 900 10000 8100 0
email_spec4_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 20    260 190    1 false(unreach-call) 3.0  54 30   0 false(unreach-call) 470   9300 3000 1 false(unreach-call) 21   740 150 1 false(unreach-call) 11   480 99 1 false(unreach-call) 490    220 5600   0 false(unreach-call) 2.0  37 31   1 false(unreach-call) 2.9   40 32    1 timeout 900   4800 12000 0 false(unreach-call) .37 15 4.0 1 timeout 910   12000 7000 0 timeout 900   3700 12000 0 timeout 900   6200 11000 0 unknown 500 3900 6300 0
email_spec4_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 23    280 150    1 false(unreach-call) 3.0  55 33   1 timeout 910   11000 6200 0 false(unreach-call) 40   1300 340 0 false(unreach-call) 12   490 110 1 false(unreach-call) 490    200 5500   0 false(unreach-call) 2.6  37 25   1 false(unreach-call) 3.2   41 32    1 timeout 900   5600 10000 0 false(unreach-call) .38 15 4.0 1 timeout 900   12000 9000 0 timeout 900   4400 13000 0 timeout 900   5300 11000 0 unknown 510 3800 5500 0
email_spec4_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 38    430 400    1 false(unreach-call) 4.2  61 51   0 timeout 910   11000 6400 0 false(unreach-call) 220   4400 2300 1 false(unreach-call) 12   480 100 1 false(unreach-call) 490    250 5500   0 false(unreach-call) 2.9  44 25   1 false(unreach-call) 4.0   49 37    1 timeout 900   5100 9900 0 false(unreach-call) .37 17 4.2 1 timeout 910   11000 9600 0 timeout 900   6100 12000 0 timeout 900   6000 10000 0 unknown 530 3900 6700 0
email_spec4_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 21    290 280    1 false(unreach-call) 3.1  54 32   0 timeout 910   11000 6000 0 false(unreach-call) 41   1500 310 1 false(unreach-call) 12   480 98 1 false(unreach-call) 490    290 5400   0 false(unreach-call) 2.7  39 26   1 false(unreach-call) 3.5   43 34    1 timeout 900   5000 9800 0 false(unreach-call) .38 16 4.9 1 timeout 900   13000 7000 0 timeout 900   3800 13000 0 timeout 900   5500 10000 0 unknown 510 3900 5500 0
email_spec4_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 41    480 360    1 false(unreach-call) 4.5  63 65   0 timeout 910   11000 7300 0 timeout 900   6100 9900 0 false(unreach-call) 13   480 110 1 false(unreach-call) 490    260 5400   0 false(unreach-call) 2.7  45 33   1 false(unreach-call) 4.3   49 43    1 timeout 930   5900 9800 0 false(unreach-call) .39 17 4.5 1 timeout 900   12000 10000 0 timeout 900   5000 12000 0 timeout 900   5300 12000 0 unknown 530 3900 6400 0
email_spec4_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 40    510 360    1 false(unreach-call) 4.9  64 51   0 timeout 910   11000 7100 0 timeout 900   8200 7300 0 false(unreach-call) 12   490 120 1 false(unreach-call) 490    210 5500   0 false(unreach-call) 3.0  47 34   1 false(unreach-call) 4.3   52 51    1 timeout 910   5400 12000 0 false(unreach-call) .40 19 4.5 1 timeout 900   10000 6600 0 timeout 900   3200 11000 0 timeout 900   6100 12000 0 unknown 540 4000 6300 0
email_spec4_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 21    280 180    1 false(unreach-call) 3.2  55 33   0 false(unreach-call) 180   6500 1200 1 false(unreach-call) 21   810 170 1 false(unreach-call) 16   620 130 1 false(unreach-call) 490    250 6400   0 false(unreach-call) 2.3  39 23   1 false(unreach-call) 2.9   42 26    1 timeout 900   5800 11000 0 false(unreach-call) .39 16 5.0 1 timeout 910   10000 8500 0 timeout 900   6400 11000 0 timeout 900   4600 10000 0 unknown 500 3800 5600 0
email_spec4_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 22    310 210    1 false(unreach-call) 3.4  56 41   1 timeout 910   11000 6100 0 false(unreach-call) 44   1600 340 0 false(unreach-call) 20   840 170 1 false(unreach-call) 490    230 5600   0 false(unreach-call) 2.6  39 23   1 false(unreach-call) 3.3   43 35    1 timeout 910   6300 12000 0 false(unreach-call) .37 17 4.3 1 timeout 900   13000 7500 0 timeout 900   6400 11000 0 timeout 900   5700 12000 0 unknown 510 3800 5800 0
email_spec4_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 42    510 400    1 false(unreach-call) 5.2  67 59   0 timeout 910   11000 5600 0 false(unreach-call) 330   4600 4000 1 false(unreach-call) 13   510 110 1 false(unreach-call) 490    240 5400   0 false(unreach-call) 2.7  47 33   1 false(unreach-call) 4.3   53 40    1 timeout 910   5700 10000 0 false(unreach-call) .38 18 4.9 1 timeout 900   13000 8400 0 timeout 900   3500 12000 0 timeout 900   4600 9600 0 unknown 530 3900 6000 0
email_spec4_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 28    330 210    1 false(unreach-call) 3.5  57 36   0 false(unreach-call) 270   7600 1800 1 false(unreach-call) 43   1700 370 1 false(unreach-call) 13   490 120 1 false(unreach-call) 490    150 5600   0 false(unreach-call) 2.7  41 30   1 false(unreach-call) 3.4   45 35    1 timeout 930   6100 12000 0 false(unreach-call) .37 18 4.8 1 timeout 900   13000 7100 0 timeout 900   4900 11000 0 timeout 900   4700 10000 0 unknown 520 3800 6200 0
email_spec4_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 46    580 360    1 false(unreach-call) 6.0  71 90   1 timeout 910   11000 5600 0 timeout 900   7100 11000 0 false(unreach-call) 17   720 150 1 false(unreach-call) 490    280 5800   0 false(unreach-call) 3.1  48 29   1 false(unreach-call) 4.5   54 54    1 timeout 910   5800 13000 0 false(unreach-call) .39 19 4.7 1 timeout 900   13000 7300 0 timeout 900   6400 12000 0 timeout 900   5400 9900 0 unknown 540 3900 5500 0
email_spec4_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 40    620 330    1 false(unreach-call) 6.4  76 81   0 timeout 900   11000 6500 0 timeout 900   6200 11000 0 false(unreach-call) 12   480 120 1 false(unreach-call) 490    380 6300   0 false(unreach-call) 3.1  51 41   1 false(unreach-call) 4.9   57 50    1 timeout 910   6200 10000 0 false(unreach-call) .39 20 4.8 1 timeout 900   13000 8100 0 timeout 900   4000 11000 0 timeout 900   5200 12000 0 unknown 550 4000 6000 0
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 130    7600 1300    1 false(unreach-call) 130    640 1300   0 timeout 900   11000 5400 0 timeout 900   9100 8200 0 false(unreach-call) 17   570 150 1 false(unreach-call) 620    1500 6500   0 false(unreach-call) 9.4  170 96   1 false(unreach-call) 27     210 300    1 timeout 910   6900 11000 0 false(unreach-call) .76 25 11   1 timeout 900   12000 6900 0 timeout 900   4500 12000 0 timeout 900   4600 12000 0 timeout 900 4800 9600 0
email_spec6_product12_false-unreach-call_true-termination.cil.c false(unreach-call) 20    240 210    1 false(unreach-call) 2.6  53 27   0 false(unreach-call) 39   1400 320 1 false(unreach-call) 39   1300 290 1 false(unreach-call) 10   400 87 1 false(unreach-call) 490    160 5400   0 false(unreach-call) 1.8  37 19   1 false(unreach-call) 2.3   38 23    1 timeout 900   4400 11000 0 false(unreach-call) .35 14 4.3 1 timeout 900   9200 7700 0 timeout 900   6500 12000 0 timeout 900   6200 12000 0 unknown 500 3800 5200 0
email_spec6_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 39    410 300    1 false(unreach-call) 3.0  56 39   1 timeout 900   7900 9700 0 timeout 900   9300 8400 0 false(unreach-call) 9.9 400 80 1 false(unreach-call) 490    170 5400   0 false(unreach-call) 2.2  40 22   1 false(unreach-call) 2.8   45 32    1 timeout 900   4400 14000 0 false(unreach-call) .37 16 4.0 1 timeout 900   11000 6300 0 timeout 900   6200 12000 0 timeout 900   13000 6800 0 unknown 500 3900 5400 0
email_spec6_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 22    260 180    1 false(unreach-call) 2.9  56 31   0 false(unreach-call) 160   5500 1300 1 timeout 900   6900 9200 0 false(unreach-call) 10   400 81 1 false(unreach-call) 490    180 5500   0 false(unreach-call) 1.9  39 21   1 false(unreach-call) 2.5   42 19    1 timeout 910   5700 10000 0 false(unreach-call) .36 15 4.2 1 timeout 910   13000 6600 0 timeout 900   4100 12000 0 timeout 900   7000 11000 0 unknown 500 3800 5700 0
email_spec6_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 20    270 210    1 false(unreach-call) 3.1  54 36   0 false(unreach-call) 77   3700 540 1 timeout 900   11000 7700 0 false(unreach-call) 11   400 83 1 false(unreach-call) 490    330 5200   0 false(unreach-call) 2.0  39 18   1 false(unreach-call) 2.7   42 26    1 timeout 910   6100 9700 0 false(unreach-call) .36 16 4.6 1 timeout 900   9300 7700 0 timeout 900   6500 13000 0 timeout 900   7000 10000 0 unknown 500 3800 5700 0
email_spec6_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 41    460 390    1 false(unreach-call) 4.5  64 51   0 timeout 910   11000 5600 0 timeout 900   8900 7800 0 false(unreach-call) 11   400 86 1 false(unreach-call) 490    200 6400   0 false(unreach-call) 2.6  46 25   1 false(unreach-call) 4.4   52 42    1 timeout 900   5700 12000 0 false(unreach-call) .39 17 4.6 1 timeout 900   11000 8400 0 timeout 900   6200 14000 0 timeout 900   9900 9500 0 unknown 520 3900 5400 0
email_spec6_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 39    500 330    1 false(unreach-call) 4.8  66 54   1 timeout 910   11000 5900 0 timeout 910   8400 9500 0 false(unreach-call) 11   410 93 1 false(unreach-call) 490    340 5000   0 false(unreach-call) 2.4  48 26   1 false(unreach-call) 4.1   54 40    1 timeout 910   6100 12000 0 false(unreach-call) .40 18 4.7 1 timeout 900   13000 6500 0 timeout 900   6200 15000 0 timeout 900   9700 9700 0 unknown 530 3900 5800 0
email_spec6_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 26    300 210    1 false(unreach-call) 3.2  56 35   1 timeout 900   11000 6200 0 timeout 900   9900 10000 0 false(unreach-call) 10   390 76 1 false(unreach-call) 490    180 6100   0 false(unreach-call) 2.1  41 19   1 false(unreach-call) 3.0   44 36    1 timeout 910   6100 9600 0 false(unreach-call) .37 17 4.6 1 timeout 900   13000 5500 0 timeout 910   6500 13000 0 timeout 900   8700 9500 0 unknown 500 3900 5200 0
email_spec6_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 43    540 390    1 false(unreach-call) 5.3  68 65   0 timeout 900   11000 7200 0 timeout 900   8900 8800 0 false(unreach-call) 11   420 85 1 false(unreach-call) 490    210 6100   0 false(unreach-call) 2.8  51 28   1 false(unreach-call) 5.1   58 58    1 timeout 910   6200 12000 0 false(unreach-call) .38 18 5.1 1 timeout 900   14000 6600 0 timeout 900   6000 12000 0 timeout 900   10000 8300 0 unknown 530 3900 5200 0
email_spec6_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 19    270 150    1 false(unreach-call) 2.6  53 27   0 false(unreach-call) 62   2200 430 1 false(unreach-call) 39   1400 300 1 false(unreach-call) 10   410 82 1 false(unreach-call) 490    310 5000   0 false(unreach-call) 1.9  38 18   1 false(unreach-call) 2.5   40 26    1 timeout 970   6600 10000 0 false(unreach-call) .39 16 5.2 1 timeout 910   13000 7200 0 timeout 900   6400 10000 0 timeout 900   6000 11000 0 unknown 500 3800 5200 0
email_spec6_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 36    480 330    1 false(unreach-call) 3.5  59 41   0 timeout 910   8400 9300 0 timeout 910   8700 10000 0 false(unreach-call) 11   410 94 1 false(unreach-call) 490    180 5600   0 false(unreach-call) 2.4  42 24   1 false(unreach-call) 3.0   47 32    1 timeout 940   6100 11000 0 false(unreach-call) .40 18 4.7 1 timeout 900   12000 7800 0 timeout 900   6000 14000 0 timeout 900   6600 10000 0 unknown 510 3900 5500 0
email_spec6_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 24    290 230    1 false(unreach-call) 3.2  58 30   1