Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution [2017-11-30 11:20:26 CET; 2017-12-01 08:19:20 CET; 2017-12-01 09:00:44 CET; 2017-12-01 10:20:37 CET; 2017-12-01 11:41:06 CET] [2017-11-30 11:20:26 CET; 2017-12-01 08:19:34 CET; 2017-12-01 09:12:30 CET; 2017-12-01 11:16:27 CET; 2017-12-01 13:00:07 CET] [2017-11-30 11:20:26 CET; 2017-12-01 08:22:21 CET; 2017-12-01 09:11:51 CET; 2017-12-01 10:49:29 CET; 2017-12-01 12:27:04 CET] [2017-11-30 16:01:31 CET; 2017-12-01 09:05:19 CET; 2017-12-01 10:24:45 CET; 2017-12-01 13:07:37 CET; 2017-12-01 15:15:10 CET] [2017-12-01 08:49:27 CET; 2017-12-02 00:00:31 CET; 2017-12-02 01:45:33 CET; 2017-12-02 06:23:16 CET; 2017-12-02 08:45:19 CET] [2017-12-01 12:59:33 CET; 2017-12-02 11:31:00 CET; 2017-12-02 13:45:39 CET; 2017-12-02 18:23:42 CET; 2017-12-02 20:38:57 CET] [2017-12-01 22:41:19 CET; 2017-12-02 23:08:57 CET; 2017-12-03 01:39:21 CET; 2017-12-03 04:09:48 CET; 2017-12-03 05:53:57 CET] [2017-12-02 01:06:24 CET; 2017-12-03 04:39:25 CET; 2017-12-03 06:09:42 CET; 2017-12-03 11:17:40 CET; 2017-12-03 12:12:33 CET] [2017-12-02 02:33:02 CET; 2017-12-03 04:40:15 CET; 2017-12-03 06:11:17 CET; 2017-12-03 11:17:40 CET; 2017-12-03 12:06:01 CET] [2017-12-02 17:23:13 CET; 2017-12-03 07:53:44 CET; 2017-12-03 08:41:41 CET; 2017-12-03 08:43:49 CET; 2017-12-03 09:20:08 CET]
Run set 2ls.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] esbmc-incr.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] symbiotic.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-ECA; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-ProductLines; sv-comp18.ReachSafety-Recursive; sv-comp18.ReachSafety-Sequentialized; sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other; sv-comp18; sv-comp18.NoOverflows-BitVectors; sv-comp18.NoOverflows-Other; sv-comp18.Termination-MainControlFlow; sv-comp18.Termination-MainHeap; sv-comp18.Termination-Other; sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call .093 22 .78 160    14000 1700   900   9100 7500 900    750 11000   900     3800 8400    900     3900 8500    1.6   200   17    900   4700 12000 900     5100   11000     900     4100   12000    
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call 31     15000 440    23    15000 370   900   6600 9000 46    160 530   900     2800 10000    900     2800 12000    900     4000   9800    900   5200 12000 900     4900   10000     900     2900   14000    
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call 33     15000 490    23    15000 300   900   6800 10000 46    160 650   900     2800 10000    900     2800 12000    900     4100   12000    900   5100 12000 900     4900   14000     900     2800   12000    
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call 33     15000 470    62    13000 780   900   6000 7800 890    340 12000   900     7400 9800    900     7500 12000    900     100   8500    900   5000 14000 900     5100   14000     900     2000   11000    
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call 33     15000 470    77    13000 1000   900   6900 9200 890    360 9100   900     7400 12000    900     7300 10000    900     100   9900    900   5100 11000 900     5000   14000     900     2600   12000    
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call 290     15000 2000    420    10000 2500   900   8400 8500 900    1400 9700   900     3000 7000    900     3000 6800    1.1   140   15    900   5400 11000 900     5300   12000     900     5500   12000    
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call 31     15000 360    100    15000 1300   900   7600 11000 900    2400 13000   900     9300 10000    900     9500 12000    3.4   300   45    900   4500 10000 900     4900   14000     900     1700   12000    
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call 31     15000 400    120    15000 1900   900   6200 9300 900    1400 12000   900     9400 9300    900     9300 10000    4.2   350   59    900   4900 10000 900     4900   12000     900     1000   10000    
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call 31     15000 430    130    15000 1800   900   6900 9600 900    2400 11000   900     9500 10000    900     9300 8400    4.5   370   66    900   5100 10000 900     4700   11000     900     1100   11000    
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call 31     15000 460    95    15000 1300   900   8000 9700 900    2400 11000   900     9300 8800    900     9500 12000    5.0   400   69    900   5200 9400 900     4700   12000     900     1400   12000    
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call 31     15000 390    100    15000 1200   900   8100 9600 900    2500 12000   900     9500 10000    900     9300 11000    5.3   430   59    900   5200 11000 900     5500   11000     900     1500   12000    
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call 31     15000 380    110    15000 1500   900   8400 8800 900    2200 13000   900     9400 9900    900     9400 9700    5.8   470   67    900   5300 9800 900     4900   11000     900     1600   9400    
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call 31     15000 420    120    15000 1900   900   8100 9500 900    2200 13000   900     9600 8700    900     9600 9400    6.1   500   71    900   5200 11000 900     4700   13000     900     1700   7700    
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call 31     15000 390    65    14000 970   900   9000 10000 900    2200 11000   900     9900 9700    900     9600 11000    6.5   530   82    900   5300 9900 900     4800   11000     900     1800   11000    
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call 31     15000 490    70    15000 910   900   8900 10000 900    2500 11000   900     9200 9500    900     9300 9800    7.0   560   88    900   5200 10000 900     4900   11000     900     2000   10000    
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call 33     15000 440    72    15000 980   900   4100 8700 890    220 9100   900     6200 12000    900     6100 11000    .80  71   11    900   4500 11000 900     4800   14000     900     880   10000    
array-examples/standard_init1_false-unreach-call_ground.i unreach-call 32     12000 400    100    15000 1500   900   4600 10000 900    700 11000   900     5900 9600    900     5800 10000    .42  39   5.7  900   2100 10000 900     4800   11000     900     1100   11000    
array-examples/standard_init2_false-unreach-call_ground.i unreach-call 31     15000 410    61    15000 790   900   2900 8900 900    710 13000   900     5900 10000    900     6000 10000    .64  68   8.5  900   2200 11000 900     4800   12000     900     760   13000    
array-examples/standard_init3_false-unreach-call_ground.i unreach-call 31     15000 400    64    15000 840   900   4300 11000 900    730 12000   900     5900 10000    900     5900 10000    .88  95   12    900   4200 11000 900     4800   12000     900     780   10000    
array-examples/standard_init4_false-unreach-call_ground.i unreach-call 31     15000 390    67    15000 1100   900   4400 10000 900    700 12000   900     6000 9000    900     6000 10000    1.1   120   15    900   4900 9200 900     4800   12000     900     730   12000    
array-examples/standard_init5_false-unreach-call_ground.i unreach-call 31     15000 460    71    15000 1000   900   4200 8900 890    210 9200   900     5900 9700    900     6100 9600    1.3   150   18    900   5500 9200 900     4800   11000     900     720   11000    
array-examples/standard_init6_false-unreach-call_ground.i unreach-call 31     15000 410    74    15000 980   900   4100 11000 890    240 8400   900     6100 11000    900     6100 9900    1.5   180   23    900   5700 9400 900     4800   11000     900     770   12000    
array-examples/standard_init7_false-unreach-call_ground.i unreach-call 31     15000 470    52    15000 790   900   4100 8300 900    270 8300   900     6000 11000    900     6100 10000    1.8   200   24    900   5700 12000 900     4800   12000     900     840   11000    
array-examples/standard_init8_false-unreach-call_ground.i unreach-call 31     15000 470    54    15000 660   900   4300 9200 890    290 8700   900     6100 9100    900     6100 12000    2.0   230   28    900   5100 8500 900     4800   12000     900     920   10000    
array-examples/standard_init9_false-unreach-call_ground.i unreach-call 33     15000 480    56    15000 680   900   4300 11000 900    320 10000   900     6000 11000    900     6100 9700    2.2   260   31    900   5600 8900 900     4800   11000     900     930   11000    
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call 320     15000 2200    870    1400 3800   900   4100 11000 98    110 1400   900     7100 11000    900     7100 9800    100     15000   1200    900   5200 11000 900     4800   11000     900     2900   15000    
array-examples/standard_partition_false-unreach-call_ground.i unreach-call 31     15000 380    65    14000 710   900   6000 8300 900    2300 12000   900     4200 10000    900     4300 11000    900     12000   9400    900   4500 11000 900     4900   9300     900     2800   12000    
array-examples/standard_running_false-unreach-call.i unreach-call 31     15000 370    88    15000 1300   900   4700 9200 890    340 9300   430     15000 5600    430     15000 5600    900     11000   13000    900   6300 10000 900     4800   12000     900     6300   11000    
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call .11  22 .62 870    1500 4900   93   2300 980 890    970 7800   900     9200 10000    900     9100 10000    .15  11   1.8  6.2 290 49 900     5200   13000     6.2   300   48    
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call .078 22 .71 26    13000 420   900   8700 9100 900    260 8100   900     3500 7700    900     3600 11000    900     1300   10000    900   2000 11000 900     4900   12000     900     2500   11000    
array-examples/relax_true-unreach-call.i unreach-call .18  26 1.6  690    14000 3800   900   5500 8000 890    190 7100   900     350 10000    900     360 13000    370     180   1900    900   740 11000 900     590   13000     900     5100   10000    
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call 180     15000 1400    870    2600 4400   900   4300 9800 320    180 4200   900     10000 12000    900     10000 10000    460     15000   3900    900   5300 13000 900     4900   11000     900     3300   13000    
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call 34     15000 390    28    13000 400   900   9100 9100 890    180 11000   900     360 12000    900     520 10000    900     830   11000    900   980 13000 900     5300   11000     900     1100   11000    
array-examples/sanfoundry_24_true-unreach-call_true-termination.i unreach-call 17     5700 190    870    4200 9100   6.1 480 65 900    3900 11000   900     1000 12000    .10  26 .80 900     5400   8400    6.3 290 49 5.8   330   48     6.5   300   59    
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call 270     15000 2100    870    1400 4100   900   4600 9200 120    120 1500   900     7000 10000    900     7000 9800    100     15000   990    900   2800 8900 900     4700   11000     900     3000   10000    
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call .074 22 .82 93    15000 1200   93   2300 1000 52    100 720   900     9700 12000    .10  26 .87 .15  11   1.3  4.2 250 34 4.3   250   35     4.5   250   35    
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call 31     15000 370    20    15000 250   900   6400 9100 46    160 510   900     2800 9900    900     2800 10000    900     3900   9800    900   5000 11000 900     5200   11000     900     5300   11000    
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call 33     15000 520    74    13000 820   900   6000 9400 890    300 7800   900     7300 11000    900     7300 8600    900     100   8100    900   5100 15000 900     5100   12000     900     2500   14000    
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call 32     15000 450    120    15000 1800   900   6000 8700 890    190 9500   900     5800 11000    900     5700 9500    900     10000   10000    900   2600 11000 900     4900   12000     900     2700   9500    
array-examples/standard_compare_true-unreach-call_ground.i unreach-call 150     15000 1300    870    1500 3800   900   3900 10000 110    170 1300   900     7500 10000    900     7500 10000    900     11000   11000    900   5200 12000 900     4800   13000     900     3900   15000    
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call 33     15000 440    68    15000 1100   900   6600 9800 890    240 9600   900     10000 10000    900     10000 11000    2.2   130   29    900   4400 11000 900     4700   11000     900     1000   11000    
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call 34     15000 430    81    15000 1000   900   6900 8900 900    2200 12000   900     10000 11000    900     10000 9100    2.5   150   32    900   5100 13000 900     4900   12000     900     940   10000    
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call 33     15000 430    92    15000 1100   900   6600 10000 900    2200 12000   900     10000 9900    900     10000 11000    2.9   160   34    900   5100 11000 900     4700   12000     900     1000   12000    
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call 33     15000 470    100    15000 1300   900   7700 9700 900    1400 12000   900     10000 9900    900     10000 10000    3.2   170   38    900   5200 11000 900     4700   12000     900     1100   9200    
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call 33     15000 440    82    15000 1100   900   8400 8500 900    2200 11000   900     10000 12000    900     10000 11000    3.5   180   45    900   5100 12000 900     4900   13000     900     1300   11000    
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call 33     15000 480    91    15000 1200   900   8800 9300 900    1400 11000   900     10000 10000    900     10000 9800    3.9   190   49    900   5300 10000 900     4700   11000     900     1500   11000    
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call 33     15000 450    99    15000 1200   900   8700 11000 900    2200 11000   900     10000 12000    900     10000 9700    4.1   200   50    900   5200 9700 900     4800   13000     900     1500   9300    
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call 33     15000 520    82    15000 1300   900   8200 8900 900    2200 12000   900     10000 9800    900     10000 11000    4.6   210   71    900   5400 12000 900     4700   13000     900     1900   7700    
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call 33     15000 390    62    14000 730   900   9000 10000 900    2400 13000   900     10000 9900    900     10000 11000    5.1   220   61    900   5300 10000 900     4700   11000     900     2100   11000    
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call 32     15000 500    72    15000 900   900   4100 8900 890    160 10000   900     6000 9700    900     6100 10000    1.4   51   18    900   5000 10000 900     4800   12000     900     780   11000    
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call 32     15000 420    75    15000 1100   900   4100 8700 900    210 9800   900     6100 10000    900     6000 10000    1.8   59   27    900   4800 11000 900     4800   11000     900     780   12000    
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call 32     15000 460    72    15000 1000   900   4000 8600 890    190 8600   900     6000 9600    900     6000 10000    1.5   82   20    900   5100 12000 900     4800   12000     900     1000   11000    
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call 32     15000 390    69    15000 900   900   4700 10000 890    220 10000   900     6000 9500    900     5900 9800    1.1   41   16    900   3300 9900 900     5000   11000     900     910   11000    
array-examples/standard_find_true-unreach-call_ground.i unreach-call 40     15000 500    100    15000 1300   900   6500 9000 900    2300 13000   900     10000 9800    900     10000 9600    530     2400   8300    900   5000 12000 900     5000   12000     900     1300   12000    
array-examples/standard_init1_true-unreach-call_ground.i unreach-call 32     12000 390    100    15000 1400   900   2800 9300 900    730 13000   900     5800 11000    900     5900 11000    .80  32   10    900   2200 10000 900     4800   13000     900     890   11000    
array-examples/standard_init2_true-unreach-call_ground.i unreach-call 31     15000 380    61    15000 860   900   4300 11000 900    770 10000   900     5900 9600    900     5900 9900    .97  39   14    900   2900 10000 900     4700   12000     900     790   12000    
array-examples/standard_init3_true-unreach-call_ground.i unreach-call 31     15000 410    64    15000 880   900   4300 10000 900    730 10000   900     6000 12000    900     5900 9300    1.2   47   17    900   4400 9700 900     5200   12000     900     890   10000    
array-examples/standard_init4_true-unreach-call_ground.i unreach-call 31     15000 470    67    15000 910   900   4200 9400 900    770 10000   900     6000 10000    900     5900 11000    1.4   54   21    900   5100 8100 900     5200   14000     900     770   11000    
array-examples/standard_init5_true-unreach-call_ground.i unreach-call 31     15000 400    71    15000 1000   900   4100 9200 890    220 9700   900     6000 11000    900     6000 9700    1.6   61   23    900   5500 8700 900     4800   12000     900     850   10000    
array-examples/standard_init6_true-unreach-call_ground.i unreach-call 31     15000 400    74    15000 990   900   4200 9300 900    240 9600   900     6000 8600    900     6000 10000    1.8   68   27    900   5700 8300 900     4800   12000     900     790   13000    
array-examples/standard_init7_true-unreach-call_ground.i unreach-call 31     15000 490    52    15000 700   900   4300 9200 890    270 9800   900     6000 10000    900     6000 11000    2.0   75   27    900   5800 11000 900     4800   11000     900     800   10000    
array-examples/standard_init8_true-unreach-call_ground.i unreach-call 31     15000 440    54    15000 730   900   4400 9100 890    290 10000   900     6000 10000    900     6000 13000    2.2   83   30    900   5100 8100 900     4800   13000     900     910   9800    
array-examples/standard_init9_true-unreach-call_ground.i unreach-call 31     15000 450    56    15000 730   900   4000 9300 900    320 9000   900     6000 10000    900     6000 11000    2.4   90   38    900   5600 8000 900     4800   13000     900     910   13000    
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call 260     15000 1900    870    1400 4900   900   4500 8500 120    120 1600   900     7100 10000    900     7100 9800    100     15000   940    900   2600 11000 900     4800   12000     910     4300   9700    
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call 310     15000 2100    870    1400 3900   900   5200 8000 100    120 1500   900     7200 12000    900     7200 9700    100     15000   1000    900   2700 8800 900     4800   11000     900     4400   9200    
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call 34     15000 420    100    15000 1300   900   5600 11000 890    160 10000   900     10000 12000    900     10000 11000    .69  45   8.6  900   1400 10000 900     4800   11000     900     850   9900    
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call 31     15000 400    90    13000 870   900   4700 8000 900    2200 13000   900     4200 12000    900     4200 11000    900     3800   8200    900   2900 11000 900     4800   14000     900     2100   9400    
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call 29     15000 370    74    14000 880   900   4900 10000 900    2500 12000   480     15000 6600    470     15000 5200    16     15000   180    910   14000 3500 900     5200   11000     910     15000   3400    
array-examples/standard_partition_true-unreach-call_ground.i unreach-call 31     15000 400    66    14000 810   900   6400 8700 890    270 9600   900     4200 12000    900     4300 12000    900     12000   8700    900   650 13000 900     4700   12000     32     720   310    
array-examples/standard_password_true-unreach-call_ground.i unreach-call 150     15000 1400    870    1500 3500   900   3800 9600 120    180 1400   900     7500 11000    900     7500 9500    900     10000   10000    900   5200 13000 900     4800   11000     900     3500   13000    
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call 33     15000 510    110    15000 1500   900   7200 8800 900    180 8600   900     8700 9700    900     8600 11000    1.1   75   13    900   1800 11000 900     4800   9400     900     980   10000    
array-examples/standard_running_true-unreach-call.i unreach-call 31     15000 510    88    15000 1100   900   4900 9000 890    300 9900   430     15000 5200    430     15000 6200    900     7400   11000    900   860 13000 900     4800   13000     900     1000   8300    
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call 110     15000 880    870    3900 11000   6.5 480 66 100    75 1000   900     300 11000    900     300 11000    900     410   9100    6.6 330 52 5.5   310   42     7.6   440   58    
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call 34     15000 420    100    15000 1400   900   3400 11000 900    780 13000   900     6100 9900    900     6200 12000    .93  33   11    900   1800 11000 900     4800   12000     900     790   11000    
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call 75     11000 870    870    3500 5500   900   3500 8800 120    120 1800   900     7200 10000    900     7300 11000    900     640   9600    900   5200 12000 900     6900   10000     900     3500   7700    
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call 33     15000 410    73    15000 940   900   6500 8300 900    2300 11000   900     10000 10000    900     10000 11000    28     2200   250    900   3700 11000 900     4800   13000     900     1300   11000    
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call 33     15000 420    73    15000 1100   900   5900 8600 890    270 13000   900     10000 11000    900     10000 12000    26     2200   180    900   3300 13000 900     4700   11000     900     1400   11000    
array-examples/standard_two_index_01_true-unreach-call.i unreach-call 250     15000 1600    96    15000 1100   900   6600 8200 890    250 9700   900     10000 12000    900     10000 9600    .38  22   4.2  900   2900 10000 900     4800   14000     900     970   11000    
array-examples/standard_two_index_02_true-unreach-call.i unreach-call 34     15000 440    68    15000 890   900   6200 11000 890    200 10000   900     10000 10000    900     10000 12000    1.9   120   24    900   3000 9800 900     4800   11000     900     870   11000    
array-examples/standard_two_index_03_true-unreach-call.i unreach-call 240     15000 1800    96    15000 1300   900   6200 11000 890    180 8600   900     10000 10000    900     10000 10000    .32  20   3.3  900   3000 10000 900     5000   14000     900     880   12000    
array-examples/standard_two_index_04_true-unreach-call.i unreach-call 33     15000 480    68    15000 890   900   5700 8500 890    230 13000   900     10000 12000    900     10000 9700    1.6   120   22    900   2800 9800 900     4800   12000     900     960   9900    
array-examples/standard_two_index_05_true-unreach-call.i unreach-call 34     15000 430    68    15000 950   900   6000 10000 890    220 9700   900     9900 9800    900     10000 12000    1.5   120   18    900   2900 9500 900     4800   12000     900     1100   10000    
array-examples/standard_two_index_06_true-unreach-call.i unreach-call 240     15000 1700    96    15000 1400   900   6300 9000 890    180 8600   900     10000 9700    900     10000 10000    .33  20   3.6  900   3300 8900 900     4800   13000     900     980   11000    
array-examples/standard_two_index_07_true-unreach-call.i unreach-call 34     15000 420    68    15000 860   900   6500 11000 890    230 9200   900     10000 10000    900     10000 11000    1.5   120   19    900   2800 10000 900     4800   12000     900     1100   11000    
array-examples/standard_two_index_08_true-unreach-call.i unreach-call 34     15000 420    68    15000 880   900   6200 8900 890    190 13000   900     10000 8500    900     9900 11000    1.5   120   19    900   2900 10000 900     5000   12000     900     1300   13000    
array-examples/standard_two_index_09_true-unreach-call.i unreach-call 34     15000 430    68    15000 900   900   5900 8400 890    180 8700   900     10000 10000    900     10000 10000    1.4   120   18    900   2500 10000 900     4800   12000     900     1300   12000    
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call 170     15000 1200    870    4500 4900   900   5700 7700 98    100 1400   900     830 11000    900     830 11000    900     500   11000    900   4600 13000 900     3000   11000     900     2900   14000    
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call 32     15000 400    120    15000 1600   900   6600 8400 900    2400 12000   900     4500 9900    900     4500 9700    1.6   170   19    900   1900 11000 900     4800   11000     900     850   9300    
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unreach-call 32     15000 380    60    15000 770   900   4900 9900 890    330 9300   900     6400 9900    900     6400 9600    .42  44   6.1  900   2500 11000 900     4900   10000     900     1100   12000    
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call 34     15000 500    410    15000 3800   900   6300 8600 890    300 9800   900     5200 10000    900     5200 10000    .39  38   4.8  900   5100 9400 900     5200   7300     900     5200   7100    
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unreach-call 26     15000 330    71    15000 930   900   4000 8900 890    250 9900   900     5000 11000    900     5000 13000    2.0   200   25    900   5100 13000 900     4900   12000     900     2000   9900    
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call 38     15000 460    440    15000 6400   900   5100 9900 890    190 9700   900     4600 11000    900     4600 10000    .45  42   5.9  900   5200 6700 900     5200   7100     900     5000   8700    
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unreach-call 26     15000 340    71    15000 960   900   4500 10000 890    250 9600   900     5000 12000    900     5000 11000    900     3900   9400    900   5100 11000 900     5900   9900     900     1800   11000    
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call .079 23 .65 23    12000 300   900   6600 9100 900    5900 9600   900     3500 7700    900     3500 7600    900     1200   11000    900   5300 12000 900     4900   11000     900     4400   12000    
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unreach-call 29     15000 370    100    15000 1300   900   5300 8600 890    230 9000   900     4200 10000    900     4200 10000    20     15000   230    900   3400 11000 900     4900   11000     900     910   11000    
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unreach-call 30     15000 370    120    15000 1500   900   4700 11000 890    1700 9800   900     4200 11000    900     4100 8700    14     15000   180    900   1700 10000 900     5200   13000     900     1900   12000    
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call 36     13000 390    250    15000 2500   900   7700 7600 890    220 9400   660     15000 5000    670     15000 4800    .86  32   12    900   5300 8800 900     5200   7500     900     5300   8700    
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call 110     7000 820    280    15000 3900   900   7000 8400 900    3700 7100   900     6400 9800    900     6400 9800    11     360   140    900   5900 7400 900     6000   8800     900     5800   8100    
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call .16  24 1.6  150    15000 1800   900   6900 8200 540    650 5000   900     8400 11000    900     8400 13000    3.0   110   41    9.6 500 83 900     4900   11000     14     640   110    
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call 100     7000 830    290    15000 3300   900   6400 11000 900    4100 8200   900     4800 8900    900     4900 9900    900     3700   8200    900   5900 7900 900     6000   8500     900     5800   7000    
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call 34     15000 440    560    15000 8100   900   5800 9800 890    230 11000   900     2500 11000    900     2400 9300    330     15000   4200    900   5900 7800 900     6400   7600     900     6100   8700    
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call 26     15000 320    130    15000 1700   900   6300 10000 890    250 9500   900     1600 11000    900     1600 11000    2.9   110   34    900   5900 9600 900     6400   8600     900     5900   11000    
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call 130     11000 1200    430    15000 5200   900   5200 8600 890    430 8600   900     7300 11000    900     7300 9500    1.9   71   25    900   5800 7200 900     6200   6500     900     6000   9700    
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call 29     12000 360    200    15000 2500   900   5000 9900 890    390 9500   900     4300 10000    900     4400 9700    900     3700   8000    900   5900 9400 900     6000   8700     900     5900   8000    
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unreach-call 900     14000 3700    870    5600 5100   900   6600 8700 900    4100 8700   900     190 13000    900     180 11000    .19  11   2.1  900   3700 12000 900     2700   12000     900     1400   10000    
reducercommutativity/rangesum05_false-unreach-call_true-termination.i unreach-call .089 22 .64 .67 34 6.4 81   670 810 490    210 5400   1.1   28 10    1.8   55 22    .21  12   2.4  9.8 530 83 9.9   480   84     25     840   230    
reducercommutativity/rangesum10_false-unreach-call_true-termination.i unreach-call .11  22 .64 1.1  34 9.8 370   2300 3800 500    210 6800   2.0   29 14    2.5   57 23    .21  13   2.8  25   730 250 18     700   170     31     1000   240    
reducercommutativity/rangesum20_false-unreach-call.i unreach-call .092 22 .76 2.0  35 26   900   2700 8000 640    210 8400   4.1   32 35    4.5   55 49    .52  24   7.1  900   1400 13000 39     1000   390     90     1400   890    
reducercommutativity/rangesum40_false-unreach-call.i unreach-call .094 22 .82 4.9  41 61   900   3900 7700 890    250 12000   15     45 170    16     57 160    .46  27   6.0  900   860 11000 900     1900   10000     55     1900   530    
reducercommutativity/rangesum60_false-unreach-call.i unreach-call .11  23 .63 8.9  59 110   900   5700 8500 890    210 13000   180     170 2600    180     170 2500    .74  32   10    900   2400 11000 900     3300   8700     600     2400   8100    
reducercommutativity/rangesum_false-unreach-call_true-termination.i unreach-call .097 22 .63 .96 58 12   30   560 360 490    210 6000   1.2   31 11    2.2   57 23    .21  12   2.0  10   540 88 17     680   190     39     760   350    
reducercommutativity/avg05_true-unreach-call_true-termination.i unreach-call 110     360 1300    35    51 500   900   2500 11000 900    2200 11000   42     72 630    43     75 480    .19  11   1.9  900   5300 9400 900     710   11000     900     6300   11000    
reducercommutativity/avg10_true-unreach-call_true-termination.i unreach-call 900     710 12000    530    180 6000   900   5100 7400 900    3400 11000   490     190 5600    490     190 6000    .19  11   2.0  900   7700 8800 900     960   12000     900     7400   8100    
reducercommutativity/avg20_true-unreach-call.i unreach-call 900     810 12000    870    280 10000   900   2800 9200 900    700 6500   900     290 11000    900     290 11000    .20  11   1.5  900   2200 7400 900     1500   10000     900     1800   9600    
reducercommutativity/avg40_true-unreach-call.i unreach-call 900     890 7700    870    300 11000   900   2700 9000 890    260 7300   900     370 11000    900     380 13000    .17  11   1.9  900   4100 12000 310     4300   3700     900     1800   11000    
reducercommutativity/avg60_true-unreach-call.i unreach-call 900     1000 8800    870    350 11000   900   3100 10000 890    260 8300   900     440 10000    900     420 10000    .18  11   2.6  900   2900 9600 800     5000   11000     900     1700   11000    
reducercommutativity/avg_true-unreach-call_true-termination.i unreach-call 900     1600 7200    870    220 11000   900   3000 7700 890    180 10000   900     150 12000    900     140 13000    .21  12   2.1  900   660 9900 900     510   12000     900     2900   9900    
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call 6.0   89 85    2.4  35 27   210   2400 1600 900    1500 10000   .65  28 8.3  .70  28 9.1  3.9   14   53    900   1600 10000 900     11000   11000     910     8000   10000    
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call 300     480 3800    87    66 970   900   2700 6600 900    2400 8700   17     44 210    17     42 200    200     20   3300    900   2400 10000 900     13000   12000     900     2000   14000    
reducercommutativity/max20_true-unreach-call.i unreach-call 900     1000 11000    870    200 11000   900   2900 10000 890    190 11000   900     140 11000    900     140 10000    900     58   13000    900   3400 10000 900     6200   15000     900     2300   11000    
reducercommutativity/max40_true-unreach-call.i unreach-call 900     1400 9000    870    230 14000   900   2200 11000 890    270 7900   900     190 13000    900     190 13000    900     89   12000    900   4400 11000 900     7400   9400     900     1900   11000    
reducercommutativity/max60_true-unreach-call.i unreach-call 900     1900 5600    870    260 9500   900   3600 8700 890    230 8900   900     260 11000    900     250 12000    900     130   12000    900   2900 9900 900     6800   7600     900     2100   10000    
reducercommutativity/max_true-unreach-call_true-termination.i unreach-call 900     2500 3700    870    230 12000   900   5300 8400 890    250 9400   900     110 11000    900     100 13000    .21  11   2.3  900   1200 11000 900     2900   13000     900     3200   13000    
reducercommutativity/sep05_true-unreach-call_true-termination.i unreach-call 2.1   69 24    .93 35 8.9 860   3800 11000 790    1600 9900   .11  26 .89 .17  27 1.7  .17  11   1.9  900   1700 13000 900     4600   7300     900     1600   13000    
reducercommutativity/sep10_true-unreach-call.i unreach-call 3.3   100 41    1.5  38 18   900   5300 7200 900    4900 9200   .10  26 1.2  .19  27 1.8  .19  11   1.9  910   8000 13000 900     6100   13000     900     2000   13000    
reducercommutativity/sep20_true-unreach-call.i unreach-call 12     280 120    4.8  48 59   900   4300 8600 900    190 10000   .17  26 1.4  .23  27 2.2  .19  11   2.1  900   7100 9700 910     13000   8400     900     2600   13000    
reducercommutativity/sep40_true-unreach-call.i unreach-call 900     1400 9300    35    87 490   900   2700 9600 900    190 9400   .21  26 2.2  .30  27 3.3  .18  11   2.3  900   3900 11000 910     13000   8400     900     1800   14000    
reducercommutativity/sep60_true-unreach-call.i unreach-call 900     2200 9400    150    160 2100   900   3800 9000 890    190 9400   .33  26 3.5  .39  28 4.2  .21  11   2.2  900   3000 10000 900     13000   8100     900     1900   11000    
reducercommutativity/sep_true-unreach-call_true-termination.i unreach-call 900     10000 7000    880    9700 4300   900   5600 7400 890    190 7500   900     120 12000    900     130 10000    .20  12   2.4  900   1500 11000 900     1800   13000     900     4600   13000    
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call 20     170 270    4.7  39 56   900   2000 11000 900    4000 10000   .12  26 .88 .14  27 1.8  .19  11   2.1  310   3200 3700 40     2600   370     900     6000   6600    
reducercommutativity/sum10_true-unreach-call_true-termination.i unreach-call 900     760 11000    180    130 2200   900   6500 7300 900    1900 13000   .099 26 1.0  .15  27 1.9  .19  11   2.2  900   5700 9400 230     4500   2700     900     5100   6800    
reducercommutativity/sum20_true-unreach-call.i unreach-call 900     720 8100    870    270 10000   900   4400 9100 890    240 8100   .14  26 1.5  .20  27 2.4  .20  11   2.0  900   4700 11000 900     5300   6400     900     4700   12000    
reducercommutativity/sum40_true-unreach-call.i unreach-call 900     860 8600    870    270 11000   900   3600 8200 890    200 9000   .17  26 2.2  .23  27 2.6  .19  11   2.2  900   4600 12000 900     5200   11000     900     1700   11000    
reducercommutativity/sum60_true-unreach-call.i unreach-call 900     1000 6100    870    270 9900   900   3500 9600 890    230 6900   .25  26 2.7  .32  27 3.2  .19  11   2.1  900   2400 10000 900     5600   8400     900     1700   10000    
reducercommutativity/sum_true-unreach-call_true-termination.i unreach-call 900     1900 8000    870    220 13000   900   5500 8800 890    200 9000   900     150 12000    900     130 11000    .20  12   2.2  900   4900 8400 900     2000   13000     900     4700   6400    
array-tiling/mlceu_false-unreach-call.i unreach-call 670     15000 3200    870    5800 8700   900   6700 6900 900    3500 7800   900     180 11000    900     180 13000    .17  12   2.2  900   1600 12000 900     3100   11000     900     1100   12000    
array-tiling/skippedu_false-unreach-call.i unreach-call .33  38 3.4  .26 33 2.8 3.4 270 30 1.1  100 13   .13  28 1.9  .14  28 1.4  .21  12   2.4  6.4 290 58 5.2   290   43     7.5   370   62    
array-tiling/mbpr2_true-unreach-call.i unreach-call 510     15000 2500    81    13000 690   900   5800 8000 890    160 10000   900     240 13000    900     180 13000    .21  11   2.0  20   330 220 900     880   12000     23     360   240    
array-tiling/mbpr3_true-unreach-call.i unreach-call 410     15000 2000    230    13000 1400   900   6500 7700 890    220 9700   900     240 11000    900     180 11000    .21  12   2.2  900   1300 10000 900     1100   12000     29     560   280    
array-tiling/mbpr4_true-unreach-call.i unreach-call 440     15000 2600    210    13000 2000   900   6800 8400 890    300 9100   900     200 12000    900     210 10000    .20  12   2.5  21   380 160 900     920   11000     900     830   11000    
array-tiling/mbpr5_true-unreach-call.i unreach-call 900     12000 4400    150    14000 1400   900   5800 9500 890    350 9600   900     210 11000    900     190 11000    .22  12   2.3  93   790 980 900     1100   12000     26     550   220    
array-tiling/nr2_true-unreach-call.i unreach-call 680     15000 3300    60    14000 720   900   5800 6100 890    420 8900   900     220 11000    900     220 13000    .21  11   2.3  900   2400 11000 900     2300   12000     900     1500   11000    
array-tiling/nr3_true-unreach-call.i unreach-call 490     15000 4500    56    13000 660   900   6500 8400 890    470 8900   900     160 13000    900     190 13000    .22  12   2.2  900   830 13000 900     2500   11000     900     980   12000    
array-tiling/nr4_true-unreach-call.i unreach-call 400     15000 2100    84    13000 960   900   4800 9600 890    440 8700   900     220 12000    900     160 12000    .22  12   2.3  900   890 10000 900     1900   14000     900     790   11000    
array-tiling/nr5_true-unreach-call.i unreach-call 590     15000 4100    110    13000 870   900   5700 7000 890    450 10000   900     140 11000    900     160 13000    .20  12   2.3  900   870 11000 900     2000   11000     900     990   13000    
array-tiling/pnr2_true-unreach-call.i unreach-call 560     15000 3500    660    13000 5100   900   3800 6600 890    140 11000   900     260 10000    900     220 11000    .22  12   2.0  900   2300 12000 900     1800   14000     900     1400   11000    
array-tiling/pnr3_true-unreach-call.i unreach-call 580     15000 2700    870    3700 4500   900   4300 5600 890    200 14000   900     270 11000    900     240 13000    .19  12   2.1  900   1700 12000 900     1700   13000     900     1500   11000    
array-tiling/pnr4_true-unreach-call.i unreach-call 530     15000 1800    870    6200 5600   900   4000 6800 890    240 9600   900     280 8700    900     280 11000    .21  12   2.0  900   2600 12000 900     2100   13000     900     3200   12000    
array-tiling/pnr5_true-unreach-call.i unreach-call 350     15000 1800    870    2700 5800   900   4300 7400 890    280 8800   900     290 10000    900     430 11000    .22  12   2.3  900   3400 12000 900     4700   13000     900     1900   9900    
array-tiling/poly1_true-unreach-call.i unreach-call 900     10000 4200    880    11000 7500   900   4100 7400 890    190 12000   .10  26 .80 .10  26 .73 .20  12   2.0  900   930 11000 900     1300   12000     5.9   300   53    
array-tiling/poly2_true-unreach-call.i unreach-call 900     11000 4700    160    13000 1600   900   5200 6400 890    160 10000   .058 15 .29 .033 15 .27 74     40   280    900   1700 11000 900     2700   12000     8.1   390   63    
array-tiling/pr2_true-unreach-call.i unreach-call 460     15000 2800    130    13000 1700   900   4100 6200 890    260 11000   900     230 12000    900     270 14000    .20  12   2.3  900   1200 11000 900     1200   14000     900     900   11000    
array-tiling/pr3_true-unreach-call.i unreach-call 380     15000 2100    220    13000 1800   900   3800 6900 890    230 11000   900     240 12000    900     250 12000    .21  12   2.1  900   1200 14000 900     1200   12000     900     1000   10000    
array-tiling/pr4_true-unreach-call.i unreach-call 400     15000 2100    280    13000 2300   900   3800 7100 890    240 9500   900     390 11000    900     280 13000    .20  12   3.0  900   910 13000 900     970   11000     900     760   13000    
array-tiling/pr5_true-unreach-call.i unreach-call 280     15000 2100    880    9500 3900   900   3600 6400 890    280 9500   900     280 12000    900     290 12000    .22  11   2.2  900   1300 11000 900     950   11000     900     1100   11000    
array-tiling/revcpyswp2_true-unreach-call.i unreach-call 900     11000 5500    870    1400 5600   900   4200 7300 900    5600 8100   900     250 12000    900     240 11000    .18  12   2.4  900   1600 14000 900     5200   12000     900     1000   11000    
array-tiling/rew_true-unreach-call.i unreach-call 540     15000 2900    470    14000 3500   900   5100 7400 900    3400 9100   900     210 11000    900     230 11000    .20  12   2.1  900   2000 10000 900     1900   12000     900     1500   12000    
array-tiling/rewnif_true-unreach-call.i unreach-call 500     15000 3300    660    14000 5900   900   4600 6700 900    4900 10000   900     210 11000    900     200 12000    .19  12   2.0  900   1200 13000 900     2100   14000     900     1200   9900    
array-tiling/rewnifrev2_true-unreach-call.i unreach-call 610     15000 4700    130    14000 1100   900   3800 7800 900    5000 8400   900     380 11000    900     350 11000    .21  12   2.1  900   3100 9300 900     2900   10000     900     2600   8400    
array-tiling/rewnifrev_true-unreach-call.i unreach-call 560     15000 3900    130    14000 1300   900   4300 6800 900    2600 11000   900     390 10000    900     400 11000    .20  12   2.2  900   2100 10000 900     4300   14000     900     1100   11000    
array-tiling/rewrev_true-unreach-call.i unreach-call 580     15000 3300    120    14000 1500   900   4500 6800 900    3800 11000   900     410 11000    900     330 12000    .22  12   2.3  900   2200 12000 900     2600   11000     900     1400   12000    
array-tiling/skipped_true-unreach-call.i unreach-call 780     15000 2800    560    14000 4900   900   3100 7300 890    100 11000   900     230 8300    900     390 11000    .20  12   2.2  900   1500 12000 900     840   12000     900     1400   12000    
array-tiling/tcpy_true-unreach-call.i unreach-call 900     14000 6500    870    1000 4200   900   3500 6700 890    170 14000   900     180 13000    900     170 11000    .23  12   2.3  900   2600 10000 900     1800   11000     900     2500   11000    
array-programs/copysome1_false-unreach-call.i unreach-call 25     15000 310    130    15000 1500   900   11000 9300 890    280 10000   900     9300 10000    900     9700 9400    3.2   270   41    900   4300 8800 900     4900   12000     900     2500   9500    
array-programs/copysome2_false-unreach-call.i unreach-call 27     15000 340    130    14000 1800   900   8700 9300 890    310 9300   900     9600 10000    900     9600 10000    3.2   270   36    900   3300 9400 900     5000   14000     900     2800   8400    
array-programs/copysome1_true-unreach-call.i unreach-call 25     15000 340    130    15000 2100   900   9500 8500 890    280 7900   900     9700 10000    900     9700 9400    3.2   270   41    900   2600 9000 900     4900   13000     900     2800   9200    
array-programs/copysome2_true-unreach-call.i unreach-call 27     15000 380    130    14000 1700   900   7600 9800 890    260 9300   900     9600 9700    900     9600 12000    3.1   270   36    900   3200 8800 900     4900   11000     900     2800   10000    
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unreach-call .32  28 3.8  .70 34 6.7 17   440 180 2.2  110 33   1.1   29 10    1.2   29 14    .31  12   4.0  85   880 880 31     490   280     110     1500   940    
bitvector/sum02_false-unreach-call_true-no-overflow.i unreach-call 900     1400 10000    870    6000 3300   910   7700 10000 70    75 990   900     780 11000    900     780 11000    900     790   13000    14   380 140 900     680   10000     900     700   11000    
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unreach-call .33  29 4.3  .86 34 8.1 12   440 100 74    1700 820   .18  27 1.6  .16  27 1.9  .32  12   3.9  900   1400 12000 720     1600   7700     900     2600   12000    
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unreach-call .34  31 3.7  .85 34 8.5 13   470 120 28    910 330   .17  27 2.0  .15  27 1.8  .35  12   4.0  900   1400 10000 900     1500   7600     900     3100   12000    
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unreach-call .25  27 2.6  .53 36 5.7 6.8 280 76 490    310 7300   .97  29 12    .38  27 4.3  .42  12   5.0  900   630 13000 660     670   4700     900     1000   12000    
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unreach-call .76  39 9.0  2.0  42 24   7.6 280 83 230    280 3000   27     45 330    37     44 420    9.8   15   130    900   670 12000 900     520   11000     900     1100   11000    
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unreach-call .64  40 7.4  2.0  42 26   150   310 2000 470    330 5000   30     43 370    37     45 460    9.4   15   120    900   2800 11000 900     500   12000     510     1200   4100    
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unreach-call .56  33 6.0  .76 33 9.5 2.5 260 20 490    260 6000   .082 27 .78 .53  32 8.1  .17  11   1.6  56   520 590 11     580   97     240     900   2800    
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unreach-call .48  55 5.6  1.6  33 14   7.4 450 75 16    410 190   .099 26 1.1  .12  26 1.2  .16  12   2.0  170   3800 2500 100     2600   1100     230     1800   3100    
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unreach-call 900     1500 10000    870    970 7200   3.1 270 28 300    290 2800   900     1200 9800    900     1300 13000    900     75   8700    4.7 290 40 900     1700   12000     4.6   290   39    
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unreach-call 900     1500 11000    870    1300 5200   3.2 280 26 890    260 7900   900     830 10000    900     840 12000    900     94   8500    4.9 290 40 16     330   170     4.7   290   40    
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unreach-call 900     1900 11000    870    1700 6900   3.3 280 29 900    270 11000   900     750 9700    900     780 11000    900     15000   13000    4.9 290 38 6.2   320   50     4.8   290   44    
bitvector/jain_5_true-unreach-call_true-no-overflow.i unreach-call 900     1400 13000    380    15000 4800   900   3500 9800 59    75 740   900     11000 10000    900     11000 12000    900     15000   12000    900   700 11000 900     5200   13000     6.3   310   53    
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unreach-call 900     1800 10000    870    1600 4300   3.4 280 29 900    330 7100   900     750 9100    900     750 8900    900     15000   13000    20   310 230 900     2100   10000     8.0   300   86    
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unreach-call 900     1700 11000    870    1700 5900   4.6 280 52 900    370 8800   900     1000 9700    900     1000 9300    900     15000   14000    4.9 290 38 900     2900   13000     5.1   290   44    
bitvector/modulus_true-unreach-call_true-no-overflow.i unreach-call .63  39 8.9  460    1100 2100   220   2100 2400 890    380 7900   180     280 2100    200     330 2200    640     57   8600    14   410 140 110     660   1500     13     500   110    
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unreach-call .12  24 1.2  1.2  33 11   2.4 250 20 7.0  260 89   .090 26 .92 .13  26 .91 .17  11   1.6  270   3300 3300 120     470   1700     59     670   670    
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unreach-call .17  24 1.2  1.2  33 12   16   470 140 22    550 270   .12  26 .88 .14  26 .98 .17  12   2.0  900   1300 8800 240     780   2900     900     1300   12000    
bitvector/parity_true-unreach-call_true-no-overflow.i unreach-call 2.7   44 30    4.1  35 44   120   980 1400 890    150 11000   7.0   28 93    9.4   33 130    7.4   13   99    900   1000 12000 900     720   13000     900     1000   12000    
bitvector/sum02_true-unreach-call_true-no-overflow.i unreach-call 900     1500 12000    880    6300 4400   910   7000 8100 170    480 1700   900     760 12000    900     740 11000    900     770   9900    900   560 11000 900     740   11000     900     650   11000    
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 9.4   220 77    5.9  220 76   8.6 320 68 34    100 370   5.9   87 60    4.0   76 42    .42  13   4.7  24   710 180 900     6300   13000     26     580   210    
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 7.3   240 83    5.2  180 70   26   810 260 55    110 790   6.1   96 63    7.4   110 79    .61  14   8.0  27   650 210 900     6200   13000     27     690   210    
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 7.3   150 67    1.5  64 18   6.1 300 52 18    85 220   2.6   58 26    2.3   51 23    .28  12   3.5  23   580 170 88     1000   1100     24     610   190    
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 46     320 410    21    360 240   15   750 160 170    1300 2000   22     190 260    25     210 240    .59  13   7.6  41   1300 380 900     6300   11000     39     1100   330    
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 8.0   280 95    18    290 240   14   730 120 140    1600 1700   11     160 130    13     170 120    .62  13   6.8  43   1900 360 900     6300   12000     45     1400   360    
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 9.1   250 84    18    280 220   15   750 160 140    1300 2100   10     150 110    12     160 160    .62  13   6.4  25   1000 190 900     6000   13000     270     4800   3700    
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 900     810 9700    870    460 8600   900   4200 8900 890    390 7100   900     360 11000    900     290 11000    900     400   11000    900   2100 13000 900     6400   12000     900     5100   12000    
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 900     7600 9900    870    940 3500   17   760 150 46    2300 550   900     2300 8400    900     2400 11000    900     1100   12000    53   2200 490 900     6500   11000     230     4700   2500    
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unreach-call 900     6700 10000    870    800 3200   51   1300 560 890    360 11000   900     2100 12000    900     2100 8500    900     130   11000    40   1800 350 910     6500   11000     900     5400   14000    
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unreach-call 900     6800 11000    870    840 5800   56   2400 630 890    370 12000   900     2100 8300    900     2000 10000    900     220   10000    41   1800 350 900     6400   10000     900     5000   12000    
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 900     7100 10000    870    860 5600   17   760 160 900    300 11000   900     1800 9500    900     1700 9600    900     210   11000    40   1500 390 900     6400   11000     250     4800   2900    
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call 900     7000 9700    870    840 5600   16   770 170 890    300 11000   900     1800 12000    900     1700 11000    900     210   13000    39   1500 330 900     6500   11000     230     4800   2800    
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call .22  28 2.0  6.1  54 72   12   380 130 14    390 150   4.3   34 52    .35  28 4.4  680     160   9200    110   850 1200 900     1700   11000     110     870   1400    
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call .17  29 1.4  4.5  54 63   110   1300 1300 120    1200 1300   .65  32 7.4  .37  29 3.7  2.8   15   38    26   750 210 900     1500   10000     84     1300   830    
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call 4.0   160 48    4.6  53 63   100   1300 1100 120    1200 1500   .47  30 5.5  .71  30 7.9  4.7   18   62    900   890 9600 900     1400   11000     900     1100   10000    
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call 1.1   36 12    12    52 160   170   400 2400 230    380 3200   23     35 310    1.8   29 21    900     45   12000    490   910 6400 900     1500   12000     860     940   11000    
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c unreach-call .17  28 1.3  4.6  53 53   110   1200 1400 120    1200 1500   .67  32 8.5  .36  29 3.8  2.7   16   35    22   680 210 900     1600   12000     63     1200   620    
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c unreach-call .090 22 1.2  .23 33 1.7 2.5 250 22 .35 48 4.3 .11  28 .83 .082 28 .86 .14  11   1.6  8.0 240 58 8.1   240   70     8.3   240   67    
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c unreach-call .099 22 .83 .23 33 1.6 2.8 270 27 .38 48 4.4 .11  28 .85 .10  28 .91 .16  11   1.7  4.0 240 39 4.2   240   39     4.0   240   37    
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c unreach-call .12  22 .82 .23 33 2.0 2.5 250 21 .38 48 4.2 .13  28 1.1  .13  28 1.2  .14  11   1.4  8.0 240 64 8.2   240   74     9.6   320   76    
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c unreach-call .11  22 .64 2.4  34 22   64   1600 700 4.6  300 46   .75  28 8.6  .74  28 11    900     2500   11000    210   1300 2900 120     1000   1500     290     1200   4000    
bitvector-regression/signextension2_false-unreach-call_true-termination.c unreach-call .13  22 .83 .27 33 2.2 2.6 250 25 480    70 5800   .091 28 .91 .11  28 .64 .13  11   1.7  4.0 230 36 4.1   250   40     4.4   250   34    
bitvector-regression/signextension_false-unreach-call_true-termination.c unreach-call .12  22 .77 .24 33 2.5 2.5 260 26 .39 48 4.2 .080 28 .96 .078 28 .85 .16  11   1.5  4.1 240 36 4.2   250   36     4.1   250   34    
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c unreach-call .10  22 .82 .42 33 3.2 2.6 270 24 3.1  260 29   .070 26 .89 .071 26 .80 .12  11   1.3  4.5 270 38 4.2   250   38     4.3   270   37    
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c unreach-call .12  22 .84 .40 33 4.6 2.4 250 22 3.2  250 28   .089 26 .69 .076 26 .87 .15  11   1.4  8.7 280 67 8.3   250   64     8.9   290   70    
bitvector-regression/signextension2_true-unreach-call_true-termination.c unreach-call .12  22 .74 .40 33 4.3 2.3 240 18 480    250 6100   .072 26 .81 .078 26 .77 .12  11   1.5  4.5 280 35 4.5   260   36     4.7   290   39    
bitvector-regression/signextension_true-unreach-call_true-termination.c unreach-call .12  22 .76 .41 33 4.2 2.3 250 20 3.0  250 31   .097 26 .74 .097 26 .84 .15  11   1.5  4.8 290 37 4.4   260   34     4.7   290   41    
bitvector-loops/diamond_false-unreach-call2.i unreach-call .12  24 1.1  .25 33 2.3 5.3 280 46 1.2  77 14   .55  28 4.8  .60  28 4.8  .16  11   2.0  7.2 340 63 5.9   300   52     13     550   110    
bitvector-loops/overflow_false-unreach-call1.i unreach-call 900     1300 11000    310    15000 4300   900   6800 9300 54    75 710   900     11000 11000    900     11000 12000    .16  11   1.6  900   710 12000 900     2000   11000     900     1500   9700    
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i unreach-call .54  37 6.0  1.0  34 8.9 210   1400 2700 8.0  100 100   2.1   30 18    2.1   29 20    .41  13   5.3  470   780 5400 900     4600   13000     550     2000   8400    
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call 1.3   380 19    1.4  160 15   8.8 340 77 3.3  88 46   1.0   47 12    .98  47 12    .39  16   4.7  54   1300 430 900     5400   13000     58     1300   440    
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .38  65 3.2  .48 41 5.5 6.9 300 53 1.6  94 23   .76  33 7.8  .76  33 6.9  .26  13   3.7  33   940 260 900     5100   11000     33     950   270    
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .54  130 6.2  .76 60 10   8.1 330 65 2.6  100 32   1.0   36 9.6  1.0   36 9.0  .38  14   4.5  48   1200 400 630     4300   9800     50     1300   430    
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .28  41 2.2  .39 38 4.5 5.8 300 47 1.2  63 15   .49  32 4.3  .53  32 4.3  .24  13   2.9  16   660 120 45     1000   460     16     640   130    
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call 1.4   410 15    2.9  160 31   8.3 330 62 18    350 190   .64  45 8.6  .64  45 7.2  .42  16   5.7  100   2400 980 900     5500   12000     900     3900   12000    
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .53  110 5.0  870    4500 3700   100   1300 1300 140    100 1700   900     990 9400    .32  31 3.7  .35  13   3.7  66   1700 570 900     4000   12000     600     4600   6800    
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .36  71 4.7  .84 42 8.7 7.4 310 70 10    350 89   .23  31 2.9  .22  31 2.9  .29  13   3.0  69   1800 650 900     5300   12000     900     4600   12000    
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .58  140 5.9  1.4  60 15   8.0 330 66 13    370 120   .38  34 4.8  .36  34 4.6  .38  14   5.6  71   1800 730 900     3900   12000     900     4600   12000    
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .18  27 1.6  .52 35 5.2 4.9 280 40 5.3  270 47   .13  28 1.5  .12  29 1.2  .19  11   2.4  17   750 150 32     840   310     16     720   140    
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call .27  47 2.6  .63 36 9.3 6.3 290 49 7.1  290 75   .19  30 1.7  .15  30 1.7  .27  12   2.4  17   660 130 41     990   390     17     620   130    
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c unreach-call 9.6   170 69    2.0  87 24   6.4 300 47 20    92 320   2.8   64 27    2.1   56 27    .29  12   3.1  10   550 80 350     4800   5500     10     570   83    
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c unreach-call 10     180 91    2.1  87 23   6.7 300 52 20    85 260   2.8   65 25    2.3   56 24    .28  12   3.4  11   560 87 210     4300   2400     10     550   73    
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c unreach-call 15     230 140    2.4  100 30   6.1 300 46 24    95 390   3.6   75 40    2.8   65 27    .32  12   3.5  15   660 120 250     4100   3000     15     650   120    
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c unreach-call 9.1   180 80    2.1  87 24   6.3 300 49 21    85 290   3.0   65 33    2.4   57 25    .28  12   3.9  11   560 93 200     4200   2400     14     610   120    
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c unreach-call .30  42 2.9  .31 35 3.0 3.8 280 35 4.0  87 49   .35  31 2.9  .63  31 6.8  .26  12   2.6  9.3 480 83 7.8   400   61     9.3   470   73    
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c unreach-call 14     230 110    14    330 170   100   800 1400 24    88 330   3.8   71 38    4.8   86 61    .39  14   5.4  23   780 180 900     6400   12000     39     4300   370    
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c unreach-call 16     230 120    3.5  150 41   160   860 1800 42    98 620   4.1   75 40    3.6   66 36    1.1   23   14    23   820 180 900     6100   12000     710     4900   8400    
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c unreach-call 13     170 96    3.3  140 37   5.4 290 44 16    94 200   2.5   51 22    2.4   44 19    .31  13   3.5  20   730 160 900     6300   12000     21     720   170    
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c unreach-call 4.9   89 37    .32 35 3.1 8.8 380 70 14    90 170   1.3   34 15    1.2   31 15    .23  12   3.4  16   640 120 23     720   190     16     640   130    
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c unreach-call 13     170 100    3.1  140 38   5.9 290 45 21    320 280   1.9   50 14    1.7   44 16    .28  12   3.0  14   620 110 77     2000   880     15     630   130    
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c unreach-call 8.9   150 77    3.0  130 35   5.5 290 45 10    89 120   2.1   49 21    1.7   42 19    .29  12   3.1  16   660 130 69     1600   700     16     660   130    
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c unreach-call .28  43 2.8  .32 37 2.8 3.3 260 29 14    92 180   .33  31 3.5  1.1   31 11    .25  12   2.6  6.5 330 53 7.1   390   51     6.2   320   50    
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c unreach-call 9.0   250 82    25    380 270   13   710 120 150    1300 1800   12     180 130    14     190 160    .60  13   7.2  29   1300 250 900     6400   12000     440     5300   5300    
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c unreach-call 11     250 95    26    390 260   13   720 120 150    1300 1900   12     180 130    14     200 210    .60  13   7.1  35   1500 290 900     6100   12000     500     5400   6500    
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c unreach-call 16     320 140    30    460 420   14   730 140 180    1300 2000   14     210 150    17     240 180    .61  13   7.3  34   1400 240 900     6200   12000     550     5500   6500    
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c unreach-call 9.9   260 86    26    390 300   13   720 120 160    1300 2300   12     180 140    15     200 170    .59  13   8.1  31   1300 250 900     6300   13000     440     5400   5700    
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c unreach-call 900     8200 12000    870    1100 4900   14   730 140 890    470 10000   900     2400 8000    900     2400 11000    900     640   10000    24   1200 190 900     6400   12000     900     5400   12000    
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c unreach-call .61  39 9.0  870    1100 3600   3.1 250 26 370    110 4800   900     1900 9700    900     1900 10000    900     81   10000    7.4 370 59 53     1500   660     7.5   370   56    
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c unreach-call .39  29 4.8  870    2700 5100   2.6 250 24 120    77 1600   900     2300 8900    900     2300 8300    900     58   11000    6.0 300 54 15     590   130     5.7   290   52    
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c unreach-call 900     7800 10000    870    1200 5400   14   730 120 44    2300 470   900     2300 10000    900     2300 8200    900     220   9800    56   2200 500 900     6300   12000     900     5400   11000    
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c unreach-call 900     7800 9700    870    1200 4300   14   730 140 890    460 10000   900     2300 9100    900     2300 8600    900     220   10000    52   2100 480 900     6500   12000     500     4700   5900    
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c unreach-call 900     7800 10000    870    1200 5200   14   730 150 890    460 14000   900     2300 8100    900     2300 9400    900     220   10000    49   2200 430 900     6300   11000     200     4900   2400    
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c unreach-call 900     7800 10000    870    1200 4700   81   2300 1100 890    450 13000   900     2300 9800    900     2200 7700    900     220   10000    34   1300 290 900     6300   12000     900     5400   10000    
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c unreach-call 900     7900 12000    870    1200 6400   46   1300 460 890    470 11000   900     2400 11000    900     2400 8100    900     220   10000    71   2600 650 900     6400   14000     240     4900   3300    
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c unreach-call 900     7800 9400    870    1200 4700   14   740 140 49    2300 590   900     2300 8800    900     2200 8000    900     220   9600    55   2300 580 900     6200   12000     900     5400   12000    
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c unreach-call .14  26 1.3  .31 33 3.0 3.3 270 32 .48 79 6.1 .79  29 6.0  .76  29 6.6  .18  11   1.9  5.8 280 50 5.8   320   46     6.3   280   49    
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c unreach-call .15  28 1.2  .33 36 3.5 3.8 270 34 .50 79 6.5 .82  29 6.2  .86  29 7.0  .16  11   1.9  6.0 290 50 5.4   290   44     6.1   290   49    
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .14  24 1.1  870    3300 6400   15   740 120 30    1300 300   900     2100 8000    .099 27 1.1  .16  11   1.5  18   850 150 31     890   390     20     850   150    
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .14  27 .98 870    4000 5600   44   1200 470 89    2200 1200   900     2300 8200    .11  27 1.1  .13  11   1.5  25   1600 200 39     1100   500     26     1400   180    
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .15  27 1.0  870    4800 7300   150   1300 1900 160    2300 2000   900     2300 7100    .12  27 1.4  .14  11   1.5  38   2600 330 48     1800   560     37     3000   320    
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .14  26 1.0  870    5500 6300   150   1200 1800 160    2300 1900   900     2400 7800    .12  27 1.4  .13  11   1.5  65   4900 560 60     1500   720     51     4600   450    
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .15  26 1.2  870    6200 5700   150   1200 1900 160    2200 1800   900     2500 8400    .14  27 1.4  .13  11   1.8  120   6500 1000 77     1600   910     130     6100   1000    
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .15  26 1.1  870    6900 6300   150   1200 1700 160    2200 2100   900     2500 7400    .14  27 1.3  .14  11   1.5  290   8700 2100 95     2800   1300     290     8800   2000    
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .13  23 .82 870    5900 7800   3.1 250 26 4.3  260 44   900     1700 8100    .12  27 .70 .13  11   1.6  6.6 320 49 8.8   500   82     9.1   390   81    
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .14  23 .86 870    7900 6300   3.5 260 27 4.9  270 50   900     1800 8000    .10  27 1.0  .13  11   1.5  7.4 380 67 12     580   100     7.3   380   62    
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .12  24 .95 870    1900 5600   4.3 270 35 6.3  300 62   900     1900 7500    .11  27 1.1  .16  11   1.4  8.6 510 66 18     680   180     9.2   520   69    
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .12  24 .82 870    2300 5600   6.0 290 47 9.5  450 80   900     2000 7700    .12  27 1.1  .14  11   1.4  11   570 97 20     760   170     11     590   86    
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call .11  24 1.0  870    2800 5100   8.4 430 68 14    720 140   900     2100 7200    .13  27 .84 .13  11   1.7  14   730 120 25     860   290     14     670   120    
ntdrivers/cdaudio_false-unreach-call.i.cil.c unreach-call .56  63 4.3  100    5100 1300   54   1800 580 890    350 11000   900     5800 14000    1.5   290 18    1.0   36   12    900   3100 9800 900     4900   13000     900     5300   12000    
ntdrivers/diskperf_false-unreach-call.i.cil.c unreach-call .60  44 5.3  1.7  120 17   15   510 150 480    170 6900   1.1   87 12    1.0   88 12    .59  29   8.0  16   720 130 60     840   610     20     750   160    
ntdrivers/floppy_false-unreach-call.i.cil.c unreach-call 2.2   59 19    3.5  170 38   11   470 100 590    830 7000   13     460 170    900     1100 11000    .92  43   11    82   3700 790 900     1500   8000     900     6300   11000    
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unreach-call .41  36 3.7  1.5  73 15   12   460 110 890    540 9700   .65  72 8.7  .63  73 9.1  .50  32   5.0  900   2200 6600 900     4400   11000     900     4700   10000    
ntdrivers/parport_false-unreach-call.i.cil.c unreach-call 3.0   100 25    14    790 150   11   470 96 590    960 7900   7.3   350 87    28     490 310    1.7   120   18    100   1300 790 900     1300   10000     150     1400   1400    
ntdrivers/cdaudio_true-unreach-call.i.cil.c unreach-call .53  64 6.1  39    410 470   12   480 110 900    350 11000   .77  280 8.4  .87  280 10    .97  35   13    150   3300 1700 900     4400   13000     900     4800   10000    
ntdrivers/diskperf_true-unreach-call.i.cil.c unreach-call .60  46 6.1  880    7500 5000   99   1900 1300 640    170 8400   .51  83 6.7  .31  82 4.4  .80  40   8.4  160   4700 1600 900     4900   10000