Tool CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:27:04 CET 2017-12-01 18:45:24 CET 2017-12-01 18:50:14 CET
Run set cpa-seq.sv-comp18.Termination-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-Other
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1227.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-12-01_1227.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 0 2.6 260 22 - -
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 0 2.8 300 26 - -
array-examples/standard_sentinel_true-unreach-call_true-termination.i 0 2.5 270 25 - -
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 2.6 270 24 - -
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 2.5 270 22 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 2.5 260 20 - -
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 2.5 260 25 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 2.5 270 21 - -
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 900   4400 12000 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 2.6 270 26 - -
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 1 3.0 270 23 1 3.4  260 1 5.4   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 1 3.0 270 26 1 3.2  260 1 42     1000  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 1 3.2 270 31 1 4.8  270 1 66     290  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 1 3.2 270 31 1 3.9  270 1 78     280  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 1 3.3 270 28 1 4.6  270 1 67     300  
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 0 920   11000 9300 - -
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 0 900   10000 7000 - -
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 0 900   3900 11000 - -
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 76   520 890 - -
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 1 53   1900 420 0 5.9  280 1 13     480  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 1 52   1600 400 0 5.0  270 1 12     460  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c 2 8.1 450 66 - -
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 7.2 470 63 - -
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 8.1 470 70 - -
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c 2 7.3 400 56 - -
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 7.4 470 55 - -
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c 2 2.5 260 22 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c 2 2.5 260 24 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c 2 2.5 260 23 - -
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c 2 2.5 260 21 - -
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c 2 2.5 260 21 - -
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c 0 2.5 270 23 - -
bitvector-regression/signextension2_false-unreach-call_true-termination.c 2 2.6 270 23 - -
bitvector-regression/signextension2_true-unreach-call_true-termination.c 2 2.6 260 21 - -
bitvector-regression/signextension_false-unreach-call_true-termination.c 2 2.7 270 22 - -
bitvector-regression/signextension_true-unreach-call_true-termination.c 2 2.5 270 22 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i 0 900   4500 11000 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.7 360 58 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.1 340 51 - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 16   700 140 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 4.8 290 42 - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 5.0 320 43 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 5.3 300 51 - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 5.2 300 46 - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 3.1 270 25 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 3.8 290 35 - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 4.1 280 33 - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 0 900   4000 13000 0 .54 44 0 .019 4.9
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 900   4200 10000 0 .57 44 0 .028 4.8
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 900   5000 11000 0 .53 43 0 .020 4.8
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 0 900   5200 12000 0 .52 41 0 .021 4.9
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 0 900   4200 10000 0 .53 41 0 .023 4.8
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 230   3500 2300 0 7.7  270 1 74     2000  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 900   4400 9400 0 .58 42 0 .019 5.0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 1 25   680 210 0 5.6  260 1 23     610  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 1 7.3 390 61 0 5.1  270 1 13     440  
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 0 900   4500 9700 0 .53 42 0 .019 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 900   4400 12000 0 .55 44 0 .019 5.0
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 900   4800 11000 0 .71 43 0 .024 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 900   4800 9600 0 .61 43 0 .019 4.9
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 0 900   2800 11000 0 .53 43 0 .021 4.9
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 900   4300 10000 0 .55 41 0 .018 4.8
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 900   4700 11000 0 .69 42 0 .020 4.8
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 900   4600 9900 0 .52 43 0 .019 4.9
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 0 900   4100 11000 - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 0 900   4500 12000 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 0 900   4100 11000 - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 900   4100 11000 - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 0 900   4400 11000 - -
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 0 900   4200 11000 - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 0 900   4500 11000 - -
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 0 900   4600 11000 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 1 10   580 76 0 2.8  270 1 16     540  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 1 15   820 100 0 5.6  270 1 17     590  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 1 16   1100 140 0 5.6  270 1 20     590  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 1 26   2000 200 0 4.3  280 1 13     620  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 5.0 300 39 0 4.2  270 1 31     2300  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 1 43   3100 370 0 4.5  270 1 26     670  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 26   2000 210 0 4.3  270 1 23     610  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 1 96   4900 890 0 4.4  270 1 23     640  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 1 4.1 300 38 0 3.2  270 1 9.4   360  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 1 4.4 290 38 0 3.7  260 1 7.3   440  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 1 5.0 310 41 0 3.9  290 1 11     480  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 1 5.9 450 44 0 4.7  270 1 14     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 1 7.6 460 58 0 5.6  270 1 14     450  
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c 0 900   4400 9000 - -
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 910   5000 11000 - -
eca-rers2012/Problem01_label00_true-unreach-call_false-termination.c 1 210   3500 2300 0 47    2100 1 49     1300  
eca-rers2012/Problem01_label01_true-unreach-call_false-termination.c 0 910   3200 13000 0 .53 42 0 .020 4.9
eca-rers2012/Problem01_label02_true-unreach-call_false-termination.c 0 910   2900 11000 0 .52 41 0 .019 4.9
eca-rers2012/Problem01_label03_true-unreach-call_false-termination.c 1 220   3100 2800 0 47    2100 1 48     1500  
eca-rers2012/Problem01_label04_true-unreach-call_false-termination.c 0 910   2900 13000 0 .52 43 0 .020 4.8
eca-rers2012/Problem01_label05_true-unreach-call_false-termination.c 1 580   2900 6800 0 44    2100 1 48     1200  
eca-rers2012/Problem01_label06_true-unreach-call_false-termination.c 0 910   3100 13000 0 .53 41 0 .019 4.8
eca-rers2012/Problem01_label07_true-unreach-call_false-termination.c 0 910   3000 12000 0 .52 42 0 .019 4.9
eca-rers2012/Problem01_label08_true-unreach-call_false-termination.c 0 910   3200 12000 0 .53 41 0 .019 4.9
eca-rers2012/Problem01_label09_true-unreach-call_false-termination.c 0 910   3400 13000 0 .49 43 0 .019 4.8
eca-rers2012/Problem01_label10_true-unreach-call_false-termination.c 0 910   3100 11000 0 .52 42 0 .019 4.9
eca-rers2012/Problem01_label11_true-unreach-call_false-termination.c 0 910   3000 13000 0 .58 43 0 .018 4.9
eca-rers2012/Problem01_label12_true-unreach-call_false-termination.c 1 200   3400 2300 0 47    2100 1 47     1500  
eca-rers2012/Problem01_label13_true-unreach-call_false-termination.c 1 800   2800 11000 0 48    2100 1 50     1400  
eca-rers2012/Problem01_label14_true-unreach-call_false-termination.c 1 670   2800 8500 0 47    2100 1 50     1300  
eca-rers2012/Problem01_label15_false-unreach-call_false-termination.c 0 910   3200 11000 0 .54 41 0 .025 4.8
eca-rers2012/Problem01_label16_true-unreach-call_false-termination.c 0 910   2700 12000 0 .71 41 0 .020 4.8
eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c 0 910   3300 13000 0 .52 44 0 .020 4.9
eca-rers2012/Problem01_label18_true-unreach-call_false-termination.c 0 910   3500 11000 0 .53 41 0 .019 4.9
eca-rers2012/Problem01_label19_true-unreach-call_false-termination.c 0 910   3200 13000 0 .52 43 0 .019 4.8
eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c 0 910   3400 11000 0 .39 45 0 .019 5.0
eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c 0 910   3000 12000 0 .55 41 0 .019 4.9
eca-rers2012/Problem01_label22_true-unreach-call_false-termination.c 0 910   2900 12000 0 .40 44 0 .019 4.9
eca-rers2012/Problem01_label23_true-unreach-call_false-termination.c 0 910   2800 12000 0 .52 41 0 .019 4.9
eca-rers2012/Problem01_label24_true-unreach-call_false-termination.c 1 210   3100 2500 0 44    2100 1 54     1500  
eca-rers2012/Problem01_label25_true-unreach-call_false-termination.c 0 910   3200 13000 0 .51 41 0 .019 4.9
eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c 1 850   2600 11000 0 44    2100 1 54     1300  
eca-rers2012/Problem01_label27_true-unreach-call_false-termination.c 0 910   3400 13000 0 .55 42 0 .019 4.9
eca-rers2012/Problem01_label28_true-unreach-call_false-termination.c 0 910   3400 11000 0 .51 43 0 .018 4.8
eca-rers2012/Problem01_label29_true-unreach-call_false-termination.c 0 910   3600 10000 0 .53 41 0 .019 5.0
eca-rers2012/Problem01_label30_true-unreach-call_false-termination.c 0 910   2900 11000 0 .83 43 0 .019 4.9
eca-rers2012/Problem01_label31_true-unreach-call_false-termination.c 1 440   2900 5300 0 57    2100 1 51     1400  
eca-rers2012/Problem01_label32_false-unreach-call_false-termination.c 0 910   2700 13000 0 .53 44 0 .019 4.8
eca-rers2012/Problem01_label33_false-unreach-call_false-termination.c 0 910   3100 12000 0 .52 42 0 .021 4.8
eca-rers2012/Problem01_label34_true-unreach-call_false-termination.c 0 910   3200 12000 0 .53 43 0 .037 4.9
eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c 0 910   3300 11000 0 .53 43 0 .023 4.9
eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c 1 820   2900 10000 0 45    2100 1 50     1400  
eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c 0 910   3200 12000 0 .52 44 0 .019 4.9
eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c 0 910   3100 13000 0 .59 43 0 .019 4.9
eca-rers2012/Problem01_label39_true-unreach-call_false-termination.c 0 910   3500 13000 0 .51 41 0 .019 5.0
eca-rers2012/Problem01_label40_true-unreach-call_false-termination.c 1 190   3600 2400 0 44    2100 1 53     1300  
eca-rers2012/Problem01_label41_true-unreach-call_false-termination.c 0 910   3100 13000 0 .52 41 0 .019 4.9
eca-rers2012/Problem01_label42_true-unreach-call_false-termination.c 1 790   3100 10000 0 46    2100 1 35     1500  
eca-rers2012/Problem01_label43_true-unreach-call_false-termination.c 0 910   3500 13000 0 .51 44 0 .019 5.0
eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c 0 910   3300 13000 0 .75 42 0 .019 4.8
eca-rers2012/Problem01_label45_true-unreach-call_false-termination.c 1 690   2700 8600 0 45    2100 1 50     1300  
eca-rers2012/Problem01_label46_true-unreach-call_false-termination.c 1 190   3500 2100 0 44    2100 1 36     1400  
eca-rers2012/Problem01_label47_false-unreach-call_false-termination.c 0 910   3000 12000 0 .51 41 0 .024 4.8
eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c 0 910   3200 12000 0 .53 44 0 .022 4.8
eca-rers2012/Problem01_label49_true-unreach-call_false-termination.c 0 910   3100 12000 0 .53 42 0 .020 4.8
eca-rers2012/Problem01_label50_false-unreach-call_false-termination.c 0 910   3200 13000 0 .54 43 0 .019 4.8
eca-rers2012/Problem01_label51_true-unreach-call_false-termination.c 0 910   3100 13000 0 .69 42 0 .019 4.9
eca-rers2012/Problem01_label52_true-unreach-call_false-termination.c 0 910   3200 12000 0 .51 43 0 .019 4.8
eca-rers2012/Problem01_label53_true-unreach-call_false-termination.c 1 200   3400 2300 0 44    2100 1 49     1500  
eca-rers2012/Problem01_label54_true-unreach-call_false-termination.c 0 910   3000 11000 0 .53 41 0 .019 4.9
eca-rers2012/Problem01_label55_true-unreach-call_false-termination.c 0 910   3400 12000 0 .51 41 0 .019 4.9
eca-rers2012/Problem01_label56_false-unreach-call_false-termination.c 0 910   2800 14000 0 .62 41 0 .018 4.8
eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c 0 910   3200 11000 0 .52 43 0 .027 4.8
eca-rers2012/Problem01_label58_true-unreach-call_false-termination.c 0 910   3000 14000 0 .71 41 0 .018 4.9
eca-rers2012/Problem01_label59_true-unreach-call_false-termination.c 0 910   3000 14000 0 .71 44 0 .019 5.0
eca-rers2012/Problem02_label00_true-unreach-call_false-termination.c 1 310   2800 3900 0 91    2700 1 39     820  
eca-rers2012/Problem02_label01_true-unreach-call_false-termination.c 1 45   2400 460 0 92    2700 1 38     990  
eca-rers2012/Problem02_label02_true-unreach-call_false-termination.c 1 65   3200 660 0 91    2900 1 42     890  
eca-rers2012/Problem02_label03_true-unreach-call_false-termination.c 1 44   2300 420 0 92    2700 1 43     880  
eca-rers2012/Problem02_label04_true-unreach-call_false-termination.c 1 65   3300 810 0 92    2700 1 37     870  
eca-rers2012/Problem02_label05_true-unreach-call_false-termination.c 1 320   2900 3900 0 91    2700 1 38     890  
eca-rers2012/Problem02_label06_true-unreach-call_false-termination.c 1 310   3200 4200 0 92    2700 1 42     880  
eca-rers2012/Problem02_label07_true-unreach-call_false-termination.c 1 300   2900 3600 0 92    2500 1 37     790  
eca-rers2012/Problem02_label08_true-unreach-call_false-termination.c 1 64   3000 720 0 92    2700 1 38     890  
eca-rers2012/Problem02_label09_true-unreach-call_false-termination.c 1 310   2800 4000 0 92    2500 1 38     870  
eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c 1 43   2300 370 0 91    2700 1 36     870  
eca-rers2012/Problem02_label11_true-unreach-call_false-termination.c 1 50   2800 540 0 92    2800 1 41     880  
eca-rers2012/Problem02_label12_true-unreach-call_false-termination.c 1 50   2400 490 0 91    2700 1 42     980  
eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c 1 48   2500 390 0 91    2700 1 39     880  
eca-rers2012/Problem02_label14_true-unreach-call_false-termination.c 1 65   3300 720 0 92    2700 1 42     990  
eca-rers2012/Problem02_label15_true-unreach-call_false-termination.c 1 47   2500 450 0 91    2700 1 40     890  
eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c 1 45   2400 440 0 91    2700 1 29     900  
eca-rers2012/Problem02_label17_true-unreach-call_false-termination.c 1 53   2300 420 0 91    2700 1 47     770  
eca-rers2012/Problem02_label18_true-unreach-call_false-termination.c 1 50   2800 590 0 91    2700 1 26     880  
eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c 1 48   2600 530 0 92    2700 1 38     880  
eca-rers2012/Problem02_label20_true-unreach-call_false-termination.c 1 46   2500 470 0 92    2600 1 40     990  
eca-rers2012/Problem02_label21_true-unreach-call_false-termination.c 1 320   2900 3600 0 91    2700 1 40     870  
eca-rers2012/Problem02_label22_true-unreach-call_false-termination.c 1 72   3300 740 0 91    2700 1 43     1000  
eca-rers2012/Problem02_label23_true-unreach-call_false-termination.c 1 290   2900 3100 0 92    2700 1 40     870  
eca-rers2012/Problem02_label24_true-unreach-call_false-termination.c 1 290   2600 3500 0 91    2700 1 38     980  
eca-rers2012/Problem02_label25_true-unreach-call_false-termination.c 1 310   2800 4300 0 91    2500 1 38     880  
eca-rers2012/Problem02_label26_true-unreach-call_false-termination.c 1 48   2600 420 0 91    2700 1 37     870  
eca-rers2012/Problem02_label27_true-unreach-call_false-termination.c 1 54   3000 560 0 92    2700 1 42     890  
eca-rers2012/Problem02_label28_true-unreach-call_false-termination.c 1 61   3400 670 0 91    2600 1 39     880  
eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c 1 44   2300 410 0 91    2700 1 37     880  
eca-rers2012/Problem02_label30_true-unreach-call_false-termination.c 1 43   2400 430 0 92    2700 1 40     880  
eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c 1 47   2600 490 0 92    2700 1 44     990  
eca-rers2012/Problem02_label32_true-unreach-call_false-termination.c 1 44   2400 390 0 91    2700 1 39     930  
eca-rers2012/Problem02_label33_true-unreach-call_false-termination.c 1 130   3100 1500 0 91    2700 1 42     920  
eca-rers2012/Problem02_label34_true-unreach-call_false-termination.c 1 43   2400 460 0 91    2800 1 41     880  
eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c 1 45   2400 410 0 91    2700 1 41     980  
eca-rers2012/Problem02_label36_true-unreach-call_false-termination.c 1 390   2900 4900 0 91    2700 1 39     900  
eca-rers2012/Problem02_label37_true-unreach-call_false-termination.c 1 63   3000 710 0 91    2700 1 39     1000  
eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c 1 48   2600 500 0 91    2700 1 37     810  
eca-rers2012/Problem02_label39_true-unreach-call_false-termination.c 1 64   3200 580 0 91    2600 1 40     880  
eca-rers2012/Problem02_label40_true-unreach-call_false-termination.c 1 41   2500 440 0 92    2700 1 43     990  
eca-rers2012/Problem02_label41_true-unreach-call_false-termination.c 1 45   2500 510 0 91    2600 1 30     910  
eca-rers2012/Problem02_label42_true-unreach-call_false-termination.c 1 320   2700 4400 0 91    2700 1 42     890  
eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c 1 47   2500 490 0 91    2800 1 39     910  
eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c 1 230   2800 2900 0 92    2700 1 42     970  
eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c 1 290   2900 3400 0 91    2700 1 41     1000  
eca-rers2012/Problem02_label46_true-unreach-call_false-termination.c 1 48   2700 440 0 91    2700 1 38     870  
eca-rers2012/Problem02_label47_true-unreach-call_false-termination.c 1 290   2700 3700 0 91    2600 1 40     880  
eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c 1 43   2200 370 0 91    2800 1 42     880  
eca-rers2012/Problem02_label49_true-unreach-call_false-termination.c 1 42   2300 360 0 92    2500 1 37     890  
eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c 1 45   2400 510 0 92    2700 1 39     870  
eca-rers2012/Problem02_label51_true-unreach-call_false-termination.c 1 46   2200 480 0 91    2700 1 38     890  
eca-rers2012/Problem02_label52_true-unreach-call_false-termination.c 1 44   2400 420 0 92    2700 1 40     880  
eca-rers2012/Problem02_label53_true-unreach-call_false-termination.c 1 67   3100 630 0 92    2700 1 37     870  
eca-rers2012/Problem02_label54_true-unreach-call_false-termination.c 1 47   2500 440 0 91    2700 1 41     990  
eca-rers2012/Problem02_label55_true-unreach-call_false-termination.c 1 69   3000 760 0 91    2700 1 39     880  
eca-rers2012/Problem02_label56_true-unreach-call_false-termination.c 1 55   2800 610 0 91    2700 1 40     920  
eca-rers2012/Problem02_label57_true-unreach-call_false-termination.c 1 450   2700 5400 0 92    2600 1 41     970  
eca-rers2012/Problem02_label58_true-unreach-call_false-termination.c 1 71   3000 810 0 92    2500 1 39     890  
eca-rers2012/Problem02_label59_false-unreach-call_false-termination.c 1 49   2400 460 0 91    2500 1 40     870  
eca-rers2012/Problem04_label11_false-unreach-call_false-termination.c 0 910   1700 10000 0 .54 43 0 .019 4.8
eca-rers2012/Problem04_label12_false-unreach-call_false-termination.c 0 910   1500 11000 0 .68 41 0 .018 4.9
eca-rers2012/Problem04_label14_false-unreach-call_false-termination.c 0 910   1500 12000 0 .51 44 0 .021 4.8
eca-rers2012/Problem04_label17_false-unreach-call_false-termination.c 0 910   1600 13000 0 .54 41 0 .018 4.9
eca-rers2012/Problem04_label20_true-unreach-call_false-termination.c 0 910   1400 10000 0 .40 43 0 .019 4.9
eca-rers2012/Problem04_label23_true-unreach-call_false-termination.c 0 910   1500 12000 0 .55 43 0 .019 4.8
eca-rers2012/Problem04_label24_true-unreach-call_false-termination.c 0 910   1400 11000 0 .52 41 0 .022 4.9
eca-rers2012/Problem04_label27_false-unreach-call_false-termination.c 0 910   1400 13000 0 .51 41 0 .018 4.9
eca-rers2012/Problem04_label29_true-unreach-call_false-termination.c 0 910   1500 9700 0 .53 41 0 .019 4.9
eca-rers2012/Problem04_label36_false-unreach-call_false-termination.c 0 910   1700 11000 0 .53 43 0 .019 4.9
eca-rers2012/Problem04_label37_true-unreach-call_false-termination.c 0 910   1200 9700 0 .54 42 0 .018 5.0
eca-rers2012/Problem04_label40_false-unreach-call_false-termination.c 0 910   1400 12000 0 .53 43 0 .037 4.9
eca-rers2012/Problem04_label42_true-unreach-call_false-termination.c 0 910   1400 12000 0 .52 42 0 .019 4.8
eca-rers2012/Problem04_label43_true-unreach-call_false-termination.c 0 910   1500 11000 0 .54 44 0 .020 4.9
eca-rers2012/Problem04_label44_true-unreach-call_false-termination.c 0 910   1900 11000 0 .51 44 0 .020 4.8
eca-rers2012/Problem04_label46_true-unreach-call_false-termination.c 0 910   1600 11000 0 .39 44 0 .018 5.0
eca-rers2012/Problem04_label49_true-unreach-call_false-termination.c 0 910   1400 13000 0 .69 43 0 .018 5.0
eca-rers2012/Problem04_label57_true-unreach-call_false-termination.c 0 910   1400 13000 0 .56 43 0 .020 4.9
eca-rers2012/Problem04_label58_false-unreach-call_false-termination.c 0 910   1600 12000 0 .53 44 0 .021 4.8
eca-rers2012/Problem14_label00_true-unreach-call_false-termination.c 0 900   4100 12000 0 .40 44 0 .019 4.8
eca-rers2012/Problem14_label01_true-unreach-call_false-termination.c 0 900   4200 12000 0 .53 41 0 .019 4.8
eca-rers2012/Problem14_label02_false-unreach-call_false-termination.c 0 910   2500 11000 0 .53 41 0 .019 4.9
eca-rers2012/Problem14_label03_true-unreach-call_false-termination.c 0 910   4200 13000 0 .53 41 0 .020 4.9
eca-rers2012/Problem14_label04_true-unreach-call_false-termination.c 0 900   4100 12000 0 .68 41 0 .019 4.8
eca-rers2012/Problem14_label05_true-unreach-call_false-termination.c 0 910   4100 13000 0 .55 43 0 .019 4.8
eca-rers2012/Problem14_label06_true-unreach-call_false-termination.c 0 900   4200 11000 0 .53 42 0 .018 4.9
eca-rers2012/Problem14_label07_true-unreach-call_false-termination.c 0 910   4100 11000 0 .53 45 0 .019 4.8
eca-rers2012/Problem14_label08_false-unreach-call_false-termination.c 0 910   4100 11000 0 .55 41 0 .019 4.9
eca-rers2012/Problem14_label09_true-unreach-call_false-termination.c 0 910   4200 11000 0 .52 43 0 .020 4.8
eca-rers2012/Problem14_label10_false-unreach-call_false-termination.c 0 900   4100 11000 0 .54 43 0 .018 4.8
eca-rers2012/Problem14_label11_false-unreach-call_false-termination.c 0 900   4200 11000 0 .52 42 0 .018 4.9
eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c 0 900   4100 9900 0 .51 41 0 .024 4.9
eca-rers2012/Problem14_label13_false-unreach-call_false-termination.c 0 900   4100 11000 0 .54 41 0 .036 4.9
eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c 0 900   4300 12000 0 .53 41 0 .019 4.9
eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c 0 900   4100 12000 0 .52 41 0 .023 4.8
eca-rers2012/Problem14_label16_true-unreach-call_false-termination.c 0 910   3900 11000 0 .52 43 0 .018 4.8
eca-rers2012/Problem14_label17_true-unreach-call_false-termination.c 0 910   4100 11000 0 .52 43 0 .019 4.8
eca-rers2012/Problem14_label18_false-unreach-call_false-termination.c 0 910   4100 11000 0 .69 44 0 .019 4.9
eca-rers2012/Problem14_label19_true-unreach-call_false-termination.c 0 910   2600 13000 0 .50 43 0 .020 5.0
eca-rers2012/Problem14_label20_true-unreach-call_false-termination.c 0 900   4100 12000 0 .55 43 0 .018 4.8
eca-rers2012/Problem14_label21_true-unreach-call_false-termination.c 0 910   4200 12000 0 .55 41 0 .018 4.8
eca-rers2012/Problem14_label22_false-unreach-call_false-termination.c 0 910   3800 12000 0 .70 42 0 .019 4.8
eca-rers2012/Problem14_label23_true-unreach-call_false-termination.c 0 910   2500 11000 0 .70 43 0 .020 4.8
eca-rers2012/Problem14_label24_true-unreach-call_false-termination.c 0 910   4200 9100 0 .52 42 0 .019 4.9
eca-rers2012/Problem14_label25_true-unreach-call_false-termination.c 0 900   4100 11000 0 .60 43 0 .019 4.8
eca-rers2012/Problem14_label26_true-unreach-call_false-termination.c 0 900   4100 11000 0 .53 43 0 .020 4.8
eca-rers2012/Problem14_label27_false-unreach-call_false-termination.c 0 910   4100 11000 0 .70 42 0 .019 4.9
eca-rers2012/Problem14_label28_false-unreach-call_false-termination.c 0 900   4000 8900 0 .52 41 0 .018 5.0
eca-rers2012/Problem14_label29_false-unreach-call_false-termination.c 0 900   4100 13000 0 .51 41 0 .020 5.0
eca-rers2012/Problem14_label30_true-unreach-call_false-termination.c 0 900   4100 9900 0 .54 41 0 .021 4.9
eca-rers2012/Problem14_label31_false-unreach-call_false-termination.c 0 900   4100 11000 0 .52 43 0 .020 4.8
eca-rers2012/Problem14_label32_true-unreach-call_false-termination.c 0 910   4100 12000 0 .53 43 0 .018 5.0
eca-rers2012/Problem14_label33_true-unreach-call_false-termination.c 0 900   4100 11000 0 .40 44 0 .020 4.9
eca-rers2012/Problem14_label34_false-unreach-call_false-termination.c 0 910   4200 11000 0 .54 43 0 .019 4.9
eca-rers2012/Problem14_label35_true-unreach-call_false-termination.c 0 900   4200 11000 0 .52 43 0 .019 5.0
eca-rers2012/Problem14_label36_true-unreach-call_false-termination.c 0 910   4200 14000 0 .72 43 0 .019 4.8
eca-rers2012/Problem14_label37_false-unreach-call_false-termination.c 0 910   4200 11000 0 .52 43 0 .018 4.9
eca-rers2012/Problem14_label38_true-unreach-call_false-termination.c 0 910   4100 11000 0 .52 43 0 .018 4.9
eca-rers2012/Problem14_label39_false-unreach-call_false-termination.c 0 900   4300 13000 0 .62 43 0 .019 4.9
eca-rers2012/Problem14_label40_false-unreach-call_false-termination.c 0 900   4000 10000 0 .51 43 0 .020 4.8
eca-rers2012/Problem14_label41_false-unreach-call_false-termination.c 0 910   4200 13000 0 .54 44 0 .025 4.9
eca-rers2012/Problem14_label42_true-unreach-call_false-termination.c 0 910   4200 11000 0 .70 41 0 .018 4.8
eca-rers2012/Problem14_label43_false-unreach-call_false-termination.c 0 900   4100 11000 0 .55 41 0 .019 4.8
eca-rers2012/Problem14_label44_false-unreach-call_false-termination.c 0 910   2800 12000 0 .50 41 0 .018 4.8
eca-rers2012/Problem14_label45_true-unreach-call_false-termination.c 0 900   4200 12000 0 .52 43 0 .019 5.0
eca-rers2012/Problem14_label46_true-unreach-call_false-termination.c 0 910   2700 12000 0 .56 43 0 .019 4.9
eca-rers2012/Problem14_label47_true-unreach-call_false-termination.c 0 900   4100 12000 0 .54 41 0 .020 5.0
eca-rers2012/Problem14_label48_true-unreach-call_false-termination.c 0 910   4200 13000 0 .52 43 0 .019 4.9
eca-rers2012/Problem14_label49_true-unreach-call_false-termination.c 0 900   4100 10000 0 .70 43 0 .024 4.9
eca-rers2012/Problem14_label50_true-unreach-call_false-termination.c 0 910   4200 13000 0 .54 43 0 .019 4.9
eca-rers2012/Problem14_label51_true-unreach-call_false-termination.c 0 900   4100 9900 0 .51 41 0 .018 4.9
eca-rers2012/Problem14_label52_false-unreach-call_false-termination.c 0 910   4100 11000 0 .66 43 0 .018 4.8
eca-rers2012/Problem14_label53_true-unreach-call_false-termination.c 0 910   4100 11000 0 .66 41 0 .019 4.8
eca-rers2012/Problem14_label54_false-unreach-call_false-termination.c 0 910   3900 11000 0 .54 41 0 .019 4.9
eca-rers2012/Problem14_label55_true-unreach-call_false-termination.c 0 910   4100 11000 0 .62 43 0 .018 4.8
eca-rers2012/Problem14_label56_false-unreach-call_false-termination.c 0 910   4100 12000 0 .51 43 0 .019 4.9
eca-rers2012/Problem14_label57_false-unreach-call_false-termination.c 0 900   4100 12000 0 .55 43 0 .019 4.8
eca-rers2012/Problem14_label58_false-unreach-call_false-termination.c 0 910   4200 12000 0 .49 44 0 .035 4.8
eca-rers2012/Problem14_label59_true-unreach-call_false-termination.c 0 900   2700 11000 0 .53 42 0 .018 4.9
eca-rers2012/Problem15_label18_false-unreach-call_false-termination.c 0 910   1300 11000 0 .72 41 0 .030 4.8
psyco/psyco_abp_1_false-unreach-call_false-termination.c - 0 .40 44 0 .019 5.0
psyco/psyco_accelerometer_1_true-unreach-call_false-termination.c 1 70   3600 550 0 94    2100 1 30     960