Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-01-13 09:38:46 CET
Run set sv-comp17.Termination-Other
Options -sv-comp17 -heap 10000M -disable-java-assertions
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu wall energy mem validator uautomizer violation t<90s status cpu wall energy mem validator cpachecker correctness t<900s status cpu wall energy mem validator uautomizer correctness t<900s status cpu wall energy mem
pthread-atomic/gcd_true-unreach-call_true-termination.i error 0 wit inspect 3.0 1.2  23 280 0   0   - - - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.5 2.0  55 380 0   0   - - - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.2 1.9  48 380 0   0   - - - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 23   6.1  190 770 0   0   - - - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.6 1.8  44 300 0   0   - - - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.7 1.8  46 300 0   0   - - - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.3 2.0  50 340 0   0   - - - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.1 1.9  48 340 0   0   - - - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 3.1 1.2  26 270 0   0   - - - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 3.4 1.3  31 280 0   0   - - - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 3.6 1.4  31 280 0   0   - - - -
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 29   7.5  220 900 0   0   - - - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 6.7 2.0  54 430 0   0   - - - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c true 2 wit inspect 570   480    7100 4200 0   0   - - - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3700 0   0   - - - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.6 1.4  30 280 0   0   - - - -
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.8 1.5  34 280 0   0   - - - -
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 4.2 1.5  33 280 0   0   - - - -
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 5.8 1.9  46 440 0   0   - - - -
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 4.7 1.8  39 290 0   0   - - - -
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 4.7 1.7  36 300 0   0   - - - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 6.2 2.0  53 410 0   0   - - - -
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 4.6 1.6  40 300 0   0   - - - -
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.1 1.3  28 270 0   0   - - - -
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.6 1.4  27 280 0   0   - - - -
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.3 1.3  31 280 0   0   - - - -
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 3.5 1.4  35 280 0   0   - - - -
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 4.0 1.5  31 280 0   0   - - - -
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c timeout 0 wit inspect 900   720    11000 5200 0   0   - - - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i unknown 0 wit inspect 4.0 1.5  36 300 0   0   - - - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 0 wit inspect 4.3 1.5  34 300 0   0   - - - -
loops/n.c11_true-unreach-call_false-termination.i unknown 0 wit inspect 570   520    7800 4100 0   0   - - - -
loops/nec11_false-unreach-call_false-termination.i unknown 0 wit inspect 660   610    8800 4300 0   0   - - - -
loops/sum03_true-unreach-call_false-termination.i unknown 0 wit inspect 8.7 2.5  70 480 0   0   - - - -
loops/trex04_true-unreach-call_false-termination.i false(termination) 1 wit inspect 3.3 1.3  25 270 0   0   - - - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i false(termination) 1 wit inspect 2.7 1.2  24 270 0   0   - - - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i false(termination) 1 wit inspect 2.7 1.2  23 270 0   0   - - - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i false(termination) 1 wit inspect 2.7 1.2  22 260 0   0   - - - -
loops/array_false-unreach-call_true-termination.i timeout 0 wit inspect 900   840    11000 4400 0   0   - - - -
loops/array_true-unreach-call_true-termination.i timeout 0 wit inspect 910   840    13000 4500 0   0   - - - -
loops/count_up_down_false-unreach-call_true-termination.i true 2 wit inspect 4.5 1.5  40 300 0   0   - - - -
loops/count_up_down_true-unreach-call_true-termination.i true 2 wit inspect 5.4 1.8  37 320 0   0   - - - -
loops/eureka_05_true-unreach-call_true-termination.i timeout 0 wit inspect 900   870    13000 4100 0   0   - - - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i true 2 wit inspect 7.2 2.2  56 480 0   0   - - - -
loops/insertion_sort_false-unreach-call_true-termination.i timeout 0 wit inspect 900   850    11000 4400 0   0   - - - -
loops/insertion_sort_true-unreach-call_true-termination.i timeout 0 wit inspect 900   850    11000 4400 0   0   - - - -
loops/invert_string_false-unreach-call_true-termination.i timeout 0 wit inspect 900   840    11000 4500 0   0   - - - -
loops/invert_string_true-unreach-call_true-termination.i timeout 0 wit inspect 900   850    13000 4500 0   0   - - - -
loops/matrix_false-unreach-call_true-termination.i timeout 0 wit inspect 910   860    13000 4600 0   0   - - - -
loops/matrix_true-unreach-call_true-termination.i timeout 0 wit inspect 900   860    13000 4000 0   0   - - - -
loops/n.c40_true-unreach-call_true-termination.i true 2 wit inspect 3.4 1.3  29 280 0   0   - - - -
loops/nec20_false-unreach-call_true-termination.i true 2 wit inspect 6.0 2.0  49 350 0   0   - - - -
loops/nec40_true-unreach-call_true-termination.i true 2 wit inspect 3.3 1.3  26 280 0   0   - - - -
loops/string_false-unreach-call_true-termination.i timeout 0 wit inspect 920   840    11000 4500 0   0   - - - -
loops/string_true-unreach-call_true-termination.i timeout 0 wit inspect 910   840    12000 4200 0   0   - - - -
loops/sum01_bug02_false-unreach-call_true-termination.i true 2 wit inspect 13   3.4  96 580 0   0   - - - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i true 2 wit inspect 8.2 2.5  59 460 0   0   - - - -
loops/sum01_false-unreach-call_true-termination.i true 2 wit inspect 17   4.6  130 590 0   0   - - - -
loops/sum01_true-unreach-call_true-termination.i true 2 wit inspect 4.0 1.5  37 290 0   0   - - - -
loops/sum03_false-unreach-call_true-termination.i true 2 wit inspect 5.1 1.8  44 320 0   0   - - - -
loops/sum04_false-unreach-call_true-termination.i true 2 wit inspect 11   3.0  91 470 0   0   - - - -
loops/sum04_true-unreach-call_true-termination.i true 2 wit inspect 9.0 2.6  69 440 0   0   - - - -
loops/terminator_01_false-unreach-call_true-termination.i true 2 wit inspect 4.4 1.7  40 290 0   0   - - - -
loops/terminator_02_false-unreach-call_true-termination.i true 2 wit inspect 5.7 1.9  42 330 0   0   - - - -
loops/terminator_02_true-unreach-call_true-termination.i true 2 wit inspect 2.8 1.2  23 270 0   0   - - - -
loops/terminator_03_false-unreach-call_true-termination.i unknown 0 wit inspect 3.2 1.3  28 280 0   0   - - - -
loops/terminator_03_true-unreach-call_true-termination.i unknown 0 wit inspect 3.4 1.3  31 270 0   0   - - - -
loops/trex01_false-unreach-call_true-termination.i true 2 wit inspect 12   3.4  100 480 0   0   - - - -
loops/trex01_true-unreach-call_true-termination.i true 2 wit inspect 13   3.5  100 510 0   0   - - - -
loops/trex02_false-unreach-call_true-termination.i true 2 wit inspect 3.5 1.4  28 270 0   0   - - - -
loops/trex02_true-unreach-call_true-termination.i true 2 wit inspect 3.5 1.4  33 270 0   0   - - - -
loops/trex03_false-unreach-call_true-termination.i true 2 wit inspect 7.4 2.2  53 430 0   0   - - - -
loops/trex03_true-unreach-call_true-termination.i true 2 wit inspect 7.3 2.3  57 440 0   0   - - - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i true 2 wit inspect 3.1 1.2  27 290 0   0   - - - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820    11000 4600 0   0   - - - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i timeout 0 wit inspect 900   840    12000 4400 0   0   - - - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i true 2 wit inspect 3.1 1.2  26 290 0   0   - - - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i timeout 0 wit inspect 900   850    13000 4400 0   0   - - - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i true 2 wit inspect 2.6 1.1  23 270 0   0   - - - -
loop-acceleration/array_false-unreach-call1_true-termination.i timeout 0 wit inspect 900   820    11000 4500 0   0   - - - -
loop-acceleration/array_false-unreach-call2_true-termination.i timeout 0 wit inspect 900   840    12000 4400 0   0   - - - -
loop-acceleration/array_false-unreach-call3_true-termination.i timeout 0 wit inspect 900   840    10000 4500 0   0   - - - -
loop-acceleration/array_true-unreach-call1_true-termination.i timeout 0 wit inspect 900   840    11000 4500 0   0   - - - -
loop-acceleration/array_true-unreach-call2_true-termination.i timeout 0 wit inspect 900   840    11000 4500 0   0   - - - -
loop-acceleration/array_true-unreach-call3_true-termination.i timeout 0 wit inspect 900   840    12000 4500 0   0   - - - -
loop-acceleration/array_true-unreach-call4_true-termination.i timeout 0 wit inspect 900   820    8700 4300 0   0   - - - -
loop-acceleration/diamond_true-unreach-call1_true-termination.i true 2 wit inspect 81   48    900 4000 0   0   - - - -
loop-acceleration/functions_false-unreach-call1_true-termination.i true 2 wit inspect 10   3.0  70 460 0   0   - - - -
loop-acceleration/functions_true-unreach-call1_true-termination.i true 2 wit inspect 8.6 2.5  67 460 0   0   - - - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i true 2 wit inspect 4.1 1.5  34 290 0   0   - - - -
loop-acceleration/multivar_true-unreach-call1_true-termination.i true 2 wit inspect 4.6 1.6  36 290 0   0   - - - -
loop-acceleration/simple_false-unreach-call2_true-termination.i true 2 wit inspect 2.9 1.3  26 270 0   0   - - - -
loop-acceleration/simple_false-unreach-call3_true-termination.i true 2 wit inspect 3.9 1.5  34 280 0   0   - - - -
loop-acceleration/simple_true-unreach-call2_true-termination.i true 2 wit inspect 2.9 1.3  29 280 0   0   - - - -
loop-acceleration/simple_true-unreach-call3_true-termination.i true 2 wit inspect 3.8 1.5  33 270 0   0   - - - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i true 2 wit inspect 8.1 2.3  72 440 0   0   - - - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i true 2 wit inspect 7.7 2.2  69 450 0   0   - - - -
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true 2 wit inspect 9.2 2.6  70 470 0   0   - - - -
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true 2 wit inspect 8.7 2.5  71 450 0   0   - - - -
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i false(termination) 1 wit inspect 11   3.0  79 470 0   0   - - - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true 2 wit inspect 6.5 2.2  48 450 0   0   - - - -
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true 2 wit inspect 5.5 1.9  49 340 0   0   - - - -
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true 2 wit inspect 26   6.7  200 960 0   0   - - - -
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true 2 wit inspect 8.9 2.8  64 460 0   0   - - - -
loop-invgen/down_true-unreach-call_true-termination.i true 2 wit inspect 6.2 1.9  50 390 0   0   - - - -
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820    11000 4400 0   0   - - - -
loop-invgen/half_2_true-unreach-call_true-termination.i true 2 wit inspect 8.3 2.5  67 480 0   0   - - - -
loop-invgen/heapsort_true-unreach-call_true-termination.i true 2 wit inspect 37   11    310 1400 0   0   - - - -
loop-invgen/id_build_true-unreach-call_true-termination.i true 2 wit inspect 14   3.8  110 580 0   0   - - - -
loop-invgen/id_trans_false-unreach-call_true-termination.i true 2 wit inspect 31   11    250 1600 0   0   - - - -
loop-invgen/large_const_true-unreach-call_true-termination.i true 2 wit inspect 6.8 2.2  53 450 0   0   - - - -
loop-invgen/nest-if3_true-unreach-call_true-termination.i true 2 wit inspect 8.1 2.4  60 460 0   0   - - - -
loop-invgen/nested6_true-unreach-call_true-termination.i true 2 wit inspect 20   5.1  160 640 0   0   - - - -
loop-invgen/nested9_true-unreach-call_true-termination.i true 2 wit inspect 12   3.3  110 480 0   0   - - - -
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true 2 wit inspect 11   3.1  81 570 0   0   - - - -
loop-invgen/seq_true-unreach-call_true-termination.i true 2 wit inspect 8.4 2.4  62 480 0   0   - - - -
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i timeout 0 wit inspect 900   860    11000 4000 0   0   - - - -
loop-invgen/up_true-unreach-call_true-termination.i true 2 wit inspect 6.3 1.9  51 390 0   0   - - - -
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   810    9200 4500 0   0   - - - -
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true 2 wit inspect 4.9 1.8  40 310 0   0   - - - -
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true 2 wit inspect 5.9 1.9  47 320 0   0   - - - -
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 4.4 1.5  37 300 0   0   - - - -
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   840    6500 4100 0   0   - - - -
loop-lit/css2003_true-unreach-call_true-termination.c.i true 2 wit inspect 6.6 2.1  58 380 0   0   - - - -
loop-lit/gj2007_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   820    9700 4300 0   0   - - - -
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true 2 wit inspect 4.2 1.6  35 280 0   0   - - - -
loop-lit/gr2006_true-unreach-call_true-termination.c.i timeout 0 wit inspect 900   850    10000 4000 0   0   - - - -
loop-lit/gsv2008_true-unreach-call_true-termination.c.i unknown 0 wit inspect 11   3.2  85 590 0   0   - - - -
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true 2 wit inspect 4.2 1.5  32 290 0   0   - - - -
loop-lit/jm2006_true-unreach-call_true-termination.c.i true 2 wit inspect 5.5 1.8  47 350 0   0   - - - -
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true 2 wit inspect 4.8 1.6  37 290 0   0   - - - -
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true 2 wit inspect 13   3.6  110 640 0   0   - - - -
loop-lit/gcnr2008_false-unreach-call_false-termination.i unknown 0 wit inspect 13   3.8  90 630 0   0   - - - -
loop-new/count_by_1_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810    9400 4400 0   0   - - - -
loop-new/count_by_1_variant_true-unreach-call_true-termination.i timeout 0 wit inspect 900   820    9600 4300 0   0   - - - -
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 0 wit inspect 900   810    9100 4400 0   0   - - - -
loop-new/count_by_k_true-unreach-call_true-termination.i unknown 0 wit inspect 3.3 1.3  32 280 0   0   - - - -
loop-new/count_by_nondet_true-unreach-call_true-termination.i true 2 wit inspect 4.7 1.6  37 300 0   0   - - - -
loop-new/gauss_sum_true-unreach-call_true-termination.i true 2 wit inspect 4.5 1.6  41 300 0   0   - - - -
loop-new/half_true-unreach-call_true-termination.i true 2 wit inspect 80   41    710 3900 0   0   - - - -
loop-new/nested_true-unreach-call_true-termination.i true 2 wit inspect 65   34    610 2500 0   0   - - - -
product-lines/elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 960   280    5200 11000 0   0   - - - -
product-lines/elevator_spec14_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   830    9600 4200 0   0   - - - -
product-lines/elevator_spec14_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    11000 4200 0   0   - - - -
product-lines/elevator_spec14_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    12000 3900 0   0   - - - -
product-lines/elevator_spec14_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   860    10000 3900 0   0   - - - -
product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    12000 4200 0   0   - - - -
product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    9700 4100 0   0   - - - -
product-lines/elevator_spec14_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    9900 3900 0   0   - - - -
product-lines/elevator_spec14_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    13000 4000 0   0   - - - -
product-lines/elevator_spec14_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 4200 0   0   - - - -
product-lines/elevator_spec14_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   840    9400 3900 0   0   - - - -
product-lines/elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    12000 4400 0   0   - - - -
product-lines/elevator_spec1_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    13000 3500 0   0   - - - -
product-lines/elevator_spec1_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    13000 4100 0   0   - - - -
product-lines/elevator_spec1_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3000 0   0   - - - -
product-lines/elevator_spec1_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 4000 0   0   - - - -
product-lines/elevator_spec1_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    14000 2900 0   0   - - - -
product-lines/elevator_spec1_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3800 0   0   - - - -
product-lines/elevator_spec1_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 4000 0   0   - - - -
product-lines/elevator_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    12000 3700 0   0   - - - -
product-lines/elevator_spec1_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3200 0   0   - - - -
product-lines/elevator_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3600 0   0   - - - -
product-lines/elevator_spec1_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3300 0   0   - - - -
product-lines/elevator_spec1_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    10000 4200 0   0   - - - -
product-lines/elevator_spec1_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    9500 2800 0   0   - - - -
product-lines/elevator_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    12000 3800 0   0   - - - -
product-lines/elevator_spec1_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    11000 4200 0   0   - - - -
product-lines/elevator_spec1_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    13000 3000 0   0   - - - -
product-lines/elevator_spec1_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3800 0   0   - - - -
product-lines/elevator_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 3800 0   0   - - - -
product-lines/elevator_spec1_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    10000 4000 0   0   - - - -
product-lines/elevator_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3700 0   0   - - - -
product-lines/elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    10000 3900 0   0   - - - -
product-lines/elevator_spec2_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3900 0   0   - - - -
product-lines/elevator_spec2_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3200 0   0   - - - -
product-lines/elevator_spec2_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3500 0   0   - - - -
product-lines/elevator_spec2_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   810    10000 4400 0   0   - - - -
product-lines/elevator_spec2_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 2600 0   0   - - - -
product-lines/elevator_spec2_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3600 0   0   - - - -
product-lines/elevator_spec2_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    13000 3100 0   0   - - - -
product-lines/elevator_spec2_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 2600 0   0   - - - -
product-lines/elevator_spec2_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    9800 3700 0   0   - - - -
product-lines/elevator_spec2_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    10000 3500 0   0   - - - -
product-lines/elevator_spec2_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3800 0   0   - - - -
product-lines/elevator_spec2_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    9900 4100 0   0   - - - -
product-lines/elevator_spec2_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    9600 3900 0   0   - - - -
product-lines/elevator_spec2_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    11000 4000 0   0   - - - -
product-lines/elevator_spec2_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3400 0   0   - - - -
product-lines/elevator_spec2_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3700 0   0   - - - -
product-lines/elevator_spec2_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3800 0   0   - - - -
product-lines/elevator_spec2_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3800 0   0   - - - -
product-lines/elevator_spec2_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 4000 0   0   - - - -
product-lines/elevator_spec2_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    13000 3800 0   0   - - - -
product-lines/elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 4000 0   0   - - - -
product-lines/elevator_spec3_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    10000 4100 0   0   - - - -
product-lines/elevator_spec3_product03_false-unreach-call_true-termination.cil.c true 2 wit inspect 240   210    2700 3000 0   0   - - - -
product-lines/elevator_spec3_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    12000 4100 0   0   - - - -
product-lines/elevator_spec3_product11_false-unreach-call_true-termination.cil.c true 2 wit inspect 290   260    4000 2500 0   0   - - - -
product-lines/elevator_spec3_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 3800 0   0   - - - -
product-lines/elevator_spec3_product18_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3900 0   0   - - - -
product-lines/elevator_spec3_product19_false-unreach-call_true-termination.cil.c true 2 wit inspect 280   250    3400 3800 0   0   - - - -
product-lines/elevator_spec3_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 3900 0   0   - - - -
product-lines/elevator_spec3_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3900 0   0   - - - -
product-lines/elevator_spec3_product22_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 3900 0   0   - - - -
product-lines/elevator_spec3_product23_false-unreach-call_true-termination.cil.c true 2 wit inspect 480   440    6700 3600 0   0   - - - -
product-lines/elevator_spec3_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   850    11000 4000 0   0   - - - -
product-lines/elevator_spec3_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3800 0   0   - - - -
product-lines/elevator_spec3_product26_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    11000 3900 0   0   - - - -
product-lines/elevator_spec3_product27_false-unreach-call_true-termination.cil.c true 2 wit inspect 490   450    6000 2600 0   0   - - - -
product-lines/elevator_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   850    13000 3900 0   0   - - - -
product-lines/elevator_spec3_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    12000 3900 0   0   - - - -
product-lines/elevator_spec3_product30_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3900 0   0   - - - -
product-lines/elevator_spec3_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 560   520    7500 3700 0   0   - - - -
product-lines/elevator_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   850    8900 3900 0   0   - - - -
product-lines/elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    9200 4500 0   0   - - - -
product-lines/elevator_spec9_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    10000 3600 0   0   - - - -
product-lines/elevator_spec9_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    11000 4200 0   0   - - - -
product-lines/elevator_spec9_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 4100 0   0   - - - -
product-lines/elevator_spec9_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    13000 2900 0   0   - - - -
product-lines/elevator_spec9_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    11000 4000 0   0   - - - -
product-lines/elevator_spec9_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   860    12000 3700 0   0   - - - -
product-lines/elevator_spec9_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    12000 4000 0   0   - - - -
product-lines/elevator_spec9_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   850    11000 3800 0   0   - - - -
product-lines/elevator_spec9_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    11000 4200 0   0   - - - -
product-lines/elevator_spec9_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   830    11000 4100 0   0   - - - -
product-lines/elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   840    11000 4100 0   0   - - - -
product-lines/email_spec0_product05_true-unreach-call_true-termination.cil.c true 2 wit inspect 180   130    1800 4100 0   0   - - - -
product-lines/email_spec0_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 160   120    2000 3900 0   0   - - - -
product-lines/email_spec0_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 96   52    910 3600 0   0   - - - -
product-lines/email_spec0_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 160   120    1900 3900 0   0   - - - -
product-lines/email_spec0_product16_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   94    1500 3800 0   0   - - - -
product-lines/email_spec0_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1500 3800 0   0   - - - -
product-lines/email_spec0_product21_false-unreach-call_true-termination.cil.c true 2 wit inspect 190   140    2200 3900 0   0   - - - -
product-lines/email_spec0_product22_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   97    1500 3800 0   0   - - - -
product-lines/email_spec0_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   92    1400 3800 0   0   - - - -
product-lines/email_spec0_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 200   160    2300 3900 0   0   - - - -
product-lines/email_spec0_product26_false-unreach-call_true-termination.cil.c true 2 wit inspect 250   200    2900 3900 0   0   - - - -
product-lines/email_spec0_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 210   160    2600 3900 0   0   - - - -
product-lines/email_spec0_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 120   69    1100 3700 0   0   - - - -
product-lines/email_spec0_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 230   180    2400 4000 0   0   - - - -
product-lines/email_spec0_product34_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   91    1400 3900 0   0   - - - -
product-lines/email_spec0_product35_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    1800 3800 0   0   - - - -
product-lines/email_spec0_product36_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   690    11000 6400 0   0   - - - -
product-lines/email_spec0_product37_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   620    9900 8900 0   0   - - - -
product-lines/email_spec0_product38_true-unreach-call_true-termination.cil.c true 2 wit inspect 290   240    3800 3900 0   0   - - - -
product-lines/email_spec0_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 600   490    6600 5400 0   0   - - - -
product-lines/email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   660    8800 7000 0   0   - - - -
product-lines/email_spec11_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 140   91    1700 3800 0   0   - - - -
product-lines/email_spec11_product07_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   77    1400 3800 0   0   - - - -
product-lines/email_spec11_product08_true-unreach-call_true-termination.cil.c true 2 wit inspect 120   74    1200 3800 0   0   - - - -
product-lines/email_spec11_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 210   160    2100 3700 0   0   - - - -
product-lines/email_spec11_product15_false-unreach-call_true-termination.cil.c true 2 wit inspect 100   58    900 3800 0   0   - - - -
product-lines/email_spec11_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 180   130    1800 4000 0   0   - - - -
product-lines/email_spec11_product20_false-unreach-call_true-termination.cil.c true 2 wit inspect 160   110    1800 4000 0   0   - - - -
product-lines/email_spec11_product22_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    1900 3900 0   0   - - - -
product-lines/email_spec11_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 230   180    2600 3900 0   0   - - - -
product-lines/email_spec11_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 160   100    1500 4100 0   0   - - - -
product-lines/email_spec11_product26_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   92    1500 3800 0   0   - - - -
product-lines/email_spec11_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 220   170    2200 3900 0   0   - - - -
product-lines/email_spec11_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   670    8900 7500 0   0   - - - -
product-lines/email_spec11_product32_false-unreach-call_true-termination.cil.c true 2 wit inspect 250   200    2700 3900 0   0   - - - -
product-lines/email_spec11_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 190   140    2000 4000 0   0   - - - -
product-lines/email_spec11_product35_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    1800 3800 0   0   - - - -
product-lines/email_spec11_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 410   350    4800 4000 0   0   - - - -
product-lines/email_spec11_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 240   190    2800 3900 0   0   - - - -
product-lines/email_spec11_product39_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   710    9300 6500 0   0   - - - -
product-lines/email_spec11_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 200   150    2100 3800 0   0   - - - -
product-lines/email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   710    9100 5300 0   0   - - - -
product-lines/email_spec1_product12_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   730    9900 6500 0   0   - - - -
product-lines/email_spec1_product14_false-unreach-call_true-termination.cil.c true 2 wit inspect 180   130    2000 3900 0   0   - - - -
product-lines/email_spec1_product15_false-unreach-call_true-termination.cil.c true 2 wit inspect 250   200    2700 3900 0   0   - - - -
product-lines/email_spec1_product16_false-unreach-call_true-termination.cil.c true 2 wit inspect 130   87    1400 3700 0   0   - - - -
product-lines/email_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   640    9100 7800 0   0   - - - -
product-lines/email_spec1_product21_false-unreach-call_true-termination.cil.c true 2 wit inspect 180   130    2100 3900 0   0   - - - -
product-lines/email_spec1_product22_false-unreach-call_true-termination.cil.c true 2 wit inspect 82   38    820 3700 0   0   - - - -
product-lines/email_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 970   690    9000 7700 0   0   - - - -
product-lines/email_spec1_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   660    9400 7500 0   0   - - - -
product-lines/email_spec1_product29_false-unreach-call_true-termination.cil.c true 2 wit inspect 360   290    4000 4300 0   0   - - - -
product-lines/email_spec1_product30_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1800 3900 0   0   - - - -
product-lines/email_spec1_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    1900 3800 0   0   - - - -
product-lines/email_spec1_product32_false-unreach-call_true-termination.cil.c true 2 wit inspect 210   160    2700 3800 0   0   - - - -
product-lines/email_spec1_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 200   150    2200 3800 0   0   - - - -
product-lines/email_spec1_product34_false-unreach-call_true-termination.cil.c true 2 wit inspect 810   600    9300 7200 0   0   - - - -
product-lines/email_spec1_product35_false-unreach-call_true-termination.cil.c true 2 wit inspect 210   160    2300 3900 0   0   - - - -
product-lines/email_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   740    10000 5400 0   0   - - - -
product-lines/email_spec27_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 240   200    2800 3900 0   0   - - - -
product-lines/email_spec27_product17_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    1900 3800 0   0   - - - -
product-lines/email_spec27_product18_false-unreach-call_true-termination.cil.c true 2 wit inspect 430   370    5400 4100 0   0   - - - -
product-lines/email_spec27_product19_false-unreach-call_true-termination.cil.c true 2 wit inspect 270   220    3100 4000 0   0   - - - -
product-lines/email_spec27_product23_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   88    1500 3800 0   0   - - - -
product-lines/email_spec27_product24_false-unreach-call_true-termination.cil.c true 2 wit inspect 340   270    3300 4500 0   0   - - - -
product-lines/email_spec27_product25_false-unreach-call_true-termination.cil.c true 2 wit inspect 160   120    1700 3800 0   0   - - - -
product-lines/email_spec27_product27_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   87    1400 3800 0   0   - - - -
product-lines/email_spec27_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 140   99    1500 3800 0   0   - - - -
product-lines/email_spec27_product29_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   110    1600 3800 0   0   - - - -
product-lines/email_spec27_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   620    8300 7500 0   0   - - - -
product-lines/email_spec27_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 690   540    7100 5800 0   0   - - - -
product-lines/email_spec27_product32_false-unreach-call_true-termination.cil.c true 2 wit inspect 220   170    2200 4000 0   0   - - - -
product-lines/email_spec27_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 190   140    2300 3900 0   0   - - - -
product-lines/email_spec27_product34_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   91    1500 3800 0   0   - - - -
product-lines/email_spec27_product35_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   98    1600 3800 0   0   - - - -
product-lines/email_spec27_productSimulator_false-unreach-call_true-termination.cil.c true 2 wit inspect 780   550    8600 6900 0   0   - - - -
product-lines/email_spec3_product13_false-unreach-call_true-termination.cil.c true 2 wit inspect 160   110    1600 3800 0   0   - - - -
product-lines/email_spec3_product17_false-unreach-call_true-termination.cil.c true 2 wit inspect 260   200    2700 4400 0   0   - - - -
product-lines/email_spec3_product18_false-unreach-call_true-termination.cil.c true 2 wit inspect 170   120    2100 4200 0   0   - - - -
product-lines/email_spec3_product19_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   94    1500 3800 0   0   - - - -
product-lines/email_spec3_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 970   710    8800 7500 0   0   - - - -
product-lines/email_spec3_product24_false-unreach-call_true-termination.cil.c true 2 wit inspect 200   160    2200 3900 0   0   - - - -
product-lines/email_spec3_product25_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1500 3900 0   0   - - - -
product-lines/email_spec3_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   550    7100 8600 0   0   - - - -
product-lines/email_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   660    8100 7900 0   0   - - - -
product-lines/email_spec3_product29_false-unreach-call_true-termination.cil.c true 2 wit inspect 160   110    1800 3900 0   0   - - - -
product-lines/email_spec3_product30_false-unreach-call_true-termination.cil.c true 2 wit inspect 190   140    1900 4100 0   0   - - - -
product-lines/email_spec3_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   94    1500 3800 0   0   - - - -
product-lines/email_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   730    12000 7200 0   0   - - - -
product-lines/email_spec3_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 190   150    2400 3900 0   0   - - - -
product-lines/email_spec3_product34_false-unreach-call_true-termination.cil.c true 2 wit inspect 240   180    3000 3900 0   0   - - - -
product-lines/email_spec3_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   720    11000 6800 0   0   - - - -
product-lines/email_spec3_productSimulator_false-unreach-call_true-termination.cil.c true 2 wit inspect 550   360    5300 5900 0   0   - - - -
product-lines/email_spec4_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 250   200    3300 3900 0   0   - - - -
product-lines/email_spec4_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   690    9800 7700 0   0   - - - -
product-lines/email_spec4_product18_false-unreach-call_true-termination.cil.c true 2 wit inspect 130   86    1400 3800 0   0   - - - -
product-lines/email_spec4_product19_false-unreach-call_true-termination.cil.c true 2 wit inspect 410   350    4200 4400 0   0   - - - -
product-lines/email_spec4_product23_false-unreach-call_true-termination.cil.c true 2 wit inspect 180   130    1800 4200 0   0   - - - -
product-lines/email_spec4_product24_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1700 3800 0   0   - - - -
product-lines/email_spec4_product25_false-unreach-call_true-termination.cil.c true 2 wit inspect 230   180    2800 3900 0   0   - - - -
product-lines/email_spec4_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   750    9900 5900 0   0   - - - -
product-lines/email_spec4_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 130   84    1300 3800 0   0   - - - -
product-lines/email_spec4_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 140   94    1400 3800 0   0   - - - -
product-lines/email_spec4_product30_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1500 3800 0   0   - - - -
product-lines/email_spec4_product31_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   90    1400 3800 0   0   - - - -
product-lines/email_spec4_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   630    9500 7600 0   0   - - - -
product-lines/email_spec4_product33_false-unreach-call_true-termination.cil.c true 2 wit inspect 200   160    1900 4000 0   0   - - - -
product-lines/email_spec4_product34_false-unreach-call_true-termination.cil.c true 2 wit inspect 240   190    2900 3900 0   0   - - - -
product-lines/email_spec4_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   740    9100 5700 0   0   - - - -
product-lines/email_spec4_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   740    11000 5200 0   0   - - - -
product-lines/email_spec6_product12_false-unreach-call_true-termination.cil.c true 2 wit inspect 87   44    860 3800 0   0   - - - -
product-lines/email_spec6_product14_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   110    1700 3700 0   0   - - - -
product-lines/email_spec6_product15_false-unreach-call_true-termination.cil.c true 2 wit inspect 130   81    1400 3800 0   0   - - - -
product-lines/email_spec6_product16_false-unreach-call_true-termination.cil.c true 2 wit inspect 230   180    2600 3900 0   0   - - - -
product-lines/email_spec6_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   750    9900 6200 0   0   - - - -
product-lines/email_spec6_product21_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   100    1600 3900 0   0   - - - -
product-lines/email_spec6_product22_false-unreach-call_true-termination.cil.c true 2 wit inspect 130   76    1300 3800 0   0   - - - -
product-lines/email_spec6_product26_false-unreach-call_true-termination.cil.c true 2 wit inspect 150   110    1900 3800 0   0   - - - -
product-lines/email_spec6_product28_false-unreach-call_true-termination.cil.c true 2 wit inspect 140   97    1300 3800 0   0   - -