Tool ULTIMATE Automizer 0.1.23-635dfa2a CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET
Run set uautomizer.sv-comp19_prop-termination.Termination-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 --- inspect 11   4.4 500 100 .66 0      - --- inspect - --- inspect
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 --- inspect 16   5.4 530 140 .66 0      - --- inspect - --- inspect
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 --- inspect 9.7 3.2 380 79 .66 0      - --- inspect - --- inspect
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i true 2 --- inspect 11   3.6 470 84 .66 0      - --- inspect - --- inspect
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i true 2 --- inspect 13   4.5 500 100 .66 0      - --- inspect - --- inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i timeout 0 --- inspect 900   870   810 10000 .63 0      - --- inspect - --- inspect
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i timeout 0 --- inspect 900   870   810 11000 .63 0      - --- inspect - --- inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i true 2 --- inspect 11   4.0 470 98 .66 .14   - --- inspect - --- inspect
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true 2 --- inspect 11   3.5 490 93 .66 0      - --- inspect - --- inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i true 2 --- inspect 10   3.7 460 90 .66 0      - --- inspect - --- inspect
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i false(termination) 1 wit inspect 7.7 2.6 370 57 .66 0      false(termination) 1 --- inspect 4.9  2.7  240 .033  0      false(termination) 1 --- inspect 7.3   4.2   310   .62  0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i false(termination) 1 wit inspect 7.9 3.0 380 67 .66 0      false(termination) 1 --- inspect 3.9  2.2  250 .033  0      false(termination) 1 --- inspect 7.5   4.7   310   .62  0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i false(termination) 1 wit inspect 7.9 2.7 360 62 .66 0      false(termination) 1 --- inspect 5.1  2.8  250 .033  0      false(termination) 1 --- inspect 7.6   4.8   310   .66  0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i false(termination) 1 wit inspect 8.2 3.1 370 57 .66 0      false(termination) 1 --- inspect 5.0  2.7  250 .033  0      false(termination) 1 --- inspect 7.3   4.6   310   .66  0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i false(termination) 1 wit inspect 8.0 2.6 360 58 .66 0      false(termination) 1 --- inspect 4.1  2.3  250 .033  0      false(termination) 1 --- inspect 7.4   4.5   300   .62  .0041
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i error (7) 0 --- inspect 130   99   1600 1400 .62 0      - --- inspect - --- inspect
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 --- inspect 110   83   940 1300 .62 0      - --- inspect - --- inspect
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 --- inspect 66   34   930 660 .62 0      - --- inspect - --- inspect
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 --- inspect 15   5.4 570 130 .66 0      - --- inspect - --- inspect
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c false(termination) 1 wit inspect 15   5.2 560 130 .66 0      false(termination) 1 wit inspect 43    22    1600 .0082 0      false(termination) 1 --- inspect 19     12     540   .62  0     
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c false(termination) 1 wit inspect 14   4.4 560 120 .66 0      false(termination) 1 wit inspect 60    30    1600 .0082 0      false(termination) 1 --- inspect 19     12     550   .62  0     
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 --- inspect 13   4.6 490 95 .66 0      - --- inspect - --- inspect
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 --- inspect 13   4.8 550 110 .66 0      - --- inspect - --- inspect
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 --- inspect 13   4.8 520 120 .66 0      - --- inspect - --- inspect
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 --- inspect 12   4.5 480 97 .66 0      - --- inspect - --- inspect
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 --- inspect 12   5.0 490 120 .66 0      - --- inspect - --- inspect
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c true 2 --- inspect 6.8 2.8 330 53 .66 0      - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c true 2 --- inspect 6.9 2.4 340 53 .65 .0041 - --- inspect - --- inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 --- inspect 7.9 2.6 350 63 .65 0      - --- inspect - --- inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c true 2 --- inspect 7.8 2.6 360 55 .66 0      - --- inspect - --- inspect
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 --- inspect 7.4 2.5 360 64 .66 0      - --- inspect - --- inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c true 2 --- inspect 9.8 3.7 390 79 .66 0      - --- inspect - --- inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c true 2 --- inspect 7.4 2.5 360 64 .66 .12   - --- inspect - --- inspect
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 --- inspect 7.9 2.6 370 60 .66 0      - --- inspect - --- inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c true 2 --- inspect 7.4 2.5 360 52 .66 0      - --- inspect - --- inspect
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 --- inspect 7.9 2.9 350 65 .66 0      - --- inspect - --- inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i true 2 --- inspect 23   12   510 220 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 18   5.3 550 150 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 17   5.2 590 130 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 13   4.3 480 95 .66 .38   - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 15   4.4 520 110 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 15   4.6 610 110 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 16   4.8 590 130 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 16   4.9 590 120 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 9.3 3.3 360 70 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 10   3.1 380 81 .66 0      - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 --- inspect 10   3.2 390 76 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 66   36   1200 680 .62 0      timeout 0 --- inspect 92    47    2000 .0082 0      false(termination) 1 --- inspect 23     14     830   .62  0     
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 45   15   1100 390 .66 0      timeout 0 --- inspect 92    51    2100 .0082 0      false(termination) 1 --- inspect 24     14     790   .62  0     
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 48   16   1400 420 .66 0      timeout 0 --- inspect 91    53    2000 .0082 0      false(termination) 1 --- inspect 28     16     830   .62  0     
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 42   14   1100 360 .66 0      timeout 0 --- inspect 92    57    1400 .0082 0      false(termination) 1 --- inspect 24     14     780   .62  .0041
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 55   19   1600 450 .66 .35   timeout 0 --- inspect 92    54    2000 .0082 0      false(termination) 1 --- inspect 60     50     890   .62  0     
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 36   10   870 310 .66 0      timeout 0 --- inspect 91    47    2100 .0082 0      false(termination) 1 --- inspect 22     13     790   .62  0     
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 38   12   1100 330 .66 0      timeout 0 --- inspect 91    48    2100 .0082 0      false(termination) 1 --- inspect 23     14     690   .62  0     
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 18   5.9 690 150 .66 0      false(termination) 1 wit inspect 40    21    810 .0082 0      false(termination) 1 --- inspect 14     8.4   520   .62  .58  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 11   4.0 470 82 .66 0      false(termination) 1 wit inspect 12    6.0  430 .0082 0      false(termination) 1 --- inspect 11     6.8   380   .62  .0082
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 37   11   940 310 .66 0      timeout 0 --- inspect 93    51    2100 .0082 0      false(termination) 1 --- inspect 22     13     800   .62  .045 
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 48   16   1500 440 .66 0      timeout 0 --- inspect 92    47    2000 .0082 0      false(termination) 1 --- inspect 22     13     780   .62  0     
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 41   13   1100 320 .66 1.0    timeout 0 --- inspect 92    47    2100 .0082 0      false(termination) 1 --- inspect 23     13     690   .62  .049 
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 41   13   1300 350 .66 0      timeout 0 --- inspect 92    47    2000 .0082 0      false(termination) 1 --- inspect 22     12     780   .62  0     
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 47   13   1300 360 .66 0      timeout 0 --- inspect 92    49    2100 .0082 .049  false(termination) 1 --- inspect 25     15     830   .62  0     
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 45   13   1300 390 .66 0      timeout 0 --- inspect 92    48    2100 .0082 1.1    false(termination) 1 --- inspect 25     14     810   .62  0     
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 38   12   1200 320 .66 0      timeout 0 --- inspect 92    46    2000 .0082 1.1    false(termination) 1 --- inspect 24     14     790   .62  0     
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c false(termination) 1 wit inspect 44   14   1100 390 .66 0      timeout 0 --- inspect 92    47    2100 .0082 0      false(termination) 1 --- inspect 22     12     780   .62  0     
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c true 2 --- inspect 29   8.2 900 240 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 --- inspect 28   8.1 810 220 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c true 2 --- inspect 35   10   1000 290 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 --- inspect 35   10   1000 280 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c true 2 --- inspect 36   11   880 300 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 --- inspect 60   19   1200 490 .62 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c true 2 --- inspect 36   11   920 290 .66 0      - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 --- inspect 36   11   900 280 .66 0      - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 13   3.9 500 120 .66 0      false(termination) 1 wit inspect 41    27    1200 .033  0      false(termination) 1 --- inspect 14     7.9   550   .66  .0041
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 13   4.0 590 110 .66 0      false(termination) 1 wit inspect 46    32    1300 .033  0      false(termination) 1 --- inspect 14     8.1   550   .62  .0041
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 16   4.6 790 120 .66 .0082 false(termination) 1 wit inspect 60    44    1700 .033  0      false(termination) 1 --- inspect 18     9.9   640   .62  0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 18   5.8 1000 160 .66 0      false(termination) 1 wit inspect 74    58    1900 .033  .0082 false(termination) 1 --- inspect 21     11     1200   .62  0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 16   4.9 830 130 .66 0      false(termination) 1 wit inspect 83    64    2100 .033  0      false(termination) 1 --- inspect 17     9.8   740   .62  0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 28   9.2 2300 220 .66 0      timeout (false(termination)) 0 wit inspect 91    72    2200 .033  0      false(termination) 1 --- inspect 28     16     2400   .62  .19  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 20   6.2 1300 160 .66 0      false(termination) 1 wit inspect 79    63    2100 .033  0      false(termination) 1 --- inspect 23     12     1200   .62  0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 49   16   3600 300 .66 0      timeout 0 --- inspect 92    77    2300 .033  0      false(termination) 1 --- inspect 46     28     3800   .62  0     
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 9.3 3.4 360 73 .66 0      false(termination) 1 wit inspect 15    8.0  450 .033  0      false(termination) 1 --- inspect 8.9   5.0   310   .62  0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 9.1 3.3 380 69 .66 0      false(termination) 1 wit inspect 18    9.5  560 .033  0      false(termination) 1 --- inspect 9.5   5.4   320   .23  .0041
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 9.8 3.2 380 75 .66 0      false(termination) 1 wit inspect 22    12    640 .033  .0082 false(termination) 1 --- inspect 10     5.7   320   .66  0     
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 11   3.5 440 90 .66 .0041 false(termination) 1 wit inspect 33    19    830 .033  0      false(termination) 1 --- inspect 11     6.2   380   .62  0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c false(termination) 1 wit inspect 11   3.4 510 100 .66 0      false(termination) 1 wit inspect 29    18    830 .033  0      false(termination) 1 --- inspect 12     7.1   470   .62  .0041
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c true 2 --- inspect 38   12   960 300 .66 0      - --- inspect - --- inspect
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c true 2 --- inspect 75   49   1100 870 .62 0      - --- inspect - --- inspect
eca-rers2012/Problem01_label00_true-unreach-call_false-termination.c timeout 0 --- inspect 910   160   13000 4300 .63 0      error (invalid witness file) 0 --- inspect .61 .36 42 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem01_label01_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4300 .63 0      error (invalid witness file) 0 --- inspect .60 .36 40 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label02_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4000 .63 0      error (invalid witness file) 0 --- inspect .61 .37 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label03_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4300 .63 0      error (invalid witness file) 0 --- inspect .57 .36 40 0      0      error (2) 0 --- inspect .022 .024 5.7 0     0     
eca-rers2012/Problem01_label04_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4300 .63 0      error (invalid witness file) 0 --- inspect .66 .42 40 0      0      error (2) 0 --- inspect .021 .021 5.7 0     0     
eca-rers2012/Problem01_label05_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4400 .63 0      error (invalid witness file) 0 --- inspect .62 .38 43 0      0      error (2) 0 --- inspect .023 .024 5.6 0     0     
eca-rers2012/Problem01_label06_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4800 .63 0      error (invalid witness file) 0 --- inspect .66 .40 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label07_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 0      error (invalid witness file) 0 --- inspect .72 .44 41 0      0      error (2) 0 --- inspect .025 .025 5.6 0     0     
eca-rers2012/Problem01_label08_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4900 .63 0      error (invalid witness file) 0 --- inspect .90 .56 42 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label09_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4300 .63 0      error (invalid witness file) 0 --- inspect .71 .43 42 0      0      error (2) 0 --- inspect .023 .025 5.7 0     0     
eca-rers2012/Problem01_label10_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4100 .63 0      error (invalid witness file) 0 --- inspect .62 .39 43 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label11_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 .025  error (invalid witness file) 0 --- inspect .73 .47 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label12_true-unreach-call_false-termination.c timeout 0 --- inspect 900   150   13000 4200 .63 0      error (invalid witness file) 0 --- inspect .70 .43 41 0      0      error (2) 0 --- inspect .022 .022 5.6 0     0     
eca-rers2012/Problem01_label13_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4700 .63 0      error (invalid witness file) 0 --- inspect .75 .46 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label14_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4800 .63 0      error (invalid witness file) 0 --- inspect .60 .38 40 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label15_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4400 .63 0      error (invalid witness file) 0 --- inspect .62 .38 42 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label16_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4400 .63 0      error (invalid witness file) 0 --- inspect .75 .47 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label17_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4900 .63 0      error (invalid witness file) 0 --- inspect .71 .44 40 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label18_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 0      error (invalid witness file) 0 --- inspect .60 .38 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label19_true-unreach-call_false-termination.c timeout 0 --- inspect 900   160   14000 4800 .63 0      error (invalid witness file) 0 --- inspect .60 .36 41 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label20_false-unreach-call_false-termination.c timeout 0 --- inspect 900   150   13000 4100 .63 0      error (invalid witness file) 0 --- inspect .59 .36 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label21_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4200 .63 0      error (invalid witness file) 0 --- inspect .67 .42 40 0      0      error (2) 0 --- inspect .022 .025 5.6 0     0     
eca-rers2012/Problem01_label22_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4600 .63 0      error (invalid witness file) 0 --- inspect .68 .42 40 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label23_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .77 .47 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label24_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4000 .63 0      error (invalid witness file) 0 --- inspect .84 .52 42 0      0      error (2) 0 --- inspect .022 .024 5.6 0     0     
eca-rers2012/Problem01_label25_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4200 .63 0      error (invalid witness file) 0 --- inspect .71 .44 41 0      0      error (2) 0 --- inspect .023 .024 5.6 0     0     
eca-rers2012/Problem01_label26_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .59 .35 41 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label27_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4300 .63 0      error (invalid witness file) 0 --- inspect .61 .39 40 0      0      error (2) 0 --- inspect .021 .032 5.6 0     0     
eca-rers2012/Problem01_label28_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4300 .63 0      error (invalid witness file) 0 --- inspect .74 .45 42 0      0      error (2) 0 --- inspect .024 .024 5.6 0     0     
eca-rers2012/Problem01_label29_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4400 .63 .71   error (invalid witness file) 0 --- inspect .70 .44 42 0      0      error (2) 0 --- inspect .020 .021 5.7 0     0     
eca-rers2012/Problem01_label30_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .59 .37 41 0      0      error (2) 0 --- inspect .024 .024 5.6 0     0     
eca-rers2012/Problem01_label31_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4800 .63 0      error (invalid witness file) 0 --- inspect .64 .39 40 0      0      error (2) 0 --- inspect .024 .026 5.6 0     0     
eca-rers2012/Problem01_label32_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 0      error (invalid witness file) 0 --- inspect .73 .46 41 0      0      error (2) 0 --- inspect .021 .022 5.7 0     0     
eca-rers2012/Problem01_label33_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .75 .46 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label34_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4100 .63 0      error (invalid witness file) 0 --- inspect .77 .47 43 0      0      error (2) 0 --- inspect .021 .022 5.7 0     0     
eca-rers2012/Problem01_label35_false-unreach-call_false-termination.c timeout 0 --- inspect 910   160   13000 4500 .63 0      error (invalid witness file) 0 --- inspect .70 .43 42 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label36_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4900 .63 0      error (invalid witness file) 0 --- inspect .74 .46 40 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem01_label37_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4700 .63 0      error (invalid witness file) 0 --- inspect .70 .43 42 0      0      error (2) 0 --- inspect .025 .026 5.7 0     0     
eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4800 .63 0      error (invalid witness file) 0 --- inspect .75 .47 41 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label39_true-unreach-call_false-termination.c timeout 0 --- inspect 910   160   14000 4900 .63 .13   error (invalid witness file) 0 --- inspect .77 .46 40 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem01_label40_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .76 .47 41 0      0      error (2) 0 --- inspect .021 .023 5.6 0     0     
eca-rers2012/Problem01_label41_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 .89   error (invalid witness file) 0 --- inspect .75 .46 40 0      0      error (2) 0 --- inspect .024 .025 5.6 0     0     
eca-rers2012/Problem01_label42_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4300 .63 0      error (invalid witness file) 0 --- inspect .64 .40 42 0      0      error (2) 0 --- inspect .022 .024 5.7 0     0     
eca-rers2012/Problem01_label43_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4800 .63 .42   error (invalid witness file) 0 --- inspect .72 .46 40 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem01_label44_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 5100 .63 0      error (invalid witness file) 0 --- inspect .74 .46 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label45_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4500 .63 0      error (invalid witness file) 0 --- inspect .61 .38 41 0      0      error (2) 0 --- inspect .022 .025 5.6 0     0     
eca-rers2012/Problem01_label46_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4300 .63 0      error (invalid witness file) 0 --- inspect .60 .37 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label47_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4100 .63 .95   error (invalid witness file) 0 --- inspect .66 .41 40 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem01_label48_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4500 .63 0      error (invalid witness file) 0 --- inspect .64 .40 42 0      0      error (2) 0 --- inspect .023 .025 5.7 0     0     
eca-rers2012/Problem01_label49_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4200 .63 0      error (invalid witness file) 0 --- inspect .62 .39 41 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem01_label50_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 0      error (invalid witness file) 0 --- inspect .69 .44 42 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem01_label51_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4400 .63 0      error (invalid witness file) 0 --- inspect .77 .46 42 0      0      error (2) 0 --- inspect .027 .028 5.6 0     0     
eca-rers2012/Problem01_label52_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4700 .63 0      error (invalid witness file) 0 --- inspect .79 .49 43 0      0      error (2) 0 --- inspect .028 .030 5.6 0     0     
eca-rers2012/Problem01_label53_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4000 .62 .16   error (invalid witness file) 0 --- inspect .62 .39 41 0      0      error (2) 0 --- inspect .021 .022 5.7 0     0     
eca-rers2012/Problem01_label54_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4400 .63 0      error (invalid witness file) 0 --- inspect .73 .46 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label55_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4800 .63 0      error (invalid witness file) 0 --- inspect .62 .39 42 0      0      error (2) 0 --- inspect .021 .022 5.7 0     0     
eca-rers2012/Problem01_label56_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 5000 .63 0      error (invalid witness file) 0 --- inspect .65 .39 42 0      0      error (2) 0 --- inspect .022 .024 5.6 0     0     
eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4900 .63 0      error (invalid witness file) 0 --- inspect .76 .45 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem01_label58_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   13000 4500 .63 0      error (invalid witness file) 0 --- inspect .76 .46 43 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem01_label59_true-unreach-call_false-termination.c timeout 0 --- inspect 910   150   14000 4200 .63 0      error (invalid witness file) 0 --- inspect .71 .43 40 0      0      error (2) 0 --- inspect .025 .026 5.6 0     0     
eca-rers2012/Problem02_label00_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   850 280 .66 0      unknown 0 --- inspect 22    11    570 .0082 0      false(termination) 1 --- inspect 20     12     520   .62  0     
eca-rers2012/Problem02_label01_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   850 270 .66 0      unknown 0 --- inspect 24    12    570 .0082 0      false(termination) 1 --- inspect 19     11     480   .62  0     
eca-rers2012/Problem02_label02_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   770 290 .66 0      unknown 0 --- inspect 24    12    580 .0082 0      false(termination) 1 --- inspect 19     11     490   .66  .14  
eca-rers2012/Problem02_label03_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   840 260 .66 0      unknown 0 --- inspect 24    12    560 .0082 .016  false(termination) 1 --- inspect 20     11     500   .62  .18  
eca-rers2012/Problem02_label04_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   850 250 .66 0      unknown 0 --- inspect 21    11    580 .0082 0      false(termination) 1 --- inspect 20     11     490   .62  .14  
eca-rers2012/Problem02_label05_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   760 270 .66 0      unknown 0 --- inspect 22    11    570 .0082 .025  false(termination) 1 --- inspect 20     12     500   .62  0     
eca-rers2012/Problem02_label06_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   830 260 .66 0      unknown 0 --- inspect 23    12    580 .0082 0      false(termination) 1 --- inspect 18     11     520   .62  0     
eca-rers2012/Problem02_label07_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   850 230 .66 0      unknown 0 --- inspect 24    12    570 .0082 0      false(termination) 1 --- inspect 19     11     510   .62  0     
eca-rers2012/Problem02_label08_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   790 270 .66 0      unknown 0 --- inspect 20    10    590 .0082 0      false(termination) 1 --- inspect 17     9.8   490   .62  0     
eca-rers2012/Problem02_label09_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   820 260 .66 .025  unknown 0 --- inspect 21    11    560 .0082 0      false(termination) 1 --- inspect 19     11     490   .62  0     
eca-rers2012/Problem02_label10_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   11   790 290 .66 0      unknown 0 --- inspect 21    11    590 .0082 0      false(termination) 1 --- inspect 17     9.9   500   .62  0     
eca-rers2012/Problem02_label11_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   850 290 .66 .30   unknown 0 --- inspect 23    12    600 .0082 0      false(termination) 1 --- inspect 17     10     520   .62  0     
eca-rers2012/Problem02_label12_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   11   820 310 .66 0      unknown 0 --- inspect 24    12    560 .0082 0      false(termination) 1 --- inspect 19     11     520   .62  0     
eca-rers2012/Problem02_label13_false-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   770 260 .66 0      unknown 0 --- inspect 24    12    590 .0082 0      false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label14_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   750 250 .66 0      unknown 0 --- inspect 24    12    620 .0082 0      false(termination) 1 --- inspect 19     11     470   .62  0     
eca-rers2012/Problem02_label15_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   770 250 .66 .48   unknown 0 --- inspect 24    13    580 .0082 0      false(termination) 1 --- inspect 17     9.6   520   .62  0     
eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   840 260 .66 .16   unknown 0 --- inspect 24    12    580 .0082 0      false(termination) 1 --- inspect 18     10     510   .62  0     
eca-rers2012/Problem02_label17_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   11   770 290 .66 0      unknown 0 --- inspect 24    12    530 .0082 .053  false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label18_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   860 300 .66 0      unknown 0 --- inspect 21    11    590 .0082 0      false(termination) 1 --- inspect 18     10     500   .62  0     
eca-rers2012/Problem02_label19_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   11   830 260 .66 0      unknown 0 --- inspect 23    12    580 .0082 0      false(termination) 1 --- inspect 18     10     490   .62  0     
eca-rers2012/Problem02_label20_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   830 300 .66 .48   unknown 0 --- inspect 24    12    610 .0082 0      false(termination) 1 --- inspect 18     10     490   .62  0     
eca-rers2012/Problem02_label21_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   840 270 .66 0      unknown 0 --- inspect 24    12    560 .0082 0      false(termination) 1 --- inspect 18     10     500   .66  0     
eca-rers2012/Problem02_label22_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   840 250 .62 0      unknown 0 --- inspect 25    13    560 .0082 0      false(termination) 1 --- inspect 18     11     510   .62  0     
eca-rers2012/Problem02_label23_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   830 260 .66 .025  unknown 0 --- inspect 19    9.7  570 .0082 0      false(termination) 1 --- inspect 19     11     510   .62  0     
eca-rers2012/Problem02_label24_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   850 270 .66 0      unknown 0 --- inspect 18    9.5  570 .0082 0      false(termination) 1 --- inspect 19     11     530   .62  0     
eca-rers2012/Problem02_label25_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   780 270 .66 0      unknown 0 --- inspect 24    12    580 .0082 0      false(termination) 1 --- inspect 16     9.8   520   .62  0     
eca-rers2012/Problem02_label26_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   840 290 .66 0      unknown 0 --- inspect 23    12    560 .0082 0      false(termination) 1 --- inspect 18     10     490   .62  0     
eca-rers2012/Problem02_label27_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   840 270 .66 0      unknown 0 --- inspect 23    12    580 .0082 .025  false(termination) 1 --- inspect 19     11     510   .62  .0041
eca-rers2012/Problem02_label28_true-unreach-call_false-termination.c false(termination) 1 wit inspect 31   10   780 260 .66 0      unknown 0 --- inspect 21    11    580 .0082 1.0    false(termination) 1 --- inspect 19     11     510   .62  0     
eca-rers2012/Problem02_label29_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   770 250 .66 0      unknown 0 --- inspect 21    11    580 .0082 0      false(termination) 1 --- inspect 19     11     520   .62  0     
eca-rers2012/Problem02_label30_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   840 250 .66 0      unknown 0 --- inspect 23    12    570 .0082 0      false(termination) 1 --- inspect 18     11     490   .62  0     
eca-rers2012/Problem02_label31_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   830 270 .66 0      unknown 0 --- inspect 24    12    560 .0082 0      false(termination) 1 --- inspect 19     11     520   .62  0     
eca-rers2012/Problem02_label32_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   780 270 .66 0      unknown 0 --- inspect 22    11    590 .0082 0      false(termination) 1 --- inspect 18     10     510   .62  0     
eca-rers2012/Problem02_label33_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   11   840 270 .66 0      unknown 0 --- inspect 20    10    600 .0082 0      false(termination) 1 --- inspect 20     11     510   .62  .0041
eca-rers2012/Problem02_label34_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   830 300 .62 0      unknown 0 --- inspect 21    11    570 .0082 0      false(termination) 1 --- inspect 19     11     520   .62  0     
eca-rers2012/Problem02_label35_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   830 270 .66 0      unknown 0 --- inspect 23    12    560 .0082 0      false(termination) 1 --- inspect 18     10     490   .62  .025 
eca-rers2012/Problem02_label36_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   800 270 .66 0      unknown 0 --- inspect 25    13    590 .0082 1.1    false(termination) 1 --- inspect 19     11     510   .62  0     
eca-rers2012/Problem02_label37_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   770 270 .66 0      unknown 0 --- inspect 21    11    570 .0082 .041  false(termination) 1 --- inspect 18     10     500   .66  0     
eca-rers2012/Problem02_label38_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   850 270 .66 0      unknown 0 --- inspect 26    13    590 .0082 0      false(termination) 1 --- inspect 20     11     520   .62  0     
eca-rers2012/Problem02_label39_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   850 260 .66 .57   unknown 0 --- inspect 23    12    570 .0082 .025  false(termination) 1 --- inspect 18     11     490   .62  0     
eca-rers2012/Problem02_label40_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   750 310 .66 0      unknown 0 --- inspect 23    12    560 .0082 0      false(termination) 1 --- inspect 17     9.9   500   .62  0     
eca-rers2012/Problem02_label41_true-unreach-call_false-termination.c false(termination) 1 wit inspect 31   10   830 260 .66 .025  unknown 0 --- inspect 24    12    570 .0082 0      false(termination) 1 --- inspect 17     10     520   .62  0     
eca-rers2012/Problem02_label42_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   11   840 270 .62 0      unknown 0 --- inspect 23    12    590 .0082 1.1    false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label43_false-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   840 290 .66 0      unknown 0 --- inspect 22    12    580 .0082 0      false(termination) 1 --- inspect 19     11     510   .62  0     
eca-rers2012/Problem02_label44_false-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   780 290 .66 0      unknown 0 --- inspect 25    13    570 .0082 0      false(termination) 1 --- inspect 19     11     510   .62  .0041
eca-rers2012/Problem02_label45_false-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   860 270 .66 0      unknown 0 --- inspect 19    9.6  560 .0082 .82   false(termination) 1 --- inspect 21     12     520   .62  0     
eca-rers2012/Problem02_label46_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   780 280 .66 0      unknown 0 --- inspect 23    12    600 .0082 .025  false(termination) 1 --- inspect 17     10     500   .62  .48  
eca-rers2012/Problem02_label47_true-unreach-call_false-termination.c false(termination) 1 wit inspect 31   10   770 270 .66 0      unknown 0 --- inspect 20    10    570 .0082 1.1    false(termination) 1 --- inspect 19     11     510   .62  .025 
eca-rers2012/Problem02_label48_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   11   850 290 .66 0      unknown 0 --- inspect 21    11    600 .0082 0      false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label49_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   11   840 260 .66 0      unknown 0 --- inspect 23    12    570 .0082 0      false(termination) 1 --- inspect 18     10     500   .62  0     
eca-rers2012/Problem02_label50_false-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   840 280 .66 0      unknown 0 --- inspect 21    11    580 .0082 0      false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label51_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   10   770 290 .66 0      unknown 0 --- inspect 22    11    580 .0082 0      false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label52_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   790 250 .66 0      unknown 0 --- inspect 20    10    580 .0082 0      false(termination) 1 --- inspect 18     10     490   .62  .52  
eca-rers2012/Problem02_label53_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   850 290 .66 0      unknown 0 --- inspect 20    10    580 .0082 .025  false(termination) 1 --- inspect 18     10     520   .62  0     
eca-rers2012/Problem02_label54_true-unreach-call_false-termination.c false(termination) 1 wit inspect 34   10   860 300 .66 0      unknown 0 --- inspect 25    13    550 .0082 0      false(termination) 1 --- inspect 17     10     520   .62  0     
eca-rers2012/Problem02_label55_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   830 280 .66 0      unknown 0 --- inspect 21    11    590 .0082 0      false(termination) 1 --- inspect 20     11     490   .62  .025 
eca-rers2012/Problem02_label56_true-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   840 270 .66 0      unknown 0 --- inspect 24    12    580 .0082 0      false(termination) 1 --- inspect 18     11     520   .62  0     
eca-rers2012/Problem02_label57_true-unreach-call_false-termination.c false(termination) 1 wit inspect 32   11   790 270 .66 0      unknown 0 --- inspect 26    13    560 .0082 1.1    false(termination) 1 --- inspect 18     11     500   .62  0     
eca-rers2012/Problem02_label58_true-unreach-call_false-termination.c false(termination) 1 wit inspect 35   10   830 270 .66 .88   unknown 0 --- inspect 23    12    590 .0082 0      false(termination) 1 --- inspect 20     11     500   .62  0     
eca-rers2012/Problem02_label59_false-unreach-call_false-termination.c false(termination) 1 wit inspect 33   10   850 270 .66 0      unknown 0 --- inspect 19    9.6  610 .0082 0      false(termination) 1 --- inspect 17     10     520   .62  0     
eca-rers2012/Problem04_label11_false-unreach-call_false-termination.c timeout 0 --- inspect 910   310   14000 6800 .63 0      error (invalid witness file) 0 --- inspect .76 .47 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label12_false-unreach-call_false-termination.c timeout 0 --- inspect 910   290   14000 5700 .63 0      error (invalid witness file) 0 --- inspect .59 .37 41 0      0      error (2) 0 --- inspect .023 .026 5.6 0     0     
eca-rers2012/Problem04_label14_false-unreach-call_false-termination.c timeout 0 --- inspect 910   310   14000 6200 .62 0      error (invalid witness file) 0 --- inspect .60 .37 41 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem04_label17_false-unreach-call_false-termination.c timeout 0 --- inspect 910   290   14000 5500 .63 0      error (invalid witness file) 0 --- inspect .58 .36 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label20_true-unreach-call_false-termination.c timeout 0 --- inspect 910   290   14000 5700 .62 0      error (invalid witness file) 0 --- inspect .62 .39 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label23_true-unreach-call_false-termination.c timeout 0 --- inspect 910   320   13000 7400 .63 0      error (invalid witness file) 0 --- inspect .77 .47 41 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem04_label24_true-unreach-call_false-termination.c timeout 0 --- inspect 910   260   14000 5700 .63 0      error (invalid witness file) 0 --- inspect .61 .38 40 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem04_label27_false-unreach-call_false-termination.c timeout 0 --- inspect 910   280   14000 6000 .62 0      error (invalid witness file) 0 --- inspect .78 .47 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label29_true-unreach-call_false-termination.c timeout 0 --- inspect 900   310   13000 6800 .63 0      error (invalid witness file) 0 --- inspect .59 .37 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label36_false-unreach-call_false-termination.c timeout 0 --- inspect 910   300   14000 6200 .62 0      error (invalid witness file) 0 --- inspect .62 .38 42 0      0      error (2) 0 --- inspect .022 .022 5.6 0     0     
eca-rers2012/Problem04_label37_true-unreach-call_false-termination.c timeout 0 --- inspect 910   310   14000 5500 .63 0      error (invalid witness file) 0 --- inspect .61 .38 41 0      0      error (2) 0 --- inspect .021 .023 5.6 0     0     
eca-rers2012/Problem04_label40_false-unreach-call_false-termination.c timeout 0 --- inspect 900   320   13000 5800 .63 0      error (invalid witness file) 0 --- inspect .74 .45 41 0      0      error (2) 0 --- inspect .023 .024 5.6 0     0     
eca-rers2012/Problem04_label42_true-unreach-call_false-termination.c timeout 0 --- inspect 910   310   13000 5900 .63 0      error (invalid witness file) 0 --- inspect .58 .36 40 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem04_label43_true-unreach-call_false-termination.c timeout 0 --- inspect 910   300   14000 6100 .62 0      error (invalid witness file) 0 --- inspect .75 .46 40 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem04_label44_true-unreach-call_false-termination.c timeout 0 --- inspect 910   290   14000 6300 .62 0      error (invalid witness file) 0 --- inspect .59 .38 41 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem04_label46_true-unreach-call_false-termination.c timeout 0 --- inspect 900   300   13000 6100 .63 0      error (invalid witness file) 0 --- inspect .76 .45 42 0      0      error (2) 0 --- inspect .020 .022 5.6 0     0     
eca-rers2012/Problem04_label49_true-unreach-call_false-termination.c timeout 0 --- inspect 900   320   14000 6000 .63 0      error (invalid witness file) 0 --- inspect .60 .36 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem04_label57_true-unreach-call_false-termination.c timeout 0 --- inspect 910   290   13000 6700 .63 0      error (invalid witness file) 0 --- inspect .80 .49 41 0      0      error (2) 0 --- inspect .022 .023 5.6 0     0     
eca-rers2012/Problem04_label58_false-unreach-call_false-termination.c timeout 0 --- inspect 910   310   13000 5600 .63 0      error (invalid witness file) 0 --- inspect .62 .38 40 0      0      error (2) 0 --- inspect .022 .025 5.7 0     0     
eca-rers2012/Problem14_label00_true-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2100 3000 .62 0      error (invalid witness file) 0 --- inspect .73 .44 40 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem14_label01_true-unreach-call_false-termination.c unknown 0 --- inspect 250   180   2400 3100 .62 0      error (invalid witness file) 0 --- inspect .68 .41 41 0      0      error (2) 0 --- inspect .023 .032 5.5 0     0     
eca-rers2012/Problem14_label02_false-unreach-call_false-termination.c unknown 0 --- inspect 250   180   2100 2700 .62 0      error (invalid witness file) 0 --- inspect .73 .45 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label03_true-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2500 2900 .62 0      error (invalid witness file) 0 --- inspect .64 .39 40 0      0      error (2) 0 --- inspect .021 .022 5.5 0     0     
eca-rers2012/Problem14_label04_true-unreach-call_false-termination.c unknown 0 --- inspect 250   170   2400 2600 .62 0      error (invalid witness file) 0 --- inspect .70 .43 41 0      0      error (2) 0 --- inspect .022 .023 5.7 0     0     
eca-rers2012/Problem14_label05_true-unreach-call_false-termination.c unknown 0 --- inspect 250   170   2400 2600 .62 0      error (invalid witness file) 0 --- inspect .59 .37 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label06_true-unreach-call_false-termination.c unknown 0 --- inspect 280   210   1900 2900 .62 0      error (invalid witness file) 0 --- inspect .76 .46 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label07_true-unreach-call_false-termination.c unknown 0 --- inspect 260   180   2100 2800 .62 0      error (invalid witness file) 0 --- inspect .83 .51 41 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem14_label08_false-unreach-call_false-termination.c unknown 0 --- inspect 270   190   1900 3400 .62 0      error (invalid witness file) 0 --- inspect .72 .44 40 0      0      error (2) 0 --- inspect .022 .024 5.6 0     0     
eca-rers2012/Problem14_label09_true-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2000 2900 .62 0      error (invalid witness file) 0 --- inspect .78 .47 40 0      0      error (2) 0 --- inspect .022 .024 5.6 0     0     
eca-rers2012/Problem14_label10_false-unreach-call_false-termination.c unknown 0 --- inspect 290   210   2000 3200 .62 0      error (invalid witness file) 0 --- inspect .82 .50 41 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem14_label11_false-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2200 3200 .62 0      error (invalid witness file) 0 --- inspect .75 .48 40 0      0      error (2) 0 --- inspect .020 .020 5.6 0     0     
eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c unknown 0 --- inspect 270   200   2300 2800 .62 0      error (invalid witness file) 0 --- inspect .79 .48 42 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label13_false-unreach-call_false-termination.c unknown 0 --- inspect 250   170   2200 3200 .62 0      error (invalid witness file) 0 --- inspect .73 .45 40 0      0      error (2) 0 --- inspect .053 .055 5.5 0     0     
eca-rers2012/Problem14_label14_false-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2000 3000 .62 0      error (invalid witness file) 0 --- inspect .74 .46 40 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label15_true-unreach-call_false-termination.c unknown 0 --- inspect 250   170   2800 2500 .62 0      error (invalid witness file) 0 --- inspect .70 .43 40 0      0      error (2) 0 --- inspect .022 .022 5.6 0     0     
eca-rers2012/Problem14_label16_true-unreach-call_false-termination.c unknown 0 --- inspect 260   170   2100 2900 .62 0      error (invalid witness file) 0 --- inspect .75 .46 41 0      0      error (2) 0 --- inspect .021 .021 5.7 0     0     
eca-rers2012/Problem14_label17_true-unreach-call_false-termination.c unknown 0 --- inspect 260   180   2000 2700 .62 0      error (invalid witness file) 0 --- inspect .76 .46 41 0      0      error (2) 0 --- inspect .022 .026 5.6 0     0     
eca-rers2012/Problem14_label18_false-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2300 2900 .62 0      error (invalid witness file) 0 --- inspect .59 .37 41 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem14_label19_true-unreach-call_false-termination.c unknown 0 --- inspect 260   180   2300 3300 .62 0      error (invalid witness file) 0 --- inspect .75 .46 41 0      0      error (2) 0 --- inspect .021 .022 5.6 0     0     
eca-rers2012/Problem14_label20_true-unreach-call_false-termination.c unknown 0 --- inspect 260   180   2400 3200 .62 0      error (invalid witness file) 0 --- inspect .75 .46 40 0      0      error (2) 0 --- inspect .021 .021 5.6 0     0     
eca-rers2012/Problem14_label21_true-unreach-call_false-termination.c unknown 0 --- inspect 250   170   2100 2500 .62 .033  error (invalid witness file) 0 --- inspect .59 .36 41 0      0      error (2) 0 --- inspect .028 .030 5.6 0     0     
eca-rers2012/Problem14_label22_false-unreach-call_false-termination.c unknown 0 --- inspect 270   190   2100 2900 .62 0      error (invalid witness file) 0 --- inspect .59 .35 42 0      0      error (2) 0 --- inspect .020 .021 5.6 0     0     
eca-rers2012/Problem14_label23_true-unreach-call_false-termination.c unknown 0 ---