Tool CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 ULTIMATE Automizer f7c3ed31 CPAchecker 1.6.1-svn 24567
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic] Linux 4.4.0-59-generic Linux 4.4.0-67-generic Linux 4.4.0-66-generic Linux 4.4.0-71-generic Linux 4.4.0-67-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]] 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]] 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]] 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]] 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]] 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]] 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]] 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]] 2017-03-17 08:36:49 CET 2017-03-11 00:07:51 CET 2017-03-30 08:12:30 CEST 2017-03-20 21:20:46 CET
Run set cpa-bam-bnb.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] cpa-kind.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] smack.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Sequentialized; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety] bmc-solver-theories.mathsat5-qf_ufbvfp induction-solver-theories.mathsat5-qf_ufbvfp impact-solver-theories.mathsat5-qf_ufbvfp predabs-solver-theories.mathsat5-qf_ufbvfp
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -bmc -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop cpa.predicate.handleFieldAccess=true -setprop solver.solver=mathsat5 -heap 11000M -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -kInduction-dfInvariants -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop cpa.predicate.handleFieldAccess=true -setprop solver.solver=mathsat5 -heap 11000M -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -predicateAnalysis-ImpactRefiner-ABEl -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop cpa.predicate.handleFieldAccess=true -setprop solver.solver=mathsat5 -heap 11000M -noout -disable-java-assertions -setprop cfa.showDeadCode=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop analysis.checkCounterexamples=false -setprop cpa.predicate.abortOnLargeArrays=false -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -predicateAnalysis-PredAbsRefiner-ABEl -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop cpa.predicate.handleFieldAccess=true -setprop solver.solver=mathsat5 -heap 11000M
../sv-benchmarks/c/ status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J) status cputime (s) walltime (s) memory (MB) cpuenergy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 2.64 1.06  280 20.7 901    846     4390 11000   901    838     4310 11600   901     890     745   13400    64.1   63.7   15000   857    901      901      1070   11300     2.74   2.69   85.3  29.4   901    765    5630 12100   909    900     10400 5440   901    416     6220 8740   901    894     733 10800   901    884     6760 10100  
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 2.51 1.06  277 24.3 901    859     2370 10800   901    862     1430 13000   46.3   45.7   159   637    151     150     15000   1070    901      901      501   9030     2.15   2.14   94.5  25.5   901    762    2470 13000   906    902     9320 7900   902    437     3650 5800   901    897     1240 10800   901    891     1600 10600  
array-examples/sorting_bubblesort_false-unreach-call_ground.i 2.37 1.04  266 21.0 901    859     2080 10800   901    863     1420 13900   46.2   45.6   159   607    141     141     15000   1060    901      901      447   7750     2.16   2.13   90.2  27.0   900    759    2270 14300   912    908     9300 8540   902    436     3840 6210   901    896     1250 11100   901    892     1630 11100  
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 2.42 1.01  263 20.1 901    855     2270 11500   901    858     2240 13300   895     895     327   10100    34.1   33.8   15000   320    901      901      400   8580     18.3    17.4    559    231     901    734    2430 12900   912    909     11400 7200   947    478     4640 10500   901    894     659 11600   901    879     5640 10300  
array-examples/sorting_selectionsort_false-unreach-call_ground.i 2.52 1.05  276 21.5 901    855     2130 12500   901    857     2240 10400   895     895     330   8180    33.9   33.6   15000   311    901      901      429   7630     120      119      651    1410     901    731    2990 12700   911    908     11600 7620   902    415     6510 8910   901    894     601 12800   901    879     5520 11000  
array-examples/standard_allDiff2_false-unreach-call_ground.i 2.52 1.05  280 22.8 901    861     2130 12100   901    862     2240 11200   897     895     1470   9260    40.0   39.7   15000   440    901      900      5890   10000     19.6    19.3    131    243     901    745    5740 15000   908    903     9130 9080   902    438     6230 7360   901    893     1170 10900   485    466     15000 6470  
array-examples/standard_copy1_false-unreach-call_ground.i 2.34 1.03  267 19.8 901    863     2220 14200   901    865     2230 12200   78.8   78.1   103   1020    312     311     671   3980    279      277      15000   3290     1.76   1.71   82.6  25.0   901    735    2300 14200   490    487     15000 4770   904    442     5210 6410   901    898     977 11200   901    887     2380 9980  
array-examples/standard_copy2_false-unreach-call_ground.i 2.35 1.03  272 22.0 901    863     2150 11900   901    866     2220 11700   895     895     186   9660    490     490     821   5820    901      901      331   2110     1.81   1.85   77.0  26.5   900    780    3250 12700   505    501     15000 6120   904    443     6340 7160   901    897     1140 10300   901    890     1760 6760  
array-examples/standard_copy3_false-unreach-call_ground.i 2.45 1.06  265 22.1 901    862     2060 13300   901    863     2400 12200   895     895     197   10200    662     662     972   8530    901      901      676   10100     1.89   1.88   79.7  23.5   900    798    4160 12400   565    562     15000 5340   904    442     6270 7570   902    897     1390 10000   901    892     1450 8100  
array-examples/standard_copy4_false-unreach-call_ground.i 2.42 1.03  259 22.7 901    860     2320 12400   901    863     2440 11300   895     895     185   11300    815     814     1120   11400    901      901      662   10300     1.97   1.97   84.5  24.7   900    806    4950 15300   568    565     15000 5540   903    440     6670 6830   902    897     1610 10600   901    893     1360 7930  
array-examples/standard_copy5_false-unreach-call_ground.i 2.46 1.05  261 21.5 901    860     2340 12300   901    865     2400 10800   895     895     213   10800    894     895     1150   10200    901      901      829   8280     2.02   1.98   82.6  28.3   900    805    4970 12700   634    631     15000 5930   904    439     7180 7160   901    896     1770 10000   901    894     1250 8710  
array-examples/standard_copy6_false-unreach-call_ground.i 2.42 1.05  264 20.8 901    860     2140 11700   901    863     2220 12600   895     895     240   9310    895     895     1230   12200    901      901      730   9660     2.10   2.11   88.4  26.3   901    804    5140 13700   633    630     15000 5530   904    441     6420 6590   902    897     1900 9540   901    893     1270 7470  
array-examples/standard_copy7_false-unreach-call_ground.i 2.42 1.03  267 21.9 901    861     2030 11700   901    862     3490 12200   895     895     267   9710    895     895     1300   9950    901      901      745   10500     2.16   2.08   91.4  27.2   901    804    5220 13100   683    679     15000 6370   904    441     6670 7000   902    898     2060 9800   901    893     1240 7070  
array-examples/standard_copy8_false-unreach-call_ground.i 2.37 1.04  268 21.2 901    859     2300 10900   901    865     2210 12500   895     895     302   9870    895     895     1360   10000    901      901      837   12200     2.27   2.23   92.5  25.3   901    810    5130 12100   685    682     15000 6560   904    441     5920 6530   901    896     2240 9140   901    894     1220 7800  
array-examples/standard_copy9_false-unreach-call_ground.i 2.48 1.05  270 23.0 901    859     2130 14500   901    863     3470 11400   895     895     330   9160    895     895     1430   9790    901      901      816   8670     2.29   2.21   93.5  28.2   900    810    5140 12100   753    750     15000 7570   905    442     5840 7000   901    896     2390 11100   901    894     1250 10500  
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 2.50 1.03  279 22.9 901    865     1900 11700   901    869     731 11300   895     895     244   9920    337     337     681   4170    901      901      674   8590     1.88   1.87   84.5  28.9   900    797    4080 13300   642    639     15000 7600   904    443     5570 7310   901    897     960 10800   901    888     2290 11300  
array-examples/standard_init1_false-unreach-call_ground.i 2.56 1.05  277 25.9 901    864     2080 12000   901    869     740 11800   901     868     769   13100    162     161     525   1840    901      901      564   10200     1.73   1.73   76.7  22.6   900    723    2380 15000   766    762     15000 9330   903    442     5040 6540   901    897     732 11200   901    881     4980 9760  
array-examples/standard_init2_false-unreach-call_ground.i 2.56 1.04  285 25.6 901    864     2070 11400   901    868     722 12400   901     869     797   11600    486     486     788   5950    901      901      657   10500     1.74   1.71   85.0  22.8   901    767    2450 12500   757    753     15000 7910   903    441     5060 6760   901    897     715 11000   901    896     497 10700  
array-examples/standard_init3_false-unreach-call_ground.i 2.51 1.02  282 20.9 901    864     1990 13200   901    868     763 11800   901     869     710   14200    789     789     1050   11000    901      901      539   9910     1.78   1.73   85.9  23.3   901    791    2740 12800   759    755     15000 8520   903    441     5480 8210   901    897     719 12500   901    882     4760 9780  
array-examples/standard_init4_false-unreach-call_ground.i 2.40 1.01  262 20.7 901    863     2110 12700   901    868     781 13000   901     869     751   10500    895     895     1170   11600    901      901      692   9260     1.81   1.73   81.9  22.6   901    799    3510 12700   761    757     15000 8080   903    440     5640 6880   901    897     709 11700   901    881     4710 10600  
array-examples/standard_init5_false-unreach-call_ground.i 2.43 1.05  264 21.3 901    864     2270 11900   901    868     735 11500   895     895     229   9390    895     895     1280   12500    901      901      649   9030     1.81   1.78   79.1  20.8   900    800    3750 14200   754    750     15000 9110   903    440     5250 6870   901    897     688 11500   901    882     4630 10500  
array-examples/standard_init6_false-unreach-call_ground.i 2.56 1.04  276 23.3 901    863     1900 11600   901    868     855 11300   895     895     239   11200    895     896     1400   10200    901      901      769   8170     1.84   1.87   85.9  22.0   900    802    5120 14100   758    754     15000 7930   903    440     5340 6070   901    897     672 12800   901    882     4520 10200  
array-examples/standard_init7_false-unreach-call_ground.i 2.58 1.05  275 20.4 901    864     1770 11500   901    867     795 14000   895     895     266   11000    895     895     1510   9980    901      901      452   1930     1.90   1.89   79.8  25.0   900    806    5070 11900   770    766     15000 8200   903    439     5710 6940   901    896     721 12500   901    882     4520 11700  
array-examples/standard_init8_false-unreach-call_ground.i 2.64 1.03  274 24.6 901    863     2130 13500   901    867     759 11400   895     895     293   8210    894     895     1630   10400    901      901      891   10900     1.89   1.88   77.9  25.7   900    805    5100 13600   767    763     15000 9230   903    438     6220 7290   901    897     710 10900   901    882     4420 11200  
array-examples/standard_init9_false-unreach-call_ground.i 2.53 1.01  266 21.2 901    863     1980 14300   901    866     758 11000   895     895     320   8390    894     895     1760   12300    901      901      743   8940     1.90   1.87   81.0  26.5   901    805    5260 11400   764    760     15000 7920   903    440     5760 6660   901    896     723 11100   901    882     4280 12600  
array-examples/standard_minInArray_false-unreach-call_ground.i 2.52 1.05  277 19.9 901    861     2300 11100   901    864     2230 12700   97.3   96.6   116   1450    33.1   33.1   1280   380    660      658      15000   8090     1.87   1.88   90.0  22.7   900    763    2330 12100   906    901     8840 9480   902    439     3290 6610   901    897     477 13900   901    879     5690 10800  
array-examples/standard_partition_false-unreach-call_ground.i 2.50 1.05  278 21.2 901    859     2330 11600   901    861     2200 12000   901     862     2230   11000    895     895     11600   10100    901      901      634   8800     2.04   1.96   90.6  29.1   900    803    3050 12000   907    903     9950 7310   903    436     6630 7730   902    897     1650 10300   901    892     1980 10000  
array-examples/standard_running_false-unreach-call.i 2.60 1.04  280 21.0 901    860     2520 12400   901    862     2240 11600   895     895     305   10500    895     895     1360   12700    901      901      727   9470     2.26   2.34   101    23.3   900    803    3330 14700   909    905     9900 8560   905    441     7580 6890   901    896     956 12200   901    887     2230 7580  
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2.73 1.20  277 22.2 3.89 1.21  275 26.2 156    144     2250 1880   895     895     1240   11700    61.3   60.9   15000   611    901      901      1220   8790     2.29   2.24   101    26.8   7.13 2.17 341 57.3 901    896     977 11700   3.40 1.14  304 29.1 901    894     1090 12000   902    886     6400 12000  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 2.54 1.06  275 23.3 901    869     3990 12100   901    857     3710 12400   895     895     259   8260    63.5   63.2   15000   757    901      901      1340   9820     881      880      221    9920     901    787    5330 13900   905    895     5410 4820   931    441     7160 8910   901    894     962 10400   901    884     6630 10800  
array-examples/relax_true-unreach-call.i 7.56 2.43  413 57.4 953    477     3780 9190   903    476     4950 8030   895     895     186   11200    895     895     3190   10100    901      901      491   7660     881      880      369    10800     901    846    1100 12500   936    883     5830 9520   916    439     5640 8470   901    894     701 11600   901    865     13400 10200  
array-examples/sanfoundry_02_true-unreach-call_ground.i 2.36 1.02  266 23.6 901    858     2230 11500   901    862     2240 11700   310     309     177   3740    901     901     440   10400    901      900      6370   11000     1.47   1.51   77.3  21.2   900    785    2160 14700   903    899     3290 8540   902    439     4000 7240   901    896     523 10700   901    879     5620 11800  
array-examples/sanfoundry_10_true-unreach-call_ground.i 901    823     4160 8770   30.8  5.93  1200 200   904    602     5710 11300   895     895     182   9760    895     896     2630   13100    901      901      999   10100     4.22   4.13   90.9  60.0   901    839    1410 12100   923    877     7380 8090   904    436     7640 8160   901    897     820 10900   901    889     2620 12700  
array-examples/sanfoundry_24_true-unreach-call.i 2.67 1.03  273 24.0 901    865     3910 11300   901    860     3900 12700   900     860     3930   11600    40.0   40.0   1740   560    .0812 .0819 23.2 .989 881      880      311    12500     8.02 2.29 368 66.5 903    894     3170 7710   4.45 1.27  313 34.1 2.31 .973 230 23.1 2.30 .984 207 21.9
array-examples/sanfoundry_27_true-unreach-call_ground.i 2.49 1.03  280 20.3 901    862     2170 11800   901    863     2240 11700   116     115     117   1450    901     901     360   10100    901      899      14100   12300     1.84   1.88   76.8  19.8   901    764    2310 13400   905    900     5740 8620   902    440     3090 6520   901    897     484 11200   901    880     5720 11000  
array-examples/sanfoundry_43_true-unreach-call_ground.i 2.75 1.16  282 24.7 2.88 1.01  266 23.5 92.7  87.6   2260 1200   51.8   51.1   103   755    .797 .796 65.3 8.36 .0897 .0887 23.1 1.05  1.19   1.22   68.6  14.2   5.55 1.81 319 42.5 2.03 .887 216 17.2 3.03 .982 305 26.6 2.11 .878 224 19.0 2.08 .923 223 18.5
array-examples/sorting_bubblesort_true-unreach-call_ground.i 2.51 1.04  280 20.9 901    860     2420 11700   901    863     2220 12800   46.2   45.6   158   631    153     152     15000   1010    901      901      493   9650     23.4    23.2    143    264     901    757    2360 12500   912    908     12000 8210   902    437     3810 9090   902    897     1240 12200   901    892     1660 10700  
array-examples/sorting_selectionsort_true-unreach-call_ground.i 2.63 1.03  277 20.7 901    855     2080 13900   901    857     2240 11000   895     895     377   8890    34.2   33.9   15000   333    901      901      407   8310     882      931      769    9940     901    729    3250 13500   912    908     11200 6990   902    432     4650 8880   901    893     601 11500   901    879     5580 10100  
array-examples/standard_compareModified_true-unreach-call_ground.i 2.60 1.05  281 23.6 901    859     2340 14200   901    861     2230 12700   895     895     219   10500    29.2   29.2   2340   441    901      901      779   10300     1.38   1.36   74.7  20.5   900    762    2590 13500   906    902     9220 6750   903    439     4320 7170   901    896     1060 10600   901    891     1760 9250  
array-examples/standard_compare_true-unreach-call_ground.i 2.58 1.09  286 22.1 901    863     3660 12000   901    863     2430 11000   111     111     174   1290    12.7   12.7   1210   163    349      347      15000   4650     1.72   1.77   74.4  20.5   900    744    2700 12500   806    800     15000 8870   903    441     4430 5650   901    893     521 10200   901    896     494 12800  
array-examples/standard_copy1_true-unreach-call_ground.i 2.44 1.03  266 20.3 901    864     2230 11400   901    866     2410 14300   895     895     205   9250    3.92  3.92  422   52.1  901      902      652   9470     1.61   1.59   82.3  29.1   900    734    3710 14100   511    507     15000 4760   904    443     6040 7900   901    897     939 12200   901    887     2290 8940  
array-examples/standard_copy2_true-unreach-call_ground.i 2.33 1.04  265 23.3 901    862     3660 13800   901    864     2230 11000   895     895     263   8370    4.07  4.07  446   45.8  901      901      627   10400     1.78   1.78   78.0  20.2   900    777    3360 12500   522    518     15000 5040   904    443     6260 7230   901    897     1160 11100   901    890     1780 9850  
array-examples/standard_copy3_true-unreach-call_ground.i 2.51 1.04  265 21.1 901    862     2180 10600   901    862     2230 13100   895     895     296   9260    4.23  4.23  471   47.8  901      901      641   10100     1.77   1.77   83.2  20.2   900    797    3830 14100   558    555     15000 6000   904    441     6220 6890   902    897     1370 11900   901    892     1430 7620  
array-examples/standard_copy4_true-unreach-call_ground.i 2.44 1.05  270 22.6 901    860     2250 13000   901    864     3500 10600   895     895     331   10200    4.33  4.33  495   53.6  901      901      365   1640     1.91   1.86   87.0  25.1   900    804    4430 13600   577    573     15000 5040   904    441     6120 6510   901    897     1540 10800   901    893     1410 11200  
array-examples/standard_copy5_true-unreach-call_ground.i 2.47 1.06  266 22.1 901    860     2200 10800   901    862     2220 12400   895     895     272   9740    4.49  4.49  520   52.5  901      901      662   9030     2.00   1.95   86.6  25.7   900    806    4910 13800   622    618     15000 5600   903    438     6290 8000   902    897     1740 10700   901    894     1230 7770  
array-examples/standard_copy6_true-unreach-call_ground.i 2.59 1.15  262 22.3 901    863     2370 13000   901    865     2410 10500   895     895     273   8400    4.70  4.70  546   55.3  901      901      638   9030     2.14   2.08   90.3  28.4   900    804    5130 13500   639    635     15000 5310   904    441     6730 7340   901    897     1890 10500   901    894     1260 10100  
array-examples/standard_copy7_true-unreach-call_ground.i 2.43 1.05  264 21.0 901    859     3700 10600   901    865     2210 12400   895     895     315   8920    4.79  4.79  571   63.1  901      901      678   9070     2.22   2.17   94.0  28.4   900    808    5190 14100   694    690     15000 6420   903    440     6850 7440   902    897     2120 10000   901    894     1210 7390  
array-examples/standard_copy8_true-unreach-call_ground.i 2.48 1.03  262 22.5 901    859     2520 13300   901    861     2220 13600   895     895     402   11600    4.95  4.95  596   57.6  901      901      727   9850     2.49   2.38   92.4  28.2   901    809    5040 12500   675    671     15000 7370   903    440     6690 8160   902    898     2270 8730   901    894     1240 9900  
array-examples/standard_copy9_true-unreach-call_ground.i 2.45 1.06  267 24.5 901    860     1900 14100   901    864     2210 10100   895     895     339   7610    5.18  5.19  622   70.3  901      901      680   8210     2.48   2.44   99.8  29.7   901    809    5090 12500   732    729     15000 8870   904    440     5790 7740   902    895     2430 9930   901    895     1220 10600  
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 2.54 1.01  280 23.2 901    863     1980 11700   901    869     694 13800   895     895     158   10100    4.28  4.28  470   49.9  901      901      315   2380     2.09   2.09   83.1  28.4   901    800    3550 11500   637    633     15000 6970   903    441     5590 7080   901    898     989 10800   901    887     2210 9320  
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 2.51 1.04  280 21.9 901    863     2030 12700   901    868     780 12100   895     895     223   12200    4.44  4.45  494   47.8  901      901      583   9810     2.51   2.48   88.4  34.6   900    806    4440 12500   642    638     15000 7710   902    439     5160 6870   901    897     921 12700   901    888     2240 9710  
array-examples/standard_copyInitSum_true-unreach-call_ground.i 2.51 1.03  278 21.8 901    864     3670 12400   901    869     784 13300   895     895     182   8060    4.29  4.29  471   54.6  901      901      500   8350     1.96   1.96   81.3  23.7   900    798    3250 11300   635    631     15000 6640   903    441     5300 7240   901    897     957 12000   901    887     2230 9460  
array-examples/standard_copyInit_true-unreach-call_ground.i 2.66 1.03  275 21.1 901    864     1810 12400   901    869     745 11000   895     895     217   11100    4.08  4.08  445   56.2  901      901      552   9780     1.68   1.66   77.5  21.8   900    780    2870 13300   638    634     15000 5890   904    442     5310 6350   901    898     976 11600   901    887     2160 9670  
array-examples/standard_find_true-unreach-call_ground.i 2.64 1.05  277 23.9 901    863     1930 12000   901    865     2400 11500   901     865     2230   11400    14.6   14.6   896   220    901      901      599   10300     2.39   2.38   80.7  26.7   901    733    2870 12500   460    456     15000 4680   902    435     5640 7380   901    897     726 10900   901    881     4990 10700  
array-examples/standard_init1_true-unreach-call_ground.i 2.53 1.02  277 24.0 901    864     2090 13000   901    869     821 11400   901     869     735   11300    3.94  3.94  421   47.3  901      901      518   9710     1.55   1.51   74.3  18.9   901    726    3430 12200   760    756     15000 7280   903    441     4950 6610   901    897     722 12600   901    896     501 12400  
array-examples/standard_init2_true-unreach-call_ground.i 2.58 1.06  279 21.8 901    864     2150 11600   901    868     694 10000   901     869     733   10800    4.08  4.08  445   50.5  901      901      558   9670     1.65   1.62   85.9  21.6   900    767    2410 12700   765    761     15000 8220   903    442     5350 7070   901    897     726 11200   901    881     4970 12900  
array-examples/standard_init3_true-unreach-call_ground.i 2.38 1.03  265 21.9 901    864     1920 13400   901    869     710 11000   901     868     786   11200    4.14  4.14  468   50.5  901      901      623   8850     1.68   1.62   78.2  22.0   901    791    2810 11300   760    756     15000 7710   902    440     5530 6950   901    897     740 11100   901    881     4770 10400  
array-examples/standard_init4_true-unreach-call_ground.i 2.50 1.02  266 19.9 901    864     2030 11600   901    870     897 11700   901     868     743   12000    4.27  4.27  491   50.2  901      901      415   1870     1.78   1.78   75.0  21.1   900    793    3740 13400   759    755     15000 8580   903    441     5500 6970   901    897     750 11500   901    882     4750 10700  
array-examples/standard_init5_true-unreach-call_ground.i 2.51 1.04  279 21.3 901    864     2100 12500   901    869     715 13000   895     895     212   9610    4.40  4.40  514   51.4  901      901      785   10500     1.86   1.88   78.3  22.9   900    802    4090 14000   755    751     15000 8920   903    440     4950 6550   901    897     715 11800   901    883     4630 10800  
array-examples/standard_init6_true-unreach-call_ground.i 2.46 1.08  262 19.7 901    863     2080 11600   901    868     773 12700   895     895     239   12200    4.51  4.51  537   52.1  901      901      787   8380     1.91   1.89   82.8  22.8   900    800    5020 13100   768    763     15000 7750   903    440     5140 6580   901    897     721 10600   901    882     4580 9860  
array-examples/standard_init7_true-unreach-call_ground.i 2.44 1.04  263 21.0 901    863     1960 13400   901    868     731 12600   895     895     266   9230    4.67  4.67  560   57.4  901      901      755   12400     1.99   1.99   83.5  24.1   900    802    5040 12600   775    771     15000 8630   903    440     5210 6380   901    897     693 10500   901    881     4500 10800  
array-examples/standard_init8_true-unreach-call_ground.i 2.49 1.05  283 22.0 901    863     2310 13200   901    867     743 11700   895     895     293   12100    4.71  4.71  584   69.5  901      901      772   10200     2.01   1.98   86.0  24.4   901    801    5250 12500   766    762     15000 8800   903    439     5530 8690   901    896     732 12900   901    882     4380 10400  
array-examples/standard_init9_true-unreach-call_ground.i 2.76 1.07  279 21.5 901    864     3640 10900   901    867     743 11500   895     895     320   9730    4.89  4.88  607   53.9  901      901      482   2310     2.06   2.07   80.8  27.2   901    809    5080 13700   761    757     15000 7760   903    439     5140 6450   901    896     728 12300   901    882     4260 10900  
array-examples/standard_maxInArray_true-unreach-call_ground.i 2.48 1.02  281 20.7 901    861     2650 13400   901    863     2230 11200   118     118     149   1570    901     901     314   10000    901      897      5040   1820     1.86   1.87   72.6  24.0   900    761    2360 12900   906    901     5960 8610   902    440     3330 5950   901    897     485 11000   901    879     5590 11300  
array-examples/standard_minInArray_true-unreach-call_ground.i 2.48 1.01  279 19.4 901    861     2510 11700   901    863     2220 13800   99.9   99.1   120   1470    901     901     348   10700    717      715      15000   10300     1.86   1.86   72.7  23.5   900    760    2180 12400   906    901     8840 8870   903    441     5010 6310   901    898     491 10900   901    879     5560 10400  
array-examples/standard_palindrome_true-unreach-call_ground.i 2.49 1.05  266 23.0 901    863     2060 12800   901    866     2220 11000   895     895     157   9220    3.98  3.98  423   48.9  901      901      505   8610     1.42   1.39   80.7  17.8   901    736    2570 13200   444    440     15000 4940   904    442     6770 6720   901    898     745 12700   901    882     5050 8160  
array-examples/standard_partial_init_true-unreach-call_ground.i 2.40 1.07  266 20.6 901    859     2500 14600   901    862     1390 13100   901     863     1410   10700    901     901     2350   6600    901      901      331   2600     116      116      100    1690     901    761    2690 13500   907    903     9810 6530   902    439     3150 6970   902    897     1710 10700   901    891     1900 9720  
array-examples/standard_partition_original_true-unreach-call_ground.i 2.60 1.01  280 21.2 901    858     2620 12200   901    861     2240 11100   901     862     2250   11900    901     901     2210   9640    901      901      599   12000     64.2    64.2    95.0  821     900    757    2300 11900   906    902     7140 6450   902    436     6640 8850   901    897     2640 11400   901    892     1850 9540  
array-examples/standard_partition_true-unreach-call_ground.i 2.53 1.03  281 21.0 901    857     2540 14200   901    865     2180 11100   895     895     247   9220    901     901     1700   9160    901      901      758   8510     21.4    21.4    85.7  333     900    803    3120 14300   906    903     9930 9150   904    439     5760 6000   902    898     1490 10500   901    887     2400 8810  
array-examples/standard_password_true-unreach-call_ground.i 2.60 1.06  276 23.3 901    859     2450 13500   901    863     2230 9920   112     111     166   1430    12.7   12.7   1210   163    902      895      10300   1740     1.67   1.65   81.5  20.3   900    742    2660 13000   827    821     15000 9640   903    441     5570 7770   901    893     654 12600   901    897     443 12600  
array-examples/standard_reverse_true-unreach-call_ground.i 2.38 1.02  263 22.8 901    864     2200 11000   901    867     2220 11100   895     895     182   9300    435     435     684   5660    901      901      703   10300     1.66   1.61   80.4  24.7   901    734    2640 14200   480    477     15000 5380   905    444     8540 7380   901    897     1000 13800   901    887     2260 9930  
array-examples/standard_running_true-unreach-call.i 2.61 1.05  278 19.6 901    860     2550 12000   901    862     2240 11700   895     895     262   9440    901     901     1230   9740    901      901      735   10400     1.72   1.82   71.2  25.4   900    803    3100 12600   910    906     9840 8450   906    441     7680 7330   901    896     924 10200   901    888     2190 9270  
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2.35 1.03  263 23.3 901    855     3850 11800   901    864     2370 12900   101     101     75.5 1330    14.3   14.3   135   189    901      901      6160   10200     1.58   1.60   85.9  20.5   8.25 2.53 419 64.2 901    898     752 11300   902    440     2770 9640   49.6  47.5   295 700   3.32 1.55  284 30.3
array-examples/standard_seq_init_true-unreach-call_ground.i 2.50 1.04  279 21.8 901    864     3670 14000   901    868     802 12300   901     869     743   11900    3.95  3.95  423   46.5  901      901      559   9690     1.72   1.72   78.9  21.6   901    726    2140 13800   684    680     15000 7180   903    442     5660 8400   901    897     762 10300   901    880     5050 10400  
array-examples/standard_strcmp_true-unreach-call_ground.i 2.59 1.06  285 23.8 901    861     3680 11900   901    863     3470 10900   120     119     128   1390    5.63  5.63  554   69.7  901      899      7420   12500     1.68   1.68   74.0  19.8   901    743    5300 11000   467    460     15000 5950   904    442     5370 6410   901    892     564 10700   901    895     559 12600  
array-examples/standard_strcpy_original_true-unreach-call.i 2.38 1.02  263 20.5 901    862     2010 11800   901    863     2430 9950   901     864     2240   12400    894     895     1160   11600    901      901      446   8590     6.14   6.04   96.9  76.7   900    726    2800 11900   463    459     15000 5410   903    439     4020 8120   901    896     976 10700   901    885     2280 10500  
array-examples/standard_strcpy_true-unreach-call_ground.i 2.42 1.05  264 23.7 901    863     2050 11700   901    865     2240 11500   895     895     304   9900    901     901     1170   13300    901      901      488   12600     4.20   4.18   90.4  64.4   901    727    2710 12900   463    460     15000 5020   903    436     6250 7770   901    897     982 10900   901    886     2250 9970  
array-examples/standard_two_index_01_true-unreach-call.i 2.43 1.01  281 20.2 901    861     2120 13100   901    861     2230 11400   895     895     226   12200    4.43  4.43  485   51.1  901      901      670   9610     883      931      903    13500     901    764    1530 12300   508    504     15000 3680   903    442     4340 7730   901    898     1020 11600   901    888     2030 8630  
array-examples/standard_two_index_02_true-unreach-call.i 2.35 1.02  263 22.0 901    863     2290 11500   901    867     2210 12100   895     895     212   8840    4.42  4.42  485   61.0  901      901      831   10800     1.46   1.42   79.0  19.3   901    764    1550 10900   492    489     15000 4970   903    442     4720 6420   901    897     1000 10300   901    888     2120 8960  
array-examples/standard_two_index_03_true-unreach-call.i 2.35 1.01  268 21.3 325    276     2740 4670   361    306     3260 4070   895     895     222   9660    4.43  4.43  485   57.5  901      901      699   10300     898      931      4100    11900     901    762    1610 12000   481    477     15000 5630   903    688     4620 7260   901    897     1010 11900   901    888     2100 9510  
array-examples/standard_two_index_04_true-unreach-call.i 2.51 1.03  283 22.7 901    863     2210 13000   901    866     2220 13600   895     895     168   9890    4.42  4.42  485   61.0  901      901      709   9160     1.41   1.51   95.0  17.4   901    767    1540 12900   473    469     15000 5540   903    442     5550 7660   901    897     1020 13100   901    889     2070 10900  
array-examples/standard_two_index_05_true-unreach-call.i 2.49 1.04  267 22.2 901    863     2510 10900   901    865     2410 13500   895     895     179   8790    4.45  4.45  485   54.1  901      901      608   7940     1.36   1.40   82.5  15.9   900    756    1650 11500   484    480     15000 4560   905    444     5550 6460   901    897     1000 11000   901    890     2160 12100  
array-examples/standard_two_index_06_true-unreach-call.i 2.61 1.04  282 23.7 95.9  70.8   3880 1060   98.5  71.2   3960 1180   895     895     170   9220    4.41  4.41  485   52.7  901      901      689   8720     891      931      1040    11400     901    761    1440 12300   469    466     15000 4650   903    840     5650 8260   901    898     996 10200   901    888     2000 9350  
array-examples/standard_two_index_07_true-unreach-call.i 2.56 1.05  279 24.4 901    864     1980 10500   901    866     2210 14400   895     895     190   8730    4.54  4.54  485   52.3  901      901      610   9630     1.39   1.45   76.2  17.4   901    766    1480 11500   468    465     15000 5190   903    442     4750 7150   901    897     1020 10700   901    889     2070 10800  
array-examples/standard_two_index_08_true-unreach-call.i 2.61 1.01  274 20.2 901    863     2310 12400   901    861     2220 11000   895     895     175   9790    4.46  4.46  485   58.3  901      901      693   13100     1.40   1.47   80.3  15.8   900    760    1510 12300   467    463     15000 4900   903    442     5440 6990   901    897     990 11300   901    888     1960 8660  
array-examples/standard_two_index_09_true-unreach-call.i 2.53 1.03  280 21.7 901    863     2120 11600   901    858     2070 11300   895     895     170   9860    4.44  4.44  486   53.4  901      901      642   8540     1.34   1.32   74.5  18.1   901    759    1480 13700   478    475     15000 4530   903    442     5530 8250   901    897     1000 10000   901    889     2060 9620  
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 2.36 1.01  263 24.2 901    856     2980 12000   901    861     2510 11700   97.2   96.3   103   1410    13.7   13.7   851   184    346      344      15000   5130     881      880      482    11600     901    749    2870 13200   927    866     12900 8380   903    438     5670 6450   901    895     1600 10400   901    894     568 10400  
array-examples/standard_vector_difference_true-unreach-call_ground.i 2.50 1.02  280 20.2 901    863     2150 11700   901    862     2240 11600   901     865     2220   11700    3.94  3.94  424   46.1  901      901      500   10000     2.10   2.08   76.2  22.2   901    728    4410 11800   912    909     9300 9730   903    442     5910 6510   901    898     1190 10100   901    891     1740 9620  
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i 2.34 1.02  262 22.9 901    864     1780 11900   901    869     865 13700   895     895     321   8890    524     524     827   7190    901      901      697   2100     1.76   1.70   80.6  21.4   901    773    1820 11200   759    755     15000 7750   903    443     5280 8160   901    898     705 13500   901    880     5060 12600  
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 900    833     4340 11000   903    295     3790 7350   903    606     4200 11400   895     895     305   8310    60.7   60.7   4900   449    901      901      1440   8490     1.76   1.69   79.7  21.9   900    864    5230 9000   670    666     15000 6670   903    442     5350 8960   901    898     707 9770   901    880     5080 12100  
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i 2.53 1.06  281 21.7 901    861     2600 12700   901    861     2240 9910   895     895     234   9620    14.3   14.3   1070   160    901      901      548   10400     2.49   2.38   87.5  26.9   901    795    3120 11300   903    899     3780 6830   903    442     4650 6220   902    897     1650 9230   902    893     2110 11900  
array-industry-pattern/array_range_init_false-unreach-call.i 2.56 1.04  274 23.9 901    863     2170 11000   901    866     748 12000   895     895     195   8480    667     667     790   6950    901      901      485   9610     1.78   1.71   87.2  24.7   901    847    4900 8470   670    666     15000 6410   903    442     5070 6310   901    896     730 11700   901    880     4860 11700  
array-industry-pattern/array_single_elem_init_false-unreach-call.i 2.60 1.04  276 21.1 901    861     2430 13500   901    863     2260 12600   895     895     250   11200    14.1   14.1   1070   155    901      901      537   13100     2.45   2.38   93.9  29.6   900    802    3170 12500   905    901     5710 6380   903    441     4830 5660   901    897     2260 8180   901    893     2060 9310  
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 901    727     5660 9680   961    351     4210 10000   902    594     5860 9810   901     592     5970   8710    901     901     4180   11800    901      901      944   7620     4.94   4.79   106    63.8   900    768    3960 13000   905    894     5430 7460   914    445     4550 10300   901    893     1120 9890   902    883     6280 12100  
array-industry-pattern/array_monotonic_true-unreach-call.i 2.41 1.10  261 21.4 901    862     2350 12800   901    864     1820 11000   895     895     343   11800    901     901     730   9440    901      901      601   9230     1.58   1.57   74.6  17.1   901    787    1730 12000   904    900     5460 8030   903    441     4360 7270   901    897     1330 9250   901    889     2130 10900  
array-industry-pattern/array_mul_init_true-unreach-call.i 2.45 1.04  267 23.0 901    860     2230 12000   901    866     810 10200   895     895     1720   10200    901     901     1280   10400    901      901      733   8580     881      931      169    12600     901    784    2380 13600   777    773     15000 7470   904    440     6270 7850   902    896     1470 10900   902    890     2700 9370  
array-industry-pattern/array_of_struct_break_true-unreach-call.i 901    841     4270 9650   902    294     4310 6280   903    610     2990 8310   895     895     207   9420    70.0   70.0   5190   581    901      901      737   9630     1.66   1.67   80.1  18.7   900    862    4940 8380   904    896     5650 6140   903    441     4670 6950   901    897     732 12500   901    894     649 11900  
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 901    819     4250 9240   902    294     3510 5280   902    606     3730 8240   902     605     3840   10200    320     320     15000   2600    .324  .323  23.4 .639 4.19   4.19   87.7  48.6   900    874    5450 8850   904    900     3570 5520   903    440     4250 8880   901    896     3710 8210   901    894     1140 7690  
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 908    187     10800 4300   903    291     5410 6370   903    603     4670 8430   533     533     670   4920    130     131     11700   934    815      810      15000   9350     1.80   1.77   77.0  21.7   901    765    4220 13300   903    899     4690 8710   905    440     8900 7800   901    897     969 12600   901    886     3310 11100  
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 901    821     4260 8980   902    293     3860 5160   902    607     4080 7920   902     606     4050   8170    327     326     15000   2940    .320  .317  23.3 .813 1.79   1.77   78.5  23.1   901    876    5460 8010   904    900     4480 6740   902    441     4070 9640   903    898     3060 8770   901    894     1030 6450  
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 901    816     4970 9660   903    295     4650 7060   903    607     4000 7780   895     895     236   9320    345     345     15000   2270    901      901      836   8920     881      931      677    9800     900    872    5200 8420   601    596     15000 4930   904    441     5120 6150   902    897     1390 10400   902    884     3880 12000  
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 901    806     3860 11900   903    294     6310 7220   903    605     4770 8260   895     895     358   8610    70.5   70.5   4690   477    901      901      900   8540     7.39   7.35   94.4  91.1   8.05 2.59 309 60.2 912    908     12600 8670   904    439     6670 8640   902    897     1810 12000   901    886     2610 10000  
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 901    849     4000 10400   902    294     4080 6700   903    605     3710 8920   895     895     405   7920    174     174     13900   1020    901      901      1040   10100     1.59   1.57   85.4  18.9   901    876    5470 7000   571    567     15000 6210   903    440     4820 6670   901    897     714 12000   901    881     4760 11700  
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 901    745     6450 8190   902    294     5130 5000   902    606     4450 7750   895     895     367   8690    479     479     15000   4340    901      901      1420   8810     14.1    14.0    104    199     900    872    5390 8580   902    898     2260 5720   902    439     4400 6500   901    897     9360 9420   901    894     2620 7530  
array-industry-pattern/array_shadowinit_true-unreach-call.i 906    404     11200 6360   336    104     5040 2740   904    538     3820 9230   902     538     3580   8060    894     895     1250   11700    901      901      879   9150     881      880      390    12900     901    749    1680 13900   906    897     6520 5790   903    441     5920 6100   626    620     658 8850   901    894     533 11600  
reducercommutativity/rangesum05_false-unreach-call.i 5.29 2.48  388 53.7 47.2  17.5   1180 343   34.7  29.2   562 459   486     486     181   5730    .200 .199 23.5 2.37 2.01   2.01   120   22.6   1.61   1.60   75.2  21.7   18.0  10.6  487 201   4.18 2.49  384 35.5 164    153     2670 1440   25.4  23.0   374 305   31.8  27.6   436 331  
reducercommutativity/rangesum10_false-unreach-call.i 7.22 3.15  408 57.8 118    52.0   1800 929   113    104     732 1470   501     501     182   5810    .237 .235 23.3 3.28 12.2    12.2    255   148     1.69   1.67   73.4  20.1   32.3  20.6  552 441   5.93 3.86  436 53.8 903    891     4850 8250   103    96.9   436 1130   108    102     666 1220  
reducercommutativity/rangesum20_false-unreach-call.i 13.3  8.32  567 126   290    137     1970 3130   905    884     5270 8800   653     653     183   8990    .431 .430 24.3 4.80 121      121      598   1180     1.86   1.88   75.4  24.5   73.9  50.8  837 729   9.67 7.17  652 88.6 903    890     6360 7630   507    499     588 5270   636    626     1140 6950  
reducercommutativity/rangesum40_false-unreach-call.i 61.2  25.1   1890 448   954    490     8150 11100   904    878     3990 8440   895     895     181   10800    6.05  6.05  35.6 77.6  901      902      1100   8950     2.27   2.20   94.4  28.9   148    110    2720 1550   19.4  16.6   1010 174   904    888     4970 8840   901    893     616 9500   901    889     1430 8280  
reducercommutativity/rangesum60_false-unreach-call.i 110    70.4   4210 993   944    480     7950 10400   904    877     4050 10900   895     895     182   9140    .958 .954 31.9 12.8  901      901      815   2210     2.83   2.72   123    35.3   268    223    4430 3130   36.5  32.8   1550 355   903    885     4270 8040   901    892     648 10000   901    889     1770 8460  
reducercommutativity/rangesum_false-unreach-call.i 13.5  4.19  586 105   261    79.7   4620 2180   175    164     2240 1800   486     486     180   5990    895     895     2810   9170    1.51   1.51   159   15.7   2.00   1.97   78.8  29.6   13.9  4.69 527 102   269    259     2490 1510   865    416     5580 5950   901    893     624 9020   22.6  19.5   400 244  
reducercommutativity/avg05_true-unreach-call.i 901    898     1540 9110   905    447     3180 5490   902    889     1740 10400   901     889     2170   9110    145     145     89.7 1800    1.88   1.88   95.2 20.9   1.29   1.38   67.9  17.2   211    186    1250 2570   901    898     884 7920   901    891     2390 8160   901    898     1940 8350   901    897     1910 9230  
reducercommutativity/avg10_true-unreach-call.i 901    897     1940 8660   908    447     4000 7270   902    889     3340 8910   901     887     3560   8750    901     901     271   10700    16.1    16.1    185   184     1.30   1.35   66.8  17.5   386    342    1600 4540   901    898     1240 8490   902    889     4040 8740   901    898     2100 8330   901    895     758 10600  
reducercommutativity/avg20_true-unreach-call.i 901    896     3600 9710   274    128     2320 2660   905    885     4380 9290   898     895     701   7810    901     901     332   10800    901      901      491   2350     1.46   1.54   84.1  18.5   901    805    3700 10800   901    898     1530 9210   903    887     4590 5880   901    897     2340 8650   901    894     696 9510  
reducercommutativity/avg40_true-unreach-call.i 109    72.8   3070 1030   133    60.2   1870 1210   906    879     5890 9160   895     895     269   7770    901     901     389   11600    901      901      663   8500     1.88   1.90   129    19.9   175    115    4600 2050   58.4  54.7   1890 620   904    884     5260 10500   159    151     701 1980   901    893     817 10200  
reducercommutativity/avg60_true-unreach-call.i 558    507     4670 7460   961    495     3290 8450   905    871     4670 11600   895     895     271   7850    901     901     473   10900    901      901      663   11200     2.80   2.81   200    35.4   275    193    4860 3680   130    126     3260 1380   905    881     3860 11100   357    347     918 3980   901    892     963 9800  
reducercommutativity/avg_true-unreach-call.i 901    778     5310 10500   95.4  27.1   2540 755   903    580     4370 7220   895     895     182   10500    901     901     411   11000    901      901      305   9470     881      880      145    11900     900    848    769 13400   902    895     1930 7150   902    439     3710 7940   901    893     592 10600   901    897     463 6030  
reducercommutativity/max05_true-unreach-call_true-termination.i 10.3  3.54  469 80.3 82.4  34.7   1480 805   912    905     1530 11500   901     894     1590   9540    6.50  6.50  25.6 11.9  5.41   5.40   34.1 72.0   1.33   1.38   65.7  15.7   900    845    1250 11100   9.40 7.82  335 101   63.9  53.9   1380 755   912    909     1100 11200   912    907     1230 12100  
reducercommutativity/max10_true-unreach-call_true-termination.i 498    488     1010 6100   56.3  22.4   1150 461   902    882     2610 8120   901     882     2530   9530    44.0   44.0   57.7 519    237      237      90.4 2950     1.55   1.58   80.3  20.5   901    821    2210 11200   901    899     1170 9120   901    887     2570 8450   902    899     2620 7550   902    896     3030 6470  
reducercommutativity/max20_true-unreach-call.i 901    887     1180 13100   905    441     3010 7320   904    879     2790 8290   895     895     185   12200    849     850     134   11500    901      901      327   12500     3.63   3.64   102    43.9   901    748    5290 12600   902    898     1750 9280   902    885     4830 8810   902    896     5030 7070   902    891     5160 9780  
reducercommutativity/max40_true-unreach-call.i 219    176     3330 2260   914    448     3680 9560   903    872     2480 9080   895     895     235   9450    901     901     217   11200    901      901      576   8770     25.7    25.7    184    202     901    741    4770 11900   902    898     1780 10200   902    878     1960 9770   235    227     894 2310   901    882     8050 9730  
reducercommutativity/max60_true-unreach-call.i 783    720     4810 8190   915    448     2170 9940   904    858     4000 9610   895     895     249   8190    901     901     277   11900    901      901      631   10800     178      178      323    1150     900    738    5000 11900   902    898     1550 8020   902    865     3150 12200   609    599     1340 5400   901    883     9220 12000  
reducercommutativity/max_true-unreach-call.i 526    477     3930 5420   40.8  8.69  1420 267   121    113     2240 1310   895     895     256   10900    901     901     446   12000    901      901      113   1840     881      880      391    9180     901    845    2170 9970   902    890     2670 5590   902    436     5680 6800   901    893     727 12300   26.4  23.5   580 250  
reducercommutativity/sep05_true-unreach-call.i 44.2  19.0   1440 382   57.1  15.4   2130 444   839    788     1550 10500   846     793     1410   11100    .614 .613 23.4 7.44 .797  .792  35.7 9.98  1.31   1.33   67.0  16.2   901    784    4820 13500   5.05 3.44  325 51.1 937    884     2540 12200   9.46 7.08  307 119   901    894     649 10600  
reducercommutativity/sep10_true-unreach-call.i 37.9  19.2   958 346   903    290     4810 7290   902    532     4840 8340   902     537     4810   8400    .602 .601 23.3 8.14 10.8    10.8    102   139     2.15   2.19   74.3  28.1   906    677    8690 9240   23.4  21.4   467 218   960    574     5080 9110   168    164     594 1910   901    891     810 12600  
reducercommutativity/sep20_true-unreach-call.i 900    858     4060 12400   914    300     5040 7860   902    595     3700 8770   895     895     186   12100    .647 .646 23.4 6.97 901      901      373   13400     881      931      99.9  12000     908    432    12700 6980   315    312     1050 1940   901    435     4170 11000   902    896     1690 4030   901    890     2580 8060  
reducercommutativity/sep40_true-unreach-call.i 602    337     7320 4640   221    66.0   3020 1980   903    596     3900 8550   895     895     186   10100    .688 .686 29.0 9.29 901      901      516   2590     881      930      161    10600     901    623    9500 10500   902    898     1800 7040   902    437     3020 8230   249    239     853 2900   901    884     5440 12400  
reducercommutativity/sep60_true-unreach-call.i 901    513     8890 7320   913    301     3530 8590   903    594     4270 9140   895     895     193   11000    .737 .736 35.2 8.79 901      901      877   11100     881      931      246    8760     901    745    6030 12700   902    898     2570 10800   902    435     2990 8850   657    647     1130 8120   901    884     6720 10900  
reducercommutativity/sep_true-unreach-call.i 901    761     5800 10100   957    347     5320 9690   902    603     2690 9630   895     895     193   8370    901     901     451   10000    901      901      386   12000     881      880      178    11300     900    782    5110 11300   905    892     2170 8040   902    434     5080 6970   901    895     442 10800   901    896     511 10900  
reducercommutativity/sum05_true-unreach-call_true-termination.i 901    898     1180 9660   15.7  4.13  612 123   901    890     3830 13200   901     889     3940   10900    .162 .161 23.3 1.98 1.38   1.36   30.7 2.72  1.27   1.32   70.0  17.6   25.8  11.3  846 230   901    899     724 10500   901    891     2560 9870   901    899     1420 11800   912    908     9390 9980  
reducercommutativity/sum10_true-unreach-call.i 901    897     1680 10700   905    445     3050 8300   902    886     1960 10400   901     885     2420   10800    .204 .204 23.5 1.93 3.96   3.95   74.4 51.2   1.28   1.34   70.4  23.4   76.7  42.3  1450 745   901    898     1200 11000   901    888     2670 10100   901    898     1650 9810   901    894     1720 9810  
reducercommutativity/sum20_true-unreach-call.i 901    897     2610 10700   914    446     2890 9290   907    882     6620 8570   895     895     239   7900    .189 .188 23.4 2.78 244      244      315   2230     1.41   1.37   82.3  15.9   901    818    4790 6600   901    899     1350 11400   903    884     6670 7720   901    897     2150 8880   901    892     3460 12500  
reducercommutativity/sum40_true-unreach-call.i 87.9  55.7   2940 870   961    495     7580 9580   905    873     7420 10800   895     895     271   7470    .230 .229 23.4 2.99 901      901      495   8110     1.83   1.79   123    22.9   900    760    4600 12000   45.9  42.3   1760 446   903    878     4960 8430   127    119     791 1350   901    886     7050 12400  
reducercommutativity/sum60_true-unreach-call.i 239    193     4630 2410   915    449     2890 8560   906    865     6490 10500   894     895     198   8690    .281 .280 23.5 3.11 901      901      498   6840     2.78   2.80   200    33.2   902    737    6410 8160   91.7  87.3   3190 901   903    869     4270 12600   308    298     939 3660   901    884     8370 10800  
reducercommutativity/sum_true-unreach-call.i 163    140     3610 2170   46.8  9.78  1470 297   904    576     4310 9150   895     895     236   9960    901     901     529   12300    901      901      203   11300     881      880      385    11000     901    850    4740 6300   903    893     3570 9730   902    436     5000 7010   901    892     579 10100   901    893     1160 9490  
bitvector/byte_add_false-unreach-call_true-no-overflow.i 12.6  3.56  533 94.9 8.59 1.86  482 52.8 75.9  64.6   1690 1040   2.17  2.16  106   28.4  50.6   50.6   2200   623    .153  .152  24.1 1.71  4.74   4.64   135    58.9   55.2  24.5  755 545   3.01 1.27  277 26.3 7.87 1.98  462 56.3 3.19 1.36  270 28.0 13.5  9.81  426 147  
bitvector/sum02_false-unreach-call_true-no-overflow.i 3.53 1.47  297 30.0 70.7  18.3   2830 574   903    533     3970 7550   69.4   68.9   75.6 839    2.24  2.24  147   23.8  246      245      15000   3410     882      882      450    11000     901    896    341 10600   870    861     15000 8870   903    440     5370 8000   901    897     469 10900   901    875     3190 8910  
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 10.3  3.16  466 82.2 14.4  2.89  586 87.4 69.7  59.7   1710 774   73.6   64.3   1760   870    41.5   41.5   2220   536    .428  .422  27.6 5.16  12.1    12.0    149    133     900    800    4130 10800   2.98 1.28  267 26.7 11.1  2.51  559 85.9 4.42 2.32  274 43.4 8.70 4.72  421 74.8
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 14.6  4.08  544 104   15.5  3.07  642 111   24.7  15.8   921 264   27.7   19.5   844   304    41.7   41.7   2220   527    .467  .461  28.1 5.97  15.0    14.9    145    178     577    506    1400 6820   3.05 1.29  261 27.1 11.5  2.65  566 83.8 4.47 2.36  280 43.4 10.0  6.06  436 92.1
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 8.26 6.12  309 94.6 9.47 3.63  333 79.6 6.51 4.70  284 86.6 488     486     282   6010    118     118     1200   1250    .463  .462  25.5 5.67  1.67   1.77   76.9  20.3   901    893    528 10700   4.26 3.00  240 50.0 5.43 3.12  299 55.5 45.4  43.4   536 515   5.83 4.52  243 61.8
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 3.64 1.43  290 31.2 243    120     656 1540   7.13 5.16  284 76.9 239     236     289   2440    361     361     1320   3770    190      190      197   2150     857      857      300    13000     901    890    727 11300   123    121     361 1290   108    105     500 1000   428    426     364 4770   6.55 5.00  283 83.3
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 4.77 2.99  296 49.8 221    109     626 1450   153    151     312 2050   457     455     320   5020    230     230     1380   2530    252      252      198   3050     881      931      189    11000     901    891    559 10700   116    115     364 1030   104    101     488 1200   684    682     388 7260   153    151     316 1700  
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 2.91 1.29  273 29.9 2.89 1.01  273 24.9 2.27 .973 243 20.1 485     484     262   6380    .164 .163 23.3 1.44 .159  .156  29.8 1.63  1.49   1.57   69.6  18.0   901    884    669 11000   2.31 1.00  217 20.0 4.97 1.38  351 36.2 4.20 2.80  244 51.7 4.39 2.48  306 44.3
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 5.56 2.15  347 47.2 9.37 2.50  454 78.6 6.94 2.84  399 57.6 16.6   12.4   411   207    .156 .155 23.4 1.99 .686  .675  74.2 8.71  1.28   1.34   67.7  17.7   117    98.1  1730 1210   2.43 1.02  230 22.2 5.50 2.07  352 42.6 3.57 1.96  264 36.5 5.55 2.46  332 49.1
bitvector/jain_1_true-unreach-call_true-no-overflow.i 2.86 1.25  268 27.2 4.27 1.24  307 29.2 2.77 1.18  269 28.4 299     298     289   3440    5.26  5.26  507   70.0  280      279      15000   3310     889      880      238    11400     6.74 2.02 340 54.6 509    502     15000 5390   603    595     15000 7230   2.04 .935 232 17.6 2.14 .946 233 20.7
bitvector/jain_2_true-unreach-call_true-no-overflow.i 2.83 1.25  269 26.7 4.30 1.25  298 30.8 2.72 1.18  264 25.9 895     895     292   7750    6.81  6.81  728   90.9  901      901      4650   7070     885      880      252    8550     7.25 2.01 343 55.6 277    272     15000 2620   475    467     15000 4330   2.16 .944 229 18.5 2.31 1.05  233 23.3
bitvector/jain_4_true-unreach-call_true-no-overflow.i 2.93 1.29  275 28.9 5.00 1.34  320 32.0 2.80 1.21  273 24.5 895     895     244   6990    8.64  8.64  892   107    901      901      3140   7580     885      880      263    9340     5.74 1.92 326 49.2 238    234     15000 2180   419    411     15000 3770   2.13 .969 230 21.4 2.41 1.05  237 20.0
bitvector/jain_5_true-unreach-call_true-no-overflow.i 900    863     3870 12300   912    303     7480 8500   904    606     7170 8940   59.0   58.4   75.2 684    .246 .246 40.2 3.33 136      134      15000   1440     885      880      204    8860     901    758    2230 12800   902    887     667 9480   904    442     6940 7950   901    898     387 9870   901    879     5440 11900  
bitvector/jain_6_true-unreach-call_true-no-overflow.i 2.91 1.27  274 25.3 4.61 1.31  300 36.3 2.88 1.24  266 24.0 895     895     268   8430    8.82  8.82  894   96.1  901      901      5690   7610     884      880      274    7890     5.95 1.99 326 48.1 241    236     15000 2660   426    418     15000 3650   2.17 .984 224 20.2 2.38 1.01  238 20.3
bitvector/jain_7_true-unreach-call_true-no-overflow.i 2.96 1.28  270 28.3 8.78 3.03  404 72.8 4.41 2.78  271 48.4 895     895     292   6690    8.20  8.21  763   87.6  901      900      7450   8250     885      880      293    8720     5.89 2.00 322 49.6 544    538     15000 6370   647    638     15000 5730   6.49 5.32  232 71.6 3.86 2.55  243 41.4
bitvector/modulus_true-unreach-call_true-no-overflow.i 20.8  19.1   312 244   20.5  5.41  1460 160   228    212     1670 3070   895     895     383   7460    901     901     5580   8660    .430  .428  25.5 5.36  342      342      264    2150     28.9  24.9  329 420   209    201     930 1980   25.2  10.0   1980 259   6.66 5.44  244 70.1 901    899     465 12200  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 3.17 1.32  290 31.5 2.90 1.05  268 24.8 2.34 .976 244 20.0 7.00  5.49  262   76.9  .162 .161 23.2 1.79 .138  .132  23.2 1.66  1.20   1.28   68.0  16.3   267    250    2300 3800   2.36 .987 229 20.6 4.50 1.25  311 32.6 2.36 1.12  220 24.6 3.22 1.36  288 27.8
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 13.8  9.92  494 134   5.71 1.43  337 39.4 17.2  10.7   536 156   22.3   15.2   602   226    .176 .175 23.2 2.03 .207  .201  23.2 2.13  1.25   1.28   65.3  15.7   901    861    882 10800   2.44 1.05  224 25.2 4.29 1.24  318 27.6 5.78 4.10  241 59.7 13.1  10.0   445 123  
bitvector/parity_true-unreach-call_true-no-overflow.i 3.03 1.28  280 28.9 25.0  9.49  650 206   117    111     730 1590   895     895     148   10000    2.26  2.26  160   24.9  901      901      204   2560     881      880      281    11600     900    884    1020 11400   8.79 6.88  280 109   12.4  8.30  333 125   15.9  13.8   277 197   117    112     546 1700  
bitvector/sum02_true-unreach-call_true-no-overflow.i 3.29 1.41  302 32.1 140    39.9   3750 1180   904    533     6320 9820   171     171     487   1820    2.60  2.59  151   33.8  289      289      15000   2570     880      880      329    10900     901    894    512 11500   879    870     15000 10500   904    441     6500 6600   901    898     466 10900   901    877     3110 7890  
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 18.3  4.77  740 137   47.2  9.55  1690 295   8.34 2.53  438 62.5 32.7   32.6   102   470    310     310     15000   3900    8.54   8.54   408   118     16.2    15.8    215    170     24.2  6.88 573 200   5.73 2.43  331 41.4 22.7  4.82  756 156   5.61 2.55  319 46.8 7.11 3.47  339 78.4
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 23.4  6.26  1020 173   69.5  16.8   2970 487   10.9  3.80  513 100   56.2   56.2   112   830    895     895     14800   11800    16.5    16.4    678   244     37.7    37.0    243    418     28.4  7.75 717 221   6.58 2.90  336 67.0 28.5  6.20  1340 195   6.02 2.90  309 56.7 15.4  10.1   477 170  
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 8.83 2.56  464 64.0 24.6  4.57  922 157   6.74 1.98  329 52.6 17.8   17.8   85.0 206    895     895     14900   8230    3.47   3.47   193   46.5   9.12   8.85   185    101     22.2  6.42 558 167   4.33 1.70  293 36.9 15.2  3.35  619 103   4.08 1.75  283 40.4 5.06 1.96  306 47.0
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 18.0  4.71  742 130   57.2  12.4   1830 354   21.5  14.4   1550 218   174     166     1290   2100    335     334     15000   3600    59.5    59.5    1910   781     154      153      378    1430     35.0  9.81 842 278   12.9  8.92  512 145   32.3  8.37  1200 245   901    889     5190 10300   901    894     685 13100  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 38.6  9.92  1590 260   35.9  6.78  1250 236   19.4  13.2   1490 213   143     136     1560   1760    895     895     15000   7090    43.1    43.1    1620   591     116      115      336    1020     42.3  12.5  1070 360   9.17 5.21  403 96.2 18.2  3.98  648 126   901    893     5460 9780   30.5  24.7   492 444  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 21.1  5.52  892 159   28.3  5.44  975 182   21.9  14.8   2150 211   145     139     2150   1800    896     896     14900   7510    44.9    44.9    1580   488     128      127      358    1200     25.1  6.41 1060 188   9.48 5.58  413 83.5 17.6  3.81  688 116   901    894     4140 10200   901    892     717 11800  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 900    698     6420 11000   905    292     3550 4560   907    550     4190 10500   895     895     387   9860    901     901     2820   8480    901      901      1810   10300     882      880      581    6850     900    870    2410 13500   904    896     5250 6370   902    433     3240 8870   901    893     3060 10600   901    897     485 10400  
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 55.6  14.7   2340 343   130    36.1   3770 1050   26.9  19.1   2290 270   45.8   38.2   2290   517    407     407     15000   4440    901      901      14800   10500     882      880      633    6110     46.9  17.1  1880 457   904    896     3650 7310   13.0  2.96  632 85.4 901    893     5870 13200   12.6  5.43  500 117  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 26.4  6.94  966 184   39.3  7.53  1340 251   94.2  84.4   2320 1230   895     895     372   11200    423     423     15000   4470    901      901      9660   11400     882      880      537    6380     38.5  12.0  1470 336   903    894     2990 9080   100    40.6   3150 877   901    883     6770 9660   110    102     759 1470  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c 25.3  6.46  969 198   160    45.7   4410 1380   93.0  83.7   2310 1140   895     895     376   11100    447     446     15000   4800    901      901      10000   11800     883      880      637    6790     38.2  11.9  1620 294   903    895     2920 6810   104    40.9   3400 1030   901    881     7040 9920   901    891     972 12100  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 45.9  12.2   2230 347   186    54.6   4870 1630   25.2  18.5   2290 248   895     895     305   12700    426     426     15000   5120    901      901      12400   9940     883      880      705    6210     36.2  10.8  1410 304   904    896     5230 6000   904    436     5950 6870   901    893     5140 9010   21.5  14.3   564 217  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 40.2  11.8   2220 320   909    292     5730 7090   26.0  19.2   2280 265   895     895     303   11700    405     405     15000   4290    901      901      12400   10400     883      880      716    6360     36.0  10.7  1490 309   904    896     5210 5820   903    435     5720 6850   902    893     5090 12200   17.6  10.5   549 175  
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c 4.05 1.60  298 36.4 87.2  39.7   2260 753   11.4  5.93  389 115   14.9   8.91  402   138    895     896     2900   11900    1.03   1.02   26.4 15.3   1.65   1.64   82.8  19.9   160    133    887 1890   155    134     3440 1570   920    854     5210 10400   902    893     686 10400   9.91 6.64  311 120  
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c 13.1  3.93  497 95.6 13.4  3.64  612 99.7 115    99.7   1250 1500   115     100     1210   1300    895     895     2900   12100    .109  .108  24.3 1.20  1.49   1.54   86.8  19.6   217    203    999 2530   125    102     3480 1330   8.00 1.92  445 58.1 26.1  15.4   491 272   110    97.4   1010 1360  
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c 7.66 2.49  447 58.7 35.5  7.65  1090 274   102    87.3   1280 1450   121     108     1430   1450    894     895     2900   10800    6.95   6.91   215   88.1   11.0    10.8    116    139     901    867    1570 10300   157    137     3370 1330   902    852     3970 11100   151    142     771 1770   106    95.0   974 1340  
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c 3.55 1.45  287 34.6 384    176     2530 3820   202    197     372 2490   225     221     364   2570    894     895     2900   13100    18.7    18.7    38.3 244     16.4    16.4    95.1  205     511    472    1040 5420   904    893     1090 11000   213    180     2290 2700   909    905     907 11200   85.2  82.6   488 1090  
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c 22.1  5.78  720 170   8.39 1.89  433 59.3 113    98.4   1330 1220   114     99.4   1200   1500    895     895     2900   11900    .133  .134  24.3 .967 1.49   1.53   85.7  22.4   15.0  4.40 613 108   131    105     3480 1230   7.72 1.91  413 55.3 21.6  13.9   491 206   109    97.6   1090 1520  
bitvector-regression/implicitfloatconversion_false-unreach-call.c 3.08 1.26  276 28.3 3.39 1.07  286 31.0 2.30 1.00  253 20.7 .376 .373 48.3 3.79 .129 .128 23.0 1.29 .0795 .0798 23.0 .654 1.48   1.47   71.0  15.9   9.07 2.99 317 68.6 2.11 .921 225 20.8 3.05 1.13  267 26.9 2.02 .914 216 18.1 2.07 .936 207 19.9
bitvector-regression/implicitunsignedconversion_false-unreach-call.c 2.56 1.09  266 22.2 3.12 1.10  280 26.4 2.51 1.00  269 19.7 .372 .370 48.3 3.86 .139 .139 23.0 1.41 .107  .107  23.1 .737 1.45   1.50   72.8  22.2   5.43 1.75 324 44.6 2.02 .915 218 19.4 3.12 1.18  268 24.8 2.15 .926 226 20.1 2.13 .961 221 19.1
bitvector-regression/integerpromotion_false-unreach-call.c 2.82 1.24  273 24.5 3.11 1.06  275 26.7 2.54 1.02  262 21.1 .347 .344 48.2 4.14 .132 .134 23.6 1.45 .106  .106  23.0 .657 1.51   1.57   69.4  17.5   8.87 2.98 318 74.3 2.06 .923 217 18.5 3.00 1.17  267 26.8 1.97 .883 212 18.8 2.11 .941 226 19.7
bitvector-regression/recHanoi03_false-unreach-call.c 3.02 1.27  281 26.2 3.06 1.05  292 22.1 3.16 1.28  299 25.4 4.58  2.48  301   48.7  4.11  4.02  298   51.0  2.38   2.35   120   30.4   8.58   8.45   78.2  127     87.0  62.3  878 1180   2.12 .916 226 19.9 2.72 1.01  257 22.1 1.95 .867 217 17.4 2.21 .956 225 15.6
bitvector-regression/signextension2_false-unreach-call.c 2.56 1.14  265 21.5 3.34 1.10  280 27.9 2.46 1.08  245 24.8 480     480     70.2 6220    .134 .133 23.4 1.47 .100  .0996 23.2 .715 1.49   1.55   72.3  19.4   5.84 1.87 318 42.8 2.10 .952 224 19.6 3.17 1.16  271 28.1 2.03 .922 218 18.8 2.22 .991 224 21.0
bitvector-regression/signextension_false-unreach-call.c 2.53 1.15  267 21.1 3.31 1.11  272 25.7 2.37 1.01  250 19.9 .369 .368 48.4 4.14 .151 .151 23.2 1.35 .0984 .0980 23.2 .826 1.49   1.54   70.0  18.0   6.75 1.88 328 50.9 2.17 .952 220 19.2 3.26 1.17  267 25.4 2.02 .905 213 18.3 2.06 .938 223 19.3
bitvector-regression/implicitunsignedconversion_true-unreach-call.c 2.59 1.14  263 25.1 2.68 .953 270 21.0 2.12 .920 220 19.1 3.17  1.66  261   29.2  .171 .170 23.2 1.29 .104  .104  23.2 .630 1.16   1.21   74.6  16.6   5.61 1.87 330 43.9 2.14 .920 222 17.8 2.36 .916 259 20.2 1.94 .872 211 16.6 2.11 .957 223 18.0
bitvector-regression/integerpromotion_true-unreach-call.c 2.59 1.14  269 20.0 2.72 .977 266 25.9 2.32 .946 248 19.9 3.18  1.67  258   27.5  .151 .150 23.1 1.39 .106  .106  23.0 .583 1.15   1.24   68.1  14.9   9.00 3.08 313 75.1 2.21 .944 223 18.5 2.28 .905 261 20.7 2.22 .974 218 18.9 2.09 .923 226 19.1
bitvector-regression/signextension2_true-unreach-call.c 2.62 1.16  271 26.4 2.67 .974 259 22.5 2.19 .946 241 18.9 483     482     274   5790    .150 .149 23.2 1.37 .0720 .0725 23.1 .736 1.19   1.28   72.1  14.6   5.71 1.85 323 49.1 2.08 .910 221 19.8 2.57 .998 257 24.7 2.05 .920 215 20.6 2.10 .913 208 18.9
bitvector-regression/signextension_true-unreach-call.c 2.69 1.16  263 21.0 2.80 1.03  270 23.2 2.22 .956 242 18.8 3.06  1.67  264   29.1  .160 .159 23.3 1.52 .105  .105  23.1 .765 1.19   1.29   80.7  12.8   6.11 1.90 329 42.9 2.23 .955 227 19.1 2.49 .975 255 20.1 2.16 .920 218 19.3 2.15 .953 207 19.7
bitvector-loops/diamond_false-unreach-call2.i 13.4  3.68  578 106   6.33 1.67  372 42.4 2.99 1.20  258 26.2 1.19  1.18  77.8 16.8  16.3   16.3   1010   193    .0864 .0863 23.3 .968 1.87   1.82   93.2  29.2   8.12 2.66 373 61.2 2.67 1.15  268 24.8 6.26 1.59  380 40.4 2.20 .997 221 20.1 2.50 1.07  279 22.9
bitvector-loops/overflow_false-unreach-call1.i 3.03 1.30  269 27.6 908    297     7090 7530   906    609     7830 9650   54.2   53.8   75.4 778    .150 .148 23.0 1.46 204      201      15000   2160     882      931      934    12300     901    754    1470 14700   902    878     783 12700   909    447     10800 8810   901    898     388 11200   901    881     6020 10400  
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 3.23 1.35  287 28.9 13.0  3.15  505 90.6 212    204     893 2510   7.87  7.83  104   96.6  2.08  2.08  224   24.2  1.08   1.07   58.7 13.4   4.65   4.54   109    61.5   163    147    737 2040   3.43 1.45  290 28.0 12.8  5.73  533 114   4.98 3.14  297 50.4 901    897     794 12200  
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 11.9  3.21  535 94.1 16.5  3.50  733 120   8.01 2.24  338 62.7 3.27  3.27  87.9 39.9  1.03  1.03  55.8 10.8  .489  .491  49.6 6.06  4.32   4.13   121    65.8   55.1  15.4  1110 442   7.11 2.16  364 56.1 22.3  4.70  941 157   6.64 3.19  330 71.8 8.60 4.52  361 85.0
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 16.4  4.55  736 126   35.8  6.96  1260 228   8.38 2.31  359 67.3 1.60  1.60  94.7 19.1  .441 .441 38.2 5.31 .797  .794  27.9 1.88  4.04   3.79   108    47.2   31.2  7.96 917 263   4.93 1.67  306 39.4 17.3  3.75  839 125   4.57 2.18  296 42.9 5.42 2.79  314 50.9
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 19.3  5.31  722 152   963    310     4630 9130   9.32 2.61  368 76.4 2.31  2.31  100   26.4  .692 .691 47.8 8.51 .343  .343  32.3 4.04  8.69   8.40   121    115     45.9  11.6  1020 332   6.02 1.93  331 54.7 21.6  4.56  926 160   5.44 2.83  318 47.8 6.55 3.53  327 67.1
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 9.72 2.77  513 73.9 10.4  2.27  490 76.4 5.41 1.66  298 40.0 1.20  1.20  63.6 13.9  .316 .315 27.3 4.20 .194  .193  27.0 1.71  3.34   3.25   95.6  44.3   17.0  4.35 531 130   3.95 1.48  283 31.1 8.83 2.21  460 61.9 3.55 1.53  277 35.4 4.21 1.77  301 37.3
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 25.0  8.08  1400 191   14.1  3.08  608 102   7.31 2.09  330 62.4 17.6   12.4   345   201    1.56  1.56  144   18.6  1.08   1.08   142   11.9   30.8    30.4    144    382     94.6  41.4  2010 820   6.69 2.17  346 49.2 9.81 2.30  515 68.1 6.47 3.19  332 54.5 8.92 5.25  364 85.7
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 18.7  5.00  731 137   49.7  9.34  1670 304   100    89.8   1270 1280   139     139     104   1680    1.41  1.41  136   17.0  .913  .911  73.7 12.5   5.85   5.68   127    77.9   63.1  24.4  1430 606   877    859     15000 9440   904    436     8010 8040   5.15 2.88  312 46.9 7.63 4.58  358 76.3
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 15.3  4.09  720 108   9.75 2.15  489 67.9 7.39 2.15  347 55.7 10.2   5.16  352   87.0  .567 .566 56.5 6.12 .330  .330  42.0 3.92  4.66   4.47   116    56.6   65.4  27.4  1560 682   4.31 1.60  287 37.9 7.26 1.82  438 50.8 4.36 2.13  289 39.0 5.64 2.84  314 52.6
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 18.3  4.84  761 134   11.1  2.47  508 72.4 8.28 2.39  359 64.0 12.8   7.11  375   125    .865 .863 77.2 9.27 .529  .529  63.8 5.90  9.47   9.21   125    139     70.2  26.9  1600 679   5.35 1.74  326 44.4 9.06 2.20  476 66.7 5.02 2.56  307 45.5 7.21 3.71  344 70.9
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 6.57 2.00  358 47.1 5.70 1.52  284 42.4 3.48 1.22  265 28.9 5.22  3.04  265   52.8  .276 .276 25.4 3.04 .169  .168  25.7 1.96  1.63   1.61   74.5  23.3   18.5  5.18 543 155   3.36 1.25  267 28.3 3.95 1.23  277 34.9 2.63 1.18  226 25.2 3.19 1.40  273 29.5
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 8.03 2.37  455 59.9 7.90 1.93  426 56.3 4.26 1.43  270 35.8 7.64  4.36  282   72.7  .360 .360 36.0 4.71 .956  .954  37.7 1.86  3.02   2.94   93.6  35.4   16.3  4.67 671 134   3.80 1.47  266 33.6 4.79 1.38  280 34.9 3.39 1.44  269 33.1 4.02 1.70  294 35.5
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 9.52