Tool CPAchecker 1.6.1-svn 22870
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS Linux 4.4.0-34-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135148 MB
Run set bmc-bitprecise.BMC k-induction-bitprecise.k-Induction predicateAnalysis-bitprecise.PredicateAbstraction impact-bitprecise.Impact
Options -heap 10000M -noout -bmc -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT -heap 10000M -noout -sv-comp16--k-induction -setprop limits.time.cpu.thread=10000s -heap 10000M -noout -predicateAnalysis-PredAbsRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -heap 10000M -noout -predicateAnalysis-ImpactRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage host k BMC formula creation (s) Bounds check (s) SMT check (s) status cputime (s) walltime (s) memUsage host k BMC formula creation (s) Invariant generation (s) Bounds check (s) SMT check (s) Induction formula creation (s) Induction check (s) status cputime (s) walltime (s) memUsage host Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) SMT without itp (s) Refinement (s) Boolean abstraction (s) Abstraction (s) Solving (s) Model enumeration (s) status cputime (s) walltime (s) memUsage host Attempted forced coverings Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) SMT without itp (s) Forced covering (s) Successful forced coverings Refinement (s) Boolean abstraction (s) Abstraction (s) Solving (s) Model enumeration (s)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i 5.22 3.02 218021888 1 .061 902    859    4136251392 1 855     825     5.35 3.08 227561472 .004 .052 .038 .00  .00  4.99 2.87 213643264 0 .004 .064 .042 .001 .00  .00 
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 5.30 3.02 219369472 1 .037 902    871    3759345664 1 867     .008 4.90 2.83 217911296 .003 .039 .028 .00  .00  5.08 2.90 204849152 0 .004 .025 .009 .001 .00  .00 
array-examples/sorting_bubblesort_false-unreach-call_ground.i 4.94 2.85 210272256 1 .040 902    872    3759636480 1 868     .014 4.84 2.83 220467200 .003 .034 .016 .00  .00  4.81 2.81 201809920 0 .004 .025 .009 .00  .00  .00 
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 5.14 2.99 214384640 1 .040 902    868    3762839552 1 864     .009 5.09 2.94 218374144 .003 .058 .031 .00  .00  4.95 2.81 205467648 0 .004 .027 .011 .001 .00  .00 
array-examples/sorting_selectionsort_false-unreach-call_ground.i 5.04 2.85 217124864 1 .034 902    867    3797401600 1 864     .008 4.81 2.75 216625152 .003 .038 .028 .00  .00  5.04 2.90 206835712 0 .003 .027 .011 .00  .00  .001
array-examples/standard_allDiff2_false-unreach-call_ground.i 5.15 3.00 211972096 1 .044 902    875    3746267136 1 871     .007 4.92 2.88 215564288 .004 .026 .014 .001 .00  5.19 2.94 208715776 0 .005 .029 .014 .00  .00  .00 
array-examples/standard_copy1_false-unreach-call_ground.i 4.64 2.67 214089728 1 .036 902    875    3735605248 1 871     .008 4.77 2.80 215719936 .003 .058 .047 .00  .00  4.69 2.71 201748480 0 .003 .027 .012 .00  .00  .00 
array-examples/standard_copy2_false-unreach-call_ground.i 5.20 3.02 218062848 1 .039 902    877    3721293824 1 873     .010 4.75 2.76 219856896 .008 .045 .016 .00  .00  4.84 2.82 205418496 0 .004 .026 .010 .001 .00  .00 
array-examples/standard_copy3_false-unreach-call_ground.i 5.10 2.97 215171072 1 .039 902    873    3738808320 1 870     859     4.82 2.74 217231360 .004 .026 .014 .00  .00  4.90 2.82 207896576 0 .003 .045 .014 .00  .00  .00 
array-examples/standard_copy4_false-unreach-call_ground.i 5.11 2.97 213622784 1 .039 902    873    3766702080 1 869     .013 4.85 2.83 220971008 .004 .052 .019 .00  .00  4.92 2.83 207417344 0 .003 .030 .013 .00  .00  .00 
array-examples/standard_copy5_false-unreach-call_ground.i 5.04 2.90 215867392 1 .037 902    873    3768774656 1 869     857     5.11 2.96 217288704 .003 .030 .016 .00  .00  4.94 2.83 203608064 0 .004 .029 .011 .001 .00  .00 
array-examples/standard_copy6_false-unreach-call_ground.i 5.25 3.03 218980352 1 .035 902    873    3775508480 1 870     .005 5.04 2.92 219791360 .003 .038 .023 .00  .00  4.78 2.70 206639104 0 .004 .031 .009 .00  .00  .00 
array-examples/standard_copy7_false-unreach-call_ground.i 4.73 2.78 212377600 1 .037 902    875    3769225216 1 871     .012 4.93 2.89 221814784 .004 .054 .031 .001 .00  4.76 2.75 206053376 0 .004 .027 .011 .00  .00  .00 
array-examples/standard_copy8_false-unreach-call_ground.i 5.31 3.06 216215552 1 .037 902    874    3754250240 1 871     .010 4.93 2.89 218189824 .003 .038 .020 .00  .00  5.05 2.91 205590528 0 .003 .027 .010 .00  .00  .00 
array-examples/standard_copy9_false-unreach-call_ground.i 5.32 3.05 217374720 1 .038 902    874    3795988480 1 871     858     5.10 2.96 221679616 .011 .050 .030 .00  .00  5.00 2.88 207470592 0 .004 .025 .009 .00  .00  .001
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 5.21 2.95 213598208 1 .041 902    876    3729698816 1 872     .008 5.07 2.95 217792512 .004 .036 .025 .00  .00  4.83 2.80 202145792 0 .004 .047 .012 .00  .00  .00 
array-examples/standard_init1_false-unreach-call_ground.i 5.27 3.04 211656704 1 .039 902    877    3700277248 1 873     .007 5.18 3.01 217350144 .004 .046 .033 .00  .00  4.88 2.83 207519744 0 .004 .032 .012 .00  .00  .00 
array-examples/standard_init2_false-unreach-call_ground.i 4.88 2.79 215867392 1 .036 902    877    3716550656 1 873     863     4.93 2.81 219447296 .004 .033 .014 .00  .00  4.83 2.79 208125952 0 .004 .028 .011 .00  .00  .00 
array-examples/standard_init3_false-unreach-call_ground.i 4.67 2.73 215699456 1 .040 901    875    3722661888 1 872     .005 5.07 2.94 214204416 .004 .064 .029 .00  .00  4.94 2.85 203636736 0 .004 .027 .014 .001 .00  .00 
array-examples/standard_init4_false-unreach-call_ground.i 5.13 2.98 214757376 1 .037 902    878    3711168512 1 874     .006 5.08 2.95 215658496 .013 .063 .036 .00  .00  4.95 2.87 212766720 0 .004 .028 .010 .00  .00  .00 
array-examples/standard_init5_false-unreach-call_ground.i 5.02 2.94 213245952 1 .043 902    878    3714928640 1 874     .011 5.27 3.03 219037696 .004 .053 .031 .00  .00  5.10 2.92 207351808 0 .004 .027 .010 .001 .00  .001
array-examples/standard_init6_false-unreach-call_ground.i 4.96 2.89 215482368 1 .045 902    877    3731673088 1 873     863     4.77 2.81 216195072 .004 .036 .024 .001 .00  5.14 2.91 208199680 0 .004 .026 .010 .00  .00  .001
array-examples/standard_init7_false-unreach-call_ground.i 5.43 3.11 218693632 1 .038 902    876    3735662592 1 873     862     5.02 2.95 218845184 .015 .045 .022 .00  .00  4.95 2.84 206393344 0 .005 .027 .011 .00  .00  .00 
array-examples/standard_init8_false-unreach-call_ground.i 4.95 2.89 219168768 1 .036 902    877    3745124352 1 873     862     5.10 2.94 219865088 .005 .052 .025 .00  .00  4.92 2.83 210546688 0 .003 .027 .010 .00  .00  .00 
array-examples/standard_init9_false-unreach-call_ground.i 5.26 3.07 216018944 1 .041 902    877    3733032960 1 873     .009 4.83 2.78 216457216 .004 .026 .014 .00  .00  5.06 2.95 207527936 0 .003 .027 .012 .00  .00  .00 
array-examples/standard_minInArray_false-unreach-call_ground.i 5.08 2.96 215969792 1 .041 902    874    3723948032 1 870     .012 5.00 2.88 219602944 .003 .046 .022 .00  .00  4.77 2.72 203853824 0 .003 .028 .013 .00  .00  .00 
array-examples/standard_partition_false-unreach-call_ground.i 5.24 3.03 214765568 1 .038 902    872    3746398208 1 868     854     5.20 3.02 221937664 .004 .052 .032 .00  .00  5.06 2.90 205811712 0 .003 .027 .012 .00  .00  .00 
array-examples/standard_running_false-unreach-call.i 5.10 2.98 214552576 1 .038 902    872    3730436096 1 868     856     4.77 2.80 220745728 .004 .066 .023 .00  .00  4.86 2.81 206954496 0 .003 .027 .011 .00  .00  .00 
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground.i 5.30 2.99 216752128 1 .060 7.34 4.05 322359296 1 .157 .005 5.47 3.12 217296896 .004 .071 .052 .00  .00  4.96 2.87 207998976 0 .004 .084 .059 .001 .00  .00 
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 5.07 2.94 218234880 1 .060 902    860    3915927552 1 856     829     5.17 2.96 219262976 .004 .065 .041 .00  .00  5.30 3.03 211263488 0 .005 .054 .032 .001 .00  .00 
array-examples/relax_true-unreach-call.i 911    892    1214275584 19 8.53  19.1   857     903    452    3745599488 14 7.87  425     18.7   365     11.1   41.5   9.76 5.46 360288256 .742 1.37  .302 .681 .397 .775 .430 .668 .258 .139 902    894    628600832 301 .397 884     .791 .335 3.08  882     0 6.92  .226 .316 .212 .004
array-examples/sanfoundry_02_true-unreach-call_ground.i 5.05 2.94 218521600 1 .039 902    870    3767492608 1 866     .006 5.17 3.01 218304512 .005 .035 .014 .00  .00  4.78 2.78 203210752 0 .004 .028 .012 .001 .00  .001
array-examples/sanfoundry_10_true-unreach-call_ground.i 907    879    5360906240 26 63.3   586     214     955    488    5075185664 19 33.9   420     147     87.0   43.0   165     902    881    1836937216 857     863     1.70  857     814     15.5   826     857     86.3   728     902    894    683421696 1000 .131 891     .596 .080 .236 890     37 .644 .031 .063 .025 .001
array-examples/sanfoundry_24_true-unreach-call.i 4.98 2.90 212598784 1 .040 902    859    3865178112 1 855     .008 5.41 3.07 219910144 .009 .047 .032 .001 .00  5.02 2.88 202457088 0 .003 .027 .010 .00  .00  .00 
array-examples/sanfoundry_27_true-unreach-call_ground.i 5.02 2.94 216481792 1 .039 902    873    3727785984 1 869     .006 5.08 2.93 220098560 .004 .042 .029 .00  .00  4.93 2.84 206753792 0 .005 .036 .017 .00  .00  .00 
array-examples/sanfoundry_43_true-unreach-call_ground.i 4.80 2.81 214097920 1 6.20 3.46 320966656 1 .435 5.06 2.93 220704768 .011 .095 .051 .004 .00  .00  .00  .00  5.01 2.88 205840384 0 .011 .114 .075 .003 .00  .00  .002 .00  .00 
array-examples/sorting_bubblesort_true-unreach-call_ground.i 5.37 3.05 218087424 1 .036 902    871    3742572544 1 867     .006 5.09 2.93 215379968 .004 .054 .026 .00  .00  4.86 2.81 201465856 0 .004 .027 .013 .00  .00  .00 
array-examples/sorting_selectionsort_true-unreach-call_ground.i 5.15 3.00 213880832 1 .038 902    866    3781361664 1 862     843     5.00 2.90 217907200 .004 .045 .015 .00  .00  4.71 2.74 207769600 0 .004 .025 .012 .001 .00  .00 
array-examples/standard_compareModified_true-unreach-call_ground.i 4.76 2.79 221921280 1 .037 902    872    3766927360 1 868     855     4.77 2.78 221679616 .010 .036 .017 .00  .00  4.60 2.62 200785920 0 .003 .022 .010 .00  .00  .00 
array-examples/standard_compare_true-unreach-call_ground.i 4.96 2.90 214097920 1 .041 902    871    3747037184 1 867     .005 5.03 2.92 217661440 .020 .064 .036 .00  .00  4.81 2.80 204681216 0 .004 .028 .011 .00  .00  .00 
array-examples/standard_copy1_true-unreach-call_ground.i 5.02 2.93 212602880 1 .036 902    876    3705298944 1 872     .004 4.61 2.69 216698880 .009 .060 .023 .00  .00  4.68 2.71 204476416 0 .008 .032 .012 .00  .00  .002
array-examples/standard_copy2_true-unreach-call_ground.i 5.19 3.03 215470080 1 .042 902    875    3722223616 1 872     .009 4.87 2.82 214134784 .003 .032 .021 .00  .00  4.86 2.82 207122432 0 .004 .037 .018 .00  .00  .00 
array-examples/standard_copy3_true-unreach-call_ground.i 4.90 2.86 211791872 1 .036 902    875    3741032448 1 871     860     5.07 2.95 216883200 .004 .026 .015 .001 .00  4.88 2.75 202850304 0 .003 .044 .022 .00  .00  .00 
array-examples/standard_copy4_true-unreach-call_ground.i 5.21 3.01 223961088 1 .038 902    872    3748016128 1 869     .005 5.10 2.97 216256512 .003 .059 .026 .00  .00  4.72 2.72 207335424 0 .004 .029 .011 .00  .00  .00 
array-examples/standard_copy5_true-unreach-call_ground.i 5.22 3.01 216748032 1 .041 902    875    3759005696 1 871     .008 5.07 2.96 214409216 .012 .059 .031 .00  .00  5.06 2.89 207847424 0 .003 .029 .013 .00  .00  .00 
array-examples/standard_copy6_true-unreach-call_ground.i 5.16 2.99 214024192 1 .038 902    873    3755925504 1 870     858     5.04 2.90 223342592 .004 .035 .020 .00  .00  5.07 2.89 209457152 0 .003 .029 .012 .00  .00  .00 
array-examples/standard_copy7_true-unreach-call_ground.i 5.08 2.95 219017216 1 .038 902    877    3746902016 1 873     .010 5.33 3.03 220659712 .016 .055 .032 .00  .00  4.78 2.80 199626752 0 .004 .025 .014 .001 .00  .00 
array-examples/standard_copy8_true-unreach-call_ground.i 4.92 2.86 214421504 1 .034 902    876    3752140800 1 873     .010 4.67 2.72 220393472 .004 .026 .015 .00  .00  4.94 2.84 204414976 0 .004 .027 .011 .00  .00  .00 
array-examples/standard_copy9_true-unreach-call_ground.i 5.02 2.90 212844544 1 .038 902    874    3779952640 1 871     .005 5.23 3.01 221573120 .012 .058 .030 .00  .00  5.11 2.94 213143552 0 .004 .027 .012 .00  .00  .00 
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 4.89 2.85 210722816 1 .036 902    876    3712770048 1 872     .005 4.86 2.88 216797184 .004 .069 .029 .00  .00  5.05 2.89 206417920 0 .003 .027 .011 .00  .00  .00 
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 5.04 2.90 213749760 1 .038 902    878    3718352896 1 874     .005 5.05 2.92 221585408 .004 .065 .035 .00  .00  4.78 2.78 207290368 0 .008 .031 .013 .001 .00  .00 
array-examples/standard_copyInitSum_true-unreach-call_ground.i 4.91 2.87 212676608 1 .041 902    877    3706097664 1 873     .016 5.11 2.94 213037056 .014 .055 .033 .00  .00  5.06 2.89 207433728 0 .005 .027 .011 .00  .00  .00 
array-examples/standard_copyInit_true-unreach-call_ground.i 4.95 2.86 213749760 1 .039 902    877    3722936320 1 873     .006 4.59 6.69 217260032 .016 .069 .046 .00  .00  4.74 2.78 203550720 0 .004 .028 .009 .00  .00  .00 
array-examples/standard_find_true-unreach-call_ground.i 4.85 2.86 218775552 1 .038 902    857    3820269568 1 854     .005 5.16 2.97 213987328 .010 .066 .036 .001 .00  4.83 2.78 209588224 0 .004 .028 .012 .00  .00  .00 
array-examples/standard_init1_true-unreach-call_ground.i 5.13 2.92 213516288 1 .042 902    878    3699879936 1 875     866     5.03 2.88 219770880 .003 .037 .017 .00  .00  4.90 2.82 206221312 0 .003 .030 .013 .00  .00  .00 
array-examples/standard_init2_true-unreach-call_ground.i 5.18 2.95 214749184 1 .037 902    876    3721117696 1 872     862     4.94 2.87 219754496 .003 .041 .031 .00  .00  4.85 2.80 204742656 0 .004 .028 .013 .00  .00  .00 
array-examples/standard_init3_true-unreach-call_ground.i 4.86 2.79 217956352 1 .042 902    876    3728150528 1 872     862     4.89 2.82 217948160 .003 .031 .021 .00  .00  4.79 2.77 204050432 0 .004 .025 .013 .00  .00  .00 
array-examples/standard_init4_true-unreach-call_ground.i 5.19 3.00 218980352 1 .037 902    877    3723018240 1 873     863     5.14 3.07 218357760 .005 .043 .029 .00  .00  4.76 2.76 205795328 0 .003 .027 .011 .00  .00  .00 
array-examples/standard_init5_true-unreach-call_ground.i 4.82 2.76 215171072 1 .037 902    877    3716902912 1 873     863     5.19 3.01 219447296 .004 .028 .018 .00  .00  4.82 2.78 207794176 0 .009 .053 .023 .00  .00  .00 
array-examples/standard_init6_true-unreach-call_ground.i 5.23 3.05 218103808 1 .039 902    876    3736064000 1 872     861     5.15 2.99 215068672 .015 .061 .038 .00  .00  4.85 2.83 207192064 0 .003 .029 .012 .00  .00  .001
array-examples/standard_init7_true-unreach-call_ground.i 4.91 2.87 217632768 1 .036 902    876    3722076160 1 872     .006 5.15 3.00 213467136 .004 .038 .023 .00  .00  4.76 2.78 209166336 0 .003 .030 .010 .00  .00  .00 
array-examples/standard_init8_true-unreach-call_ground.i 5.14 2.97 218034176 1 .038 902    875    3756097536 1 871     860     5.38 3.10 221065216 .005 .030 .017 .001 .00  4.91 2.84 203304960 0 .004 .026 .011 .00  .00  .001
array-examples/standard_init9_true-unreach-call_ground.i 5.34 3.05 216711168 1 .038 902    877    3725856768 1 873     .007 4.98 2.89 218103808 .004 .039 .026 .00  .00  5.04 2.90 207708160 0 .003 .027 .011 .00  .00  .00 
array-examples/standard_maxInArray_true-unreach-call_ground.i 4.87 2.82 208027648 1 .036 902    874    3736305664 1 870     .006 5.15 2.99 218501120 .011 .037 .018 .00  .00  4.87 2.80 204804096 0 .003 .027 .011 .00  .00  .001
array-examples/standard_minInArray_true-unreach-call_ground.i 5.13 2.94 217071616 1 .037 902    875    3722653696 1 872     .005 4.88 2.87 218755072 .004 .049 .037 .001 .00  4.84 2.82 205422592 0 .004 .027 .010 .001 .00  .00 
array-examples/standard_palindrome_true-unreach-call_ground.i 5.00 2.89 211849216 1 .036 902    876    3714117632 1 872     .006 5.21 3.10 215515136 .004 .029 .016 .00  .00  4.89 2.81 203280384 0 .016 .039 .011 .00  .00  .001
array-examples/standard_partial_init_true-unreach-call_ground.i 4.95 2.88 214777856 1 .040 902    874    3738275840 1 870     858     4.87 2.83 211763200 .004 .052 .032 .00  .00  4.77 2.76 205213696 0 .004 .028 .011 .00  .00  .00 
array-examples/standard_partition_original_true-unreach-call_ground.i 4.99 2.92 213884928 1 .038 902    869    3764699136 1 866     .009 5.00 2.87 220065792 .003 .017 .009 .00  .00  4.71 2.75 210501632 0 .015 .052 .028 .00  .00  .00 
array-examples/standard_partition_true-unreach-call_ground.i 4.99 2.87 215207936 1 .044 902    872    3735633920 1 868     .012 4.90 2.82 219320320 .004 .025 .015 .00  .00  5.18 2.95 203649024 0 .004 .027 .009 .00  .00  .00 
array-examples/standard_password_true-unreach-call_ground.i 4.97 2.90 214269952 1 .039 902    871    3748601856 1 868     .008 4.71 2.76 221843456 .004 .027 .014 .00  .00  4.90 2.83 208158720 0 .003 .029 .009 .00  .00  .00 
array-examples/standard_reverse_true-unreach-call_ground.i 5.27 3.07 218902528 1 .039 902    877    3715010560 1 873     .006 5.16 3.01 217362432 .004 .031 .019 .00  .00  4.83 2.79 204980224 0 .004 .027 .010 .001 .00  .00 
array-examples/standard_running_true-unreach-call.i 5.13 2.98 220217344 1 .040 902    872    3745861632 1 869     857     4.92 2.80 214970368 .004 .026 .015 .00  .00  4.97 2.85 208900096 0 .004 .029 .013 .00  .00  .00 
array-examples/standard_sentinel_true-unreach-call.i 5.02 2.94 215162880 1 .044 902    859    3807719424 1 855     832     5.05 2.94 211881984 .004 .054 .032 .00  .00  4.89 2.85 206282752 0 .004 .030 .011 .001 .00  .00 
array-examples/standard_seq_init_true-unreach-call_ground.i 4.89 2.86 218185728 1 .036 902    876    3717496832 1 872     862     4.89 2.84 219709440 .004 .026 .014 .001 .00  4.73 2.73 202113024 0 .004 .026 .011 .001 .00  .002
array-examples/standard_strcmp_true-unreach-call_ground.i 4.91 2.89 215805952 1 .042 902    873    3758755840 1 869     .013 4.83 2.80 216211456 .012 .053 .019 .00  .00  5.05 2.89 209637376 0 .003 .035 .019 .00  .00  .00 
array-examples/standard_strcpy_original_true-unreach-call.i 5.19 2.98 215937024 1 .038 7.09 3.95 308367360 1 .433 .005 4.93 2.87 217161728 .004 .031 .021 .001 .00  5.00 2.86 204689408 0 .004 .026 .010 .00  .00  .002
array-examples/standard_strcpy_true-unreach-call_ground.i 5.12 2.98 215728128 1 .037 902    856    3832774656 1 853     .005 5.44 3.14 219676672 .004 .049 .030 .00  .00  4.83 2.80 208424960 0 .004 .045 .026 .001 .00  .00 
array-examples/standard_two_index_01_true-unreach-call.i 4.70 2.75 212541440 1 .034 902    878    3722952704 1 874     .016 5.03 2.90 218644480 .004 .051 .023 .001 .00  4.93 2.78 210591744 0 .003 .034 .018 .00  .00  .00 
array-examples/standard_two_index_02_true-unreach-call.i 5.00 2.90 212893696 1 .039 902    876    3730182144 1 872     .010 5.09 2.95 212312064 .004 .029 .015 .00  .00  5.11 2.92 209510400 0 .004 .026 .010 .00  .00  .00 
array-examples/standard_two_index_03_true-unreach-call.i 4.97 2.87 215441408 1 .036 278    248    3772493824 1 244     .011 4.96 2.94 216178688 .004 .037 .024 .00  .00  4.80 2.80 207962112 0 .004 .038 .021 .001 .00  .00 
array-examples/standard_two_index_04_true-unreach-call.i 5.08 2.96 216793088 1 .038 902    876    3748114432 1 872     862     4.90 2.87 216260608 .004 .039 .028 .00  .00  4.89 2.79 205742080 0 .004 .028 .010 .00  .00  .00 
array-examples/standard_two_index_05_true-unreach-call.i 4.99 2.87 218484736 1 .036 902    876    3733733376 1 872     .012 4.75 2.75 213098496 .011 .042 .024 .00  .00  4.82 2.73 208519168 0 .003 .043 .027 .00  .00  .00 
array-examples/standard_two_index_06_true-unreach-call.i 4.89 2.87 216379392 1 .037 99.5  75.4  3329064960 1 71.7   .005 5.06 2.99 217112576 .003 .067 .045 .00  .00  5.00 2.86 203546624 0 .004 .026 .010 .00  .00  .00 
array-examples/standard_two_index_07_true-unreach-call.i 5.04 2.95 211324928 1 .039 902    875    3734241280 1 871     .006 4.87 2.86 220622848 .016 .050 .028 .001 .00  4.70 2.73 206729216 0 .003 .031 .010 .00  .00  .00 
array-examples/standard_two_index_08_true-unreach-call.i 5.12 3.00 215826432 1 .038 902    875    3736272896 1 871     860     5.04 2.90 222879744 .016 .055 .032 .00  .00  4.68 2.72 203251712 0 .004 .024 .010 .00  .00  .00 
array-examples/standard_two_index_09_true-unreach-call.i 5.13 2.97 215961600 1 .037 902    875    3745927168 1 871     .006 4.85 2.86 212221952 .004 .050 .039 .00  .00  4.70 2.72 208699392 0 .004 .028 .011 .00  .00  .00 
array-examples/standard_vararg_true-unreach-call_ground.i 4.86 2.81 213377024 1 .038 902    863    3797499904 1 859     838     5.06 2.93 218476544 .012 .054 .035 .00  .00  4.87 2.80 202735616 0 .003 .028 .011 .00  .00  .00 
array-examples/standard_vector_difference_true-unreach-call_ground.i 5.22 2.99 214945792 1 .039 902    873    3723071488 1 870     .008 4.85 2.82 219516928 .004 .052 .030 .00  .00  5.07 2.88 205529088 0 .003 .029 .013 .00  .00  .00 
reducercommutativity/rangesum05_false-unreach-call.i 13.7  10.2  425275392 18 .878 .178 5.43  902    886    1355051008 8 .234 .012 .020 .001 2.78  878     92.5  82.3  585662464 66.9   68.8   .778 66.7   61.3   10.2   61.7   66.6   31.9   29.4   77.4  71.3  456286208 179 28.8   33.5   .820 28.7   26.2   3.48  0 34.6   26.1   28.6   12.4   13.7  
reducercommutativity/rangesum10_false-unreach-call.i 26.6  22.4  489586688 33 .973 .798 14.5   902    886    1632976896 11 .235 .005 .025 .003 4.36  877     312    296    1009377280 265     269     1.61  265     239     24.4   240     265     137     102     347    331    879697920 1134 130     187     2.17  130     122     53.8   0 140     118     130     62.3   60.0  
reducercommutativity/rangesum20_false-unreach-call.i 29.7  24.5  722432000 63 1.33  4.80  12.1   902    884    1766027264 12 .207 .005 .027 .002 4.55  874     902    879    1390931968 815     825     4.24  815     729     51.0   734     814     378     351     902    883    1091399680 2647 129     697     3.52  129     118     564     0 183     109     129     88.4   29.1  
reducercommutativity/rangesum40_false-unreach-call.i 135    128    1123004416 123 1.76  17.6   98.2   902    881    1955381248 13 .251 .004 .011 .003 6.54  870     902    875    1798283264 743     756     7.75  742     639     115     647     742     383     255     902    892    880504832 1198 48.4   831     1.88  48.2   45.6   780     0 58.8   42.6   48.2   40.0   4.90 
reducercommutativity/rangesum60_false-unreach-call.i 903    896    1648361472 183 1.73  38.3   852     902    880    2197110784 12 .204 .005 .005 .00  7.57  867     903    876    1917911040 629     642     6.43  628     515     231     526     627     364     151     902    893    849530880 845 22.7   856     .884 22.6   22.3   832     0 34.6   20.0   22.6   9.08  12.0  
reducercommutativity/rangesum_false-unreach-call.i 795    773    2884550656 903    452    4598747136 5 1.65  424     18.8   5.97  6.57  414     72.7  64.0  563089408 52.5   53.7   .615 52.4   48.4   6.90  48.7   52.3   23.6   24.8   902    884    1057783808 3703 99.9   843     1.79  99.7   114     740     389 37.9   90.7   99.7   47.0   43.6  
reducercommutativity/avg05_true-unreach-call.i 903    897    894750720 18 .353 .139 894     902    890    1377763328 13 .227 .007 .083 .002 3.87  881     902    892    1440649216 322     323     .570 322     314     566     314     322     79.4   234     902    896    1542561792 58 5.91  7.76  .381 5.84  5.69  1.28  0 885     5.43  5.82  3.06  2.40 
reducercommutativity/avg10_true-unreach-call.i 902    896    930549760 33 1.04  .748 892     903    889    1445343232 13 .254 .009 .039 .001 4.34  879     902    888    798191616 881     883     .589 881     864     2.86  865     881     174     690     902    895    1529323520 213 14.0   20.3   .658 13.5   13.4   5.42  0 871     12.7   13.5   11.2   1.69 
reducercommutativity/avg20_true-unreach-call.i 902    896    992264192 63 1.23  4.58  888     902    884    1527914496 16 .259 .010 .011 .002 6.27  872     902    887    796737536 880     882     .658 880     863     2.93  865     880     163     701     902    894    2416480256 823 18.0   76.8   1.13  17.9   16.6   57.4   0 814     15.5   17.8   8.42  7.66 
reducercommutativity/avg40_true-unreach-call.i 1000    992    1591664640 902    883    1616912384 15 .252 .010 .012 .001 7.77  870     902    888    809558016 881     882     .709 880     863     2.92  865     880     151     713     902    888    1011867648 2528 58.1   801     2.04  58.0   57.2   740     0 84.7   54.5   58.0   25.5   30.1  
reducercommutativity/avg60_true-unreach-call.i 904    897    1903976448 183 1.93  37.1   854     902    878    1871958016 16 .195 .011 .014 .001 12.2   860     902    888    817635328 880     882     .653 880     862     3.00  864     880     181     682     902    886    1092460544 4226 51.7   763     1.99  51.5   50.7   709     0 120     47.2   51.5   40.7   7.58 
reducercommutativity/avg_true-unreach-call.i 903    888    1504915456 10 6.60  642     233     903    453    4380495872 6 2.04  424     89.6   9.30  7.82  338     902    895    509124608 890     890     .332 890     888     1.70  888     890     26.5   861     913    906    1354326016
reducercommutativity/max05_true-unreach-call.i 18.1  14.8  347725824 18 .810 2.28  8.52  115    97.2  1037770752 18 .421 .005 2.41  8.22  6.29  75.7   913    903    1068703744 913    907    2671058944
reducercommutativity/max10_true-unreach-call.i 902    896    828940288 33 .994 12.5   880     902    881    1099091968 18 .458 .010 1.96  .00  7.86  866     903    887    2882105344 45.0   48.2   1.74  44.7   34.6   836     37.0   44.5   13.7   20.9   903    895    2368585728 213 .727 8.31  1.33  .660 .533 5.93  0 884     .235 .637 .360 .050
reducercommutativity/max20_true-unreach-call.i 903    896    1284513792 63 .925 188     704     902    878    1243013120 20 .633 .011 2.67  .002 13.3   857     903    875    4250365952 411     421     3.41  409     322     451     345     409     124     198     903    893    2024013824 823 1.44  77.4   1.20  1.33  1.34  74.0   0 813     .401 1.30  .865 .086
reducercommutativity/max40_true-unreach-call.i 903    896    1204494336 100 1.32  891     .003 903    873    2634997760 40 .710 .006 19.5   .008 31.9   816     902    876    3476172800 845     861     2.85  843     695     12.4   753     842     186     509     902    886    919556096 2097 2.22  840     2.32  2.09  2.69  835     0 43.5   .624 2.03  1.34  .137
reducercommutativity/max60_true-unreach-call.i 902    896    980779008 104 1.53  891     .009 904    872    4182941696 60 .668 .005 67.1   .006 58.4   738     902    877    3649691648 848     860     2.53  846     695     12.9   752     845     196     498     902    889    575082496 1141 .704 872     1.37  .604 1.34  870     0 13.4   .317 .563 .211 .077
reducercommutativity/max_true-unreach-call.i 903    888    1406636032 15 11.5   755     115     903    452    4289490944 10 5.82  .013 124     13.9   17.1   286     37.8  32.0  434892800 4.13  5.02  .556 4.04  3.07  24.0   3.28  4.01  1.76  1.30  902    884    1108680704 3983 2.05  880     1.82  1.89  6.90  875     409 1.61  1.19  1.83  .900 .210
reducercommutativity/sep05_true-unreach-call.i 10.8  7.51 353878016 18 .482 2.89  1.01  8.79 4.83 324349952 1 .399 .823 .013 .00  902    886    1306243072 874     876     .788 874     821     7.49  872     874     4.48  817     20.3  15.5  378843136 62 .395 3.02  .527 .329 1.56  1.36  4 9.56  .142 .310 .158 .025
reducercommutativity/sep10_true-unreach-call.i 32.5  28.7  485408768 33 1.16  16.5   7.72  902    452    4012482560 12 .698 .005 3.09  .025 12.7   431     913    894    1197264896 913    905    647471104
reducercommutativity/sep20_true-unreach-call.i 335    330    970399744 63 1.12  191     134     903    452    4035473408 20 1.06  423     5.34  .002 19.7   421     903    871    2963673088 504     516     4.16  503     406     352     432     502     143     263     902    893    702160896 823 1.96  78.1   1.33  1.85  1.85  74.3   0 812     .849 1.80  1.35  .083
reducercommutativity/sep40_true-unreach-call.i 902    896    1164984320 91 1.32  891     .006 8.74 4.73 324964352 1 .267 .813 .011 .00  .499 .317 902    874    2875150336 843     856     2.68  842     707     15.1   756     841     187     520     902    887    1022529536 2412 2.71  803     1.97  2.56  3.36  798     0 81.2   .661 2.52  1.74  .143
reducercommutativity/sep60_true-unreach-call.i 903    896    941830144 91 1.51  891     .002 8.89 4.83 325820416 1 .240 .759 .011 .00  .526 .198 902    877    2765737984 845     859     3.11  843     710     14.7   760     842     185     526     902    882    1068806144 4000 2.51  746     2.80  2.35  3.66  740     0 133     .824 2.30  1.43  .199
reducercommutativity/sep_true-unreach-call.i 903    882    1346113536 14 12.4   814     50.6   902    452    4110774272 8 4.53  414     85.5   3.36  18.4   335     902    889    1213788160 884     885     .621 884     854     .718 881     884     4.60  849     902    881    986865664 7080 2.64  878     2.88  2.46  12.0   871     612 .527 1.47  2.39  1.18  .248
reducercommutativity/sum05_true-unreach-call.i 902    897    684908544 18 .851 .159 893     903    886    1274327040 18 .435 .013 .159 857     4.45  20.0   902    893    1360437248 8.99  10.1   .517 8.85  6.33  880     6.85  8.80  1.98  4.35  902    896    1343381504 58 .385 1.73  .417 .320 .211 .713 0 891     .138 .309 .135 .031
reducercommutativity/sum10_true-unreach-call.i 902    896    740175872 33 .506 1.26  892     7.59 4.18 318832640 1 .225 .632 .001 .00  902    885    1783533568 55.7   58.2   1.15  55.4   44.5   824     47.3   55.3   13.0   31.4   902    894    1300975616 213 1.23  7.10  .619 1.16  1.01  4.99  0 884     .710 1.13  .821 .051
reducercommutativity/sum20_true-unreach-call.i 902    896    920489984 63 .829 5.00  887     903    878    2261934080 39 .489 .007 .520 .00  17.7   854     903    874    3898712064 473     482     3.27  472     382     389     411     471     118     265     902    893    1585426432 823 1.49  59.3   1.05  1.41  1.36  56.4   0 831     .400 1.38  .879 .081
reducercommutativity/sum40_true-unreach-call.i 1000    993    1397686272 903    875    2620690432 42 .448 .006 .133 .002 28.6   840     902    878    3086475264 855     865     1.85  853     717     10.0   783     853     154     564     902    888    964481024 3039 2.85  798     2.11  2.73  3.42  793     0 86.5   .766 2.68  1.77  .166
reducercommutativity/sum60_true-unreach-call.i 1000    991    2011811840 8.61 4.72 308240384 1 .237 .717 .001 .00  902    877    3082153984 854     863     1.76  853     721     11.5   782     852     152     568     902    885    989093888 4295 3.48  790     2.10  3.36  4.79  784     0 92.2   1.36  3.31  1.78  .683
reducercommutativity/sum_true-unreach-call.i 911    887    2615713792 18 13.0   131     735     921    461    4816011264 15 10.8   420     122     151     24.4   145     902    891    1662038016 880     881     .405 880     406     6.82  879     880     1.63  404     902    885    1163739136 6388 3.40  872     2.10  3.26  21.3   865     571 9.97  2.26  3.20  1.95  .282
bitvector/byte_add_false-unreach-call.i 8.22 4.65 336216064 3 .983 .033 .053 26.9  13.9  690241536 3 1.24  2.46  .176 .357 3.12  1.73  28.5  21.2  561971200 15.9   17.2   .512 15.8   13.7   .859 14.9   15.7   .657 13.1   9.75 5.72 344141824 39 .148 1.61  .349 .067 .037 .834 3 .874 .023 .055 .018 .001
bitvector/byte_add_1_true-unreach-call.i 7.53 4.30 301768704 6 .922 .102 .119 36.4  18.6  822779904 6 1.36  3.26  .621 .921 7.19  3.89  23.0  15.0  753598464 10.1   11.2   .446 10.0   5.91  .887 9.27  9.98  .995 4.92  13.0  7.99 369778688 45 .118 2.96  .339 .059 .495 2.19  9 1.64  .023 .047 .019 .002
bitvector/byte_add_2_true-unreach-call.i 7.58 4.33 297213952 6 .884 .105 .168 36.3  18.6  948129792 6 1.16  3.48  .649 1.07  7.16  4.01  902    891    1202393088 885     887     .841 885     578     .996 884     885     .634 578     13.3  8.35 367284224 55 .160 3.14  .409 .073 .564 2.31  9 1.78  .034 .063 .028 .001
bitvector/gcd_1_true-unreach-call.i 7.65 5.42 241795072 2 .151 2.27  .085 10.7  6.80 351907840 2 .217 .012 2.52  .138 .160 .091 13.2  10.4  254025728 4.54  4.74  .100 4.49  4.29  2.78  4.36  4.49  .468 3.83  244    241    451780608 29 .071 184     .177 .044 30.8   184     1 53.7   .015 .041 .006 .001
bitvector/gcd_2_true-unreach-call.i 189    185    396636160 11 .378 107     73.7   189    184    551194624 10 .440 .010 43.1   40.5   .497 95.1   16.2  13.1  266006528 9.70  9.91  .108 9.66  9.42  .230 9.49  9.66  .615 8.81  630    625    528089088 56 .089 447     .191 .060 187     447     1 175     .015 .048 .010 .00 
bitvector/gcd_3_true-unreach-call.i 208    205    379392000 11 .371 120     79.9   181    176    543576064 10 .406 .005 31.2   45.5   .509 93.6   351    345    408158208 341     341     .113 341     341     .202 341     341     2.30  338     709    704    434868224 56 .086 479     .167 .049 201     479     1 223     .015 .042 .012 .00 
bitvector/gcd_4_true-unreach-call.i 5.41 3.10 221007872 6 .145 .005 .00  12.3  6.57 415752192 3 .237 .006 .013 .00  .666 1.73  10.2  6.38 373968896 1.88  2.35  .232 1.79  1.20  .743 1.32  1.77  .900 .295 12.3  9.43 260395008 16 3.48  4.06  .175 3.44  3.31  .277 1 2.60  3.12  3.44  3.05  .065
bitvector/interleave_bits_true-unreach-call.i 5.86 3.33 230367232 17 .262 .013 .003 12.4  7.00 390651904 16 .310 .005 .015 .00  1.07  1.89  14.2  8.28 415965184 2.76  3.98  .341 2.64  .625 1.25  1.24  2.57  .406 .219 13.1  9.82 257282048 137 .156 5.51  .244 .126 .486 4.95  1 1.47  .050 .122 .045 .003
bitvector/jain_1_true-unreach-call.i 780    765    14999998464 918    900    14201999360 620 3.23  .007 106     113     9.44  639     5.35 3.09 232951808 .078 .219 .094 .059 .016 .066 .025 .057 .015 .001 5.13 2.96 218767360 3 .031 .178 .074 .020 .008 .024 1 .058 .006 .017 .004 .00 
bitvector/jain_2_true-unreach-call.i 424    411    14999998464 762    745    14999998464 5.17 3.06 230834176 .106 .215 .065 .072 .018 .071 .034 .069 .016 .002 5.02 2.95 214327296 3 .043 .198 .083 .029 .013 .034 1 .087 .011 .022 .008 .00 
bitvector/jain_4_true-unreach-call.i 362    351    14999998464 679    661    14999998464 5.32 3.09 236695552 .104 .244 .082 .090 .036 .084 .050 .086 .027 .009 5.25 3.04 225370112 3 .040 .220 .092 .029 .016 .043 1 .080 .013 .027 .010 .00 
bitvector/jain_5_true-unreach-call.i 904    881    1880334336 5876 58.1   520     .908 905    454    6293446656 322 1.99  431     3.22  .019 5.75  434     902    881    4971737088 173     183     1.13  173     34.3   695     76.8   172     32.8   1.47  903    886    841629696 5356 .444 579     .310 .388 5.81  578     0 304     .157 .365 .124 .013
bitvector/jain_6_true-unreach-call.i 368    357    14999998464 696    677    14999998464 5.40 3.18 233029632 .118 .251 .084 .100 .029 .082 .049 .096 .024 .005 5.36 3.11 220246016 3 .043 .236 .111 .029 .016 .047 1 .089 .013 .028 .012 .00 
bitvector/jain_7_true-unreach-call.i 865    850    14999998464 954    908    14348861440 411 3.39  .009 95.2   126     8.29  663     7.81 5.37 236834816 .236 .398 .094 .224 .051 2.08  .125 .221 .047 .004 7.45 5.17 227180544 3 .041 .271 .090 .027 .020 .079 1 2.11  .011 .024 .007 .001
bitvector/modulus_true-unreach-call.i 458    444    1247305728 46 11.1   311     113     81.7  41.3  2317275136 1 .347 32.3   .031 4.57  .500 32.0   902    897    359145472 892     892     .079 892     892     1.96  892     892     .360 892     18.9  16.6  246931456 3 .249 11.6   .116 .234 6.79  11.2   2 2.13  .214 .231 .210 .002
bitvector/num_conversion_1_true-unreach-call.i 5.57 3.22 217026560 9 .201 .006 .001 10.8  5.85 370155520 9 .421 1.22  .006 .00  .876 .446 8.49 4.78 342761472 1.18  1.67  .199 1.10  .144 .254 .285 1.08  .135 .009 6.73 3.93 231309312 37 .082 .671 .159 .060 .100 .332 1 .288 .016 .043 .009 .002
bitvector/num_conversion_2_true-unreach-call.i 5.45 3.17 231354368 9 .228 .063 .029 11.3  6.07 409710592 9 .470 1.36  .272 .106 .692 .337 27.6  21.3  751804416 12.7   13.2   .163 12.6   1.70  5.22  11.0   12.6   .740 .962 12.7  9.21 273465344 37 .092 .736 .161 .048 .795 .358 1 5.76  .017 .039 .008 .002
bitvector/parity_true-unreach-call.i 18.4  14.5  323182592 33 .820 .298 10.3   28.2  19.8  413130752 33 .891 .015 .306 10.7   1.21  2.63  224    209    1156411392 191     193     .435 191     172     12.9   179     191     142     29.8   49.9  44.5  442191872 529 .371 19.5   .332 .288 9.79  18.5   1 22.1   .174 .273 .153 .009
bitvector/sum02_true-unreach-call.i 913    895    9315799040 903    453    5149470720 212 3.57  430     4.33  6.07  5.47  426     902    879    3972395008 604     612     .904 603     136     264     521     603     108     28.6   902    889    856117248 5262 2.70  584     .516 2.61  10.8   581     0 302     1.66  2.56  1.56  .071
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c 17.6  11.1  457502720 8 2.46  .721 .609 74.0  37.5  1464958976 8 3.47  13.2   2.93  1.57  7.58  8.05  23.5  14.8  531087360 4.30  6.42  .843 4.09  3.48  1.88  3.66  4.05  .811 2.67  21.3  15.1  497954816 30 .651 6.66  1.06  .542 .626 4.19  2 2.18  .406 .527 .341 .054
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c 22.8  15.3  544681984 11 2.75  1.23  1.04  86.2  43.7  1520918528 11 4.22  18.6   3.52  1.84  8.45  8.90  57.0  44.0  888573952 29.9   32.5   1.00  29.7   27.7   1.94  29.0   29.6   1.41  26.3   28.2  20.4  552579072 55 .664 8.21  1.24  .547 .797 5.47  0 3.22  .350 .521 .298 .046
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c 13.5  7.76 412733440 6 1.90  .243 .221 50.5  25.6  992468992 6 2.77  5.97  1.29  .732 6.77  3.64  16.6  9.45 462725120 1.47  3.18  .691 1.24  .829 1.71  .955 1.20  .402 .427 14.3  8.74 411545600 15 .474 3.14  .600 .346 .302 1.06  0 1.03  .199 .324 .183 .010
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c 28.3  20.4  587567104 15 3.60  6.81  5.53  79.6  40.3  1396162560 8 3.42  16.2   2.74  .805 7.92  19.6   902    888    1132036096 881     883     .762 881     786     1.39  880     881     1.55  785     87.0  78.6  828219392 109 1.47  48.7   1.45  1.30  19.2   43.4   4 26.3   1.01  1.27  .879 .119
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c 21.1  13.5  468557824 15 3.54  2.91  2.79  48.9  24.9  961609728 7 3.26  7.14  2.94  .468 8.16  4.08  902    886    1397288960 877     880     1.10  877     689     2.49  875     877     1.55  688     52.6  41.9  552554496 106 .994 28.2   1.53  .792 4.34  24.3   1 10.0   .559 .754 .484 .065
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c 22.1  14.2  481087488 15 3.54  3.37  2.92  52.6  26.7  970153984 7 3.21  6.70  2.44  .733 8.15  6.83  902    885    1273081856 877     880     .956 877     820     2.04  875     877     2.00  818     913    900    940695552
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c 904    886    2287824896 28 5.52  547     321     903    452    4680593408 15 4.56  418     63.0   19.2   11.6   345     902    891    698494976 886     887     .684 885     884     .832 884     885     2.39  882     902    893    971743232 33 1.82  878     1.32  1.69  11.8   873     0 11.9   1.38  1.65  1.02  .343
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c 904    888    3313184768 69 9.75  305     546     59.2  30.0  1047638016 7 4.25  8.31  3.45  1.14  8.76  6.88  57.9  40.2  929566720 27.4   33.4   2.69  26.3   22.8   2.69  24.4   26.2   3.94  18.9   902    884    2168688640 595 2.82  622     2.24  2.63  161     610     0 258     2.11  2.56  1.73  .343
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c 905    886    3177459712 63 9.36  244     611     374    188    4419948544 28 9.18  .013 42.0   68.0   14.0   44.3   901    885    1535066112 863     867     1.56  862     653     15.3   861     862     2.37  651     913    902    820006912
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c 906    885    3167014912 62 9.27  236     618     372    187    3721695232 27 9.22  .011 47.0   64.0   13.6   43.7   675    657    1295237120 647     652     2.38  647     580     .954 645     647     2.88  577     913    902    748576768
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c 905    888    3556110336 45 7.28  362     497     912    457    5845696512 28 7.29  417     122     162     15.1   135     64.4  49.8  849940480 38.9   44.3   2.34  38.5   35.9   1.50  36.9   38.4   6.58  29.3   902    887    1890832384 292 5.41  793     1.41  4.62  61.4   782     0 90.9   4.14  4.58  3.81  .299
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c 904    888    3507056640 45 6.90  371     486     904    453    5506842624 27 7.31  .004 136     142     14.3   138     64.1  49.4  887455744 37.5   43.4   2.59  36.6   33.9   1.65  34.9   36.5   5.74  28.1   902    885    1779732480 352 4.18  724     1.52  3.56  115     712     0 158     2.94  3.51  2.53  .387
bitvector/soft_float_1_true-unreach-call.c.cil.c 285    254    3888402432 48 88.5   14.8   116     949    858    5020315648 22 24.4   .013 2.42  82.7   217     519     24.8  14.9  414203904 7.87  10.7   1.46  7.64  6.63  .908 6.66  7.53  6.59  .039 24.5  15.8  394366976 9 8.26  10.9   1.41  8.11  7.27  .067 9 1.86  7.29  8.04  7.24  .014
bitvector/soft_float_2_true-unreach-call.c.cil.c 250    217    4046934016 72 88.1   26.3   60.2   27.2  14.0  593768448 1 .284 .004 .001 .001 282    255    2009251840 225     247     6.31  223     153     4.57  190     222     56.9   96.2   62.7  43.4  838426624 285 10.6   26.9   7.88  9.92  8.94  3.83  9 13.3   8.31  9.65  8.04  .240
bitvector/soft_float_3_true-unreach-call.c.cil.c 289    258    4158345216 72 88.1   23.5   106     940    840    7494975488 32 7.44  .010 1.84  15.8   488     269     267    239    1832505344 204     224     6.54  201     137     11.7   169     201     49.3   87.7   85.4  63.3  877219840 285 14.1   30.3   6.79  13.5   12.1   4.38  9 29.7   11.7   13.2   11.3   .308
bitvector/soft_float_4_true-unreach-call.c.cil.c 908    888    1226805248 14 12.8   .968 853     867    804    1904013312 1 1.93  .005 .026 49.5   5.64  742     291    284    434761728 278     280     .955 278     277     .425 277     278     277     .00  415    408    420892672 0 403     405     1.06  403     401     .017 .074 401     402     401     .00 
bitvector/soft_float_5_true-unreach-call.c.cil.c 224    195    4073275392 72 75.1   25.7   52.8   18.9  9.87 479285248 1 .313 .007 .001 .00  275    250    2092691456 223     242     6.51  221     154     4.60  186     220     56.1   97.9   68.4  46.1  849084416 285 11.4   28.1   7.30  11.0   9.71  3.98  9 14.4   9.07  10.6   8.74  .301
bitvector-regression/implicitfloatconversion_false-unreach-call.i 5.22 3.08 246386688 1 .066 .00  7.16 4.05 332992512 1 .125 .006 .001 5.55 3.27 246996992 .008 .092 .063 .001 .00  .055 .001 .00  .00  4.81 2.82 230608896 0 .007 .069 .040 .001 .00  .00  .077 .001 .00  .00 
bitvector-regression/implicitunsignedconversion_false-unreach-call.i 5.29 3.12 238088192 1 .066 .00  7.24 4.05 320548864 1 .115 .008 .00  5.23 3.10 248676352 .007 .076 .055 .002 .00  .055 .00  .00  .00  5.34 3.13 230309888 0 .008 .101 .073 .001 .00  .00  .060 .001 .00  .00 
bitvector-regression/integerpromotion_false-unreach-call.i 7.21 4.12 315355136 1 .238 .001 9.80 5.39 354238464 1 .455 .005 .001 6.76 3.82 344080384 .007 .099 .056 .001 .00  .077 .001 .00  .00  6.51 3.75 305397760 0 .006 .146 .067 .002 .00  .00  .075 .00  .00  .00 
bitvector-regression/signextension2_false-unreach-call.i 7.32 4.14 322039808 1 .235 .001 10.3  5.54 365801472 1 .423 .006 .00  7.79 4.42 349814784 .018 .122 .058 .002 .00  .083 .001 .00  .00  6.85 3.85 315662336 0 .008 .116 .054 .001 .00  .00  .094 .00  .00  .00 
bitvector-regression/signextension_false-unreach-call.i 7.55 4.32 317681664 1 .266 .001 10.3  5.50 360538112 1 .358 .797 .001 6.82 3.88 343175168 .009 .108 .057 .001 .00  .066 .00  .00  .00  6.52 3.66 285175808 0 .007 .138 .047 .001 .00  .00  .098 .001 .00  .00 
bitvector-regression/implicitunsignedconversion_true-unreach-call.i 4.84 2.80 215502848 1 .052 .00  .00  6.25 3.47 299659264 1 .069 .007 5.10 2.90 221974528 .034 .101 .043 .022 .001 .040 .011 .019 .001 .00  5.02 2.90 210186240 0 .017 .116 .075 .012 .001 .00  .036 .003 .010 .001 .00 
bitvector-regression/integerpromotion_true-unreach-call.i 6.14 3.49 235868160 1 .228 .00  .00  7.51 4.13 323211264 1 .265 .005 6.33 3.60 231157760 .037 .163 .069 .019 .00  .032 .008 .017 .00  .00  5.81 3.31 216825856 0 .021 .160 .078 .016 .00  .00  .037 .008 .015 .00  .00 
bitvector-regression/signextension2_true-unreach-call.i 6.66 3.76 294555648 1 .247 .00  .00  8.01 4.37 313405440 1 .402 .005 .00  .001 6.32 3.61 236077056 .042 .172 .065 .029 .004 .055 .015 .029 .004 .00  5.74 3.28 216780800 0 .037 .216 .075 .019 .004 .00  .045 .007 .016 .004 .00 
bitvector-regression/signextension_true-unreach-call.i 6.72 3.79 284733440 1 .236 .00  .00  8.18 4.44 303001600 1 .325 .558 .00  .00  5.84 3.38 230023168 .036 .173 .059 .028 .004 .045 .015 .026 .004 .00  5.65 3.23 217305088 0 .028 .174 .076 .016 .003 .00  .041 .004 .015 .003 .00 
bitvector-loops/diamond_false-unreach-call2.i 7.35 4.22 320241664 2 .278 .016 .017 11.8  6.31 368349184 2 .558 1.15  .026 .039 .422 .061 6.80 3.98 346423296 .083 .270 .115 .058 .016 .154 .030 .054 .015 .001 6.47 3.68 310808576 1 .050 .228 .105 .026 .008 .021 0 .161 .009 .018 .006 .001
bitvector-loops/overflow_false-unreach-call1.i 903    883    1610653696 9957 54.9   551     1.19  904    454    6394228736 575 2.16  .006 3.63  .036 12.5   425     902    881    5204762624 162     176     1.00  161     33.0   702     66.4   160     31.7   1.31  903    886    859955200 9523 .548 478     .417 .460 8.32  477     0 404     .183 .427 .150 .007
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 10.6  6.55 387854336 12 .976 .122 .170 26.9  15.9  621314048 12 .612 .010 .153 .221 3.55  3.99  902    892    1196449792 887     888     .740 887     654     1.70  885     886     .706 653     15.7  11.0  377040896 121 .128 3.91  .351 .077 .285 3.24  0 4.08  .022 .071 .014 .001
heap-manipulation/bubble_sort_linux_false-unreach-call.i 23.6  17.4  517013504 1 1.07  .176 51.8  30.0  933621760 1 3.02  .008 1.24  947    918    2861035520 673     676     1.05  673     111     191     84.3   673     45.9   65.5   914    904    2032943104
heap-manipulation/dll_of_dll_false-unreach-call.i 7.99 4.42 303452160 1 .904 136    109    1903747072 2 1.71  .011 .534 .566 17.5   .535 7.58 4.24 319741952 .007 .615 .136 .00  .00  6.37 3.63 230100992 0 .022 .238 .126 .001 .00  .00 
heap-manipulation/merge_sort_false-unreach-call.i 33.3  25.3  691920896 2 2.22  .028 .210 110    60.9  1374842880 2 2.73  .017 .047 .201 18.0   7.82  20.4  12.8  437039104 1.27  2.06  .380 1.16  .512 2.11  .449 1.13  .450 .062 10.9  6.57 350994432 12 .160 1.57  .300 .117 .127 .909 6 .909 .068 .106 .035 .020
heap-manipulation/sll_to_dll_rev_false-unreach-call.i 11.9  7.49 394604544 1 .937 .121 39.6  20.4  884432896 1 2.37  .019 .677 904    889    962441216 878     880     1.11  878     868     3.05  874     878     12.6   855     903    891    995389440 850 .547 337     .995 .481 546     325     0 551     .265 .461 .213 .031
heap-manipulation/bubble_sort_linux_true-unreach-call.i 929    897    4407533568 6 61.7   97.6   730     1000    919    5902766080 .008 902    882    2624708608 683     686     .786 683     108     191     81.8   682     42.6   65.1   902    893    1545728000 14 2.26  590     .530 2.22  161     587     0 300     2.06  2.21  .486 1.50 
heap-manipulation/dancing_true-unreach-call.i 7.70 4.28 304799744 1 .826 9.62 5.17 331853824 1 .541 .009 7.13 4.01 325128192 .009 .221 .134 .001 .00  .001 .00  .00  6.27 3.53 233570304 0 .012 .245 .126 .004 .00  .006 .001 .00  .00 
heap-manipulation/dll_of_dll_true-unreach-call.i 7.95 4.43 310816768 1 .757 134    108    1350369280 2 1.73  .007 .379 .311 17.5   .556 7.08 4.01 317181952 .008 .205 .131 .001 .00  6.49 3.63 233197568 0 .007 .221 .115 .001 .00  .001
heap-manipulation/merge_sort_true-unreach-call.i 940    859    5924052992 6 759     56.3   35.7   913    812    6042918912 5 222     .003 58.0   47.0   424     43.9   902    888    867217408 883     884     .432 883     877     1.08  881     883     4.64  872     902    887    1132617728 335 1.14  218     1.46  1.01  578     211     49 665     .617 .948 .338 .190
heap-manipulation/sll_to_dll_rev_true-unreach-call.i 1000    887    7367028736 903    823    7073222656 3 40.1   .015 22.3   196     550     7.55  902    889    966860800 882     884     1.12  882     874     1.42  878     882     12.1   861     902    893    981245952 786 .396 274     .839 .323 599     260     0 616     .122 .306 .093 .020
list-properties/alternating_list_false-unreach-call.i 8.80 5.05 346804224 2 .903 .017 .033 20.1  10.8  490651648 2 1.26  .006 .032 .046 1.62  1.18  8.57 4.87 370561024 .264 .564 .176 .231 .107 .642 .145 .226 .077 .030 8.53 4.84 327966720 3 .538 .943 .217 .515 .061 .046 1 .235 .060 .512 .040 .009
list-properties/list_false-unreach-call.i 14.1  9.67 372002816 2 1.17  .014 .044 22.6  13.7  521592832 2 1.21  .007 .023 .061 2.20  .454 902    889    906043392 883     885     .612 883     874     1.41  880     883     9.13  865     902    893    753659904 4260 2.79  889     .676 2.74  2.00  885     32 .097 1.94  2.72  1.58  .342
list-properties/list_flag_false-unreach-call.i 11.2  6.97 372674560 2 1.00  .013 .060 19.7  11.0  556544000 2 1.08  .004 .058 .468 .759 .347 8.99 5.26 372641792 .267 .584 .175 .234 .103 .787 .117 .219 .084 .019 8.78 5.17 339726336 4 .163 .552 .199 .130 .063 .074 1 .733 .069 .128 .050 .009
list-properties/list_search_false-unreach-call.i 8.62 4.94 359407616 1 .820 .056 18.4  9.60 479256576 4 1.24  .005 .495 .792 .772 .220 8.33 4.78 371146752 .028 .294 .180 .007 .00  .803 .002 .00  .00  7.85 4.55 336826368 0 .035 .325 .187 .005 .00  .00  .715 .001 .00  .00 
list-properties/simple_false-unreach-call.i 9.29 5.53 350142464 2 .968 .014 .031 15.2  8.40 405233664 2 1.02  .005 .030 .034 .614 .890 8.04 4.62 365576192 .218 .511 .188 .196 .118 .538 .134 .189 .099 .019 8.49 4.88 331706368 2 .101 .455 .204 .084 .046 .038 0 .667 .047 .079 .036 .008
list-properties/splice_false-unreach-call.i 10.4  6.23 354881536 2 1.08  .018 .026 36.8  19.4  843362304 2 .983 .010 .039 .049 2.37  9.76  904    890    1095319552 880     881     .554 880     857     2.68  876     880     5.66  852     910    902    839090176 518 1.77  890     .946 1.71  8.65  886     41 8.01  1.34  1.70  1.01  .266
list-properties/alternating_list_true-unreach-call.i 906    895    1304748032 15 3.00  25.7   859     919    890    1948508160 16 3.02  .007 30.0   834     3.85  10.2   902    892    1063636992 887     887     .382 887     860     1.82  886     887     1.16  859     902    894    789917696 267 .794 868     .845 .751 20.9   865     7 23.4   .575 .741 .428 .115
list-properties/list_flag_true-unreach-call.i 907    893    1697857536 16 4.08  109     771     917    888    2014498816 15 3.23  .009 37.8   822     5.31  10.7   902    890    930439168 885     886     .404 885     874     1.01  883     885     4.13  870     902    893    814592000 279 4.88  890     .580 4.41  4.41  884     22 .114 4.08  4.40  3.34  .709
list-properties/list_search_true-unreach-call.i 10.2  5.62 376107008 1 1.13  .039 50.1  26.6  1027362816 5 6.70  .009 3.40  .633 8.85  1.26  8.49 4.83 375275520 .030 .755 .626 .006 .00  .313 .001 .00  .00  9.15 5.15 350048256 0 .041 .345 .203 .003 .00  .003 .854 .003 .00  .00 
list-properties/list_true-unreach-call.i 912    884    3274166272 9 28.4   25.5   823     954    910    3899658240 8 17.6   .006 2.61  857     21.2   5.17  902    890    952967168 884     885     .532 884     873     1.07  882     884     5.07  868     913    905    802840576
list-properties/simple_built_from_end_true-unreach-call.i 906    896    2263982080 19 3.16  256     625     1000    984    2843885568 19 2.43  .011 248     605     3.29  12.8   902    892    848302080 887     888     .689 887     880     1.34  886     887     3.24  877     902    894    1081217024 468 .785 879     .345 .753 17.2   877     12 12.1   .575 .741 .496 .053
list-properties/simple_true-unreach-call.i 905    895    2183098368 18 3.16  232     649     903    886    2258878464 17 2.73  .009 114     741     2.66  12.4   902    891    979001344 886     887     .405 886     874     1.27  884     886     3.58  870     902    894    920940544 255 4.12  891     .554 4.08  4.99  886     20 .077 3.82  4.08  3.08  .712
list-properties/splice_true-unreach-call.i 923    888    5701148672 12 90.4   191     596     1000    929    5759049728 .005 902    892    1006088192 885     886     .449 885     862     2.22  884     885     1.55  861     907    899    778088448 329 1.25  893     .550 1.20  5.39  890     36 2.08  .914 1.18  .664 .186
ldv-regression/1_3.c_false-unreach-call.i 6.93 4.10 325648384 1 .159 .010 8.62 4.94 349384704 1 .320 .005 .021 6.81 3.99 335171584 .028 .219 .148 .014 .002 .126 .012 .002 .00  6.23 3.63 304717824 0 .017 .234 .143 .002 .00  .001 .140 .001 .00  .00 
ldv-regression/alt_test.c_false-unreach-call.i 9.07 5.25 353132544 1 .818 .006 13.6  7.30 390230016 1 1.13  .005 .064 8.35 4.75 362860544 .051 .324 .124 .031 .007 .547 .017 .030 .007 .00  8.56 4.84 338272256 0 .543 .822 .137 .523 .013 .00  .183 .015 .519 .013 .00 
ldv-regression/callfpointer.c_false-unreach-call.i 6.09 3.53 285114368 1 .079 .001 7.84 4.38 337993728 1 .171 .015 .009 4.88 2.92 241758208 .015 .115 .051 .002 .00  .053 .00  .00  .00  5.35 3.10 234954752 0 .008 .118 .081 .001 .00  .00  .062 .00  .00  .00 
ldv-regression/fo_test.c_false-unreach-call.i 7.96 4.52 336199680 1 .669 .004 12.7  6.72 383504384 1 .431 .007 .029 7.58 4.36 356032512 .012 .161 .083 .002 .00  .659 .001 .00  .00  7.64 4.33 319545344 0 .009 .211 .090 .002 .00  .00  .107 .00  .00  .00 
ldv-regression/mutex_lock_int.c_false-unreach-call.i 6.65 3.87 318447616 1 .116 .004 8.13 4.59 332312576 1 .290 .006 .021 6.05 3.52 332185600 .024 .159 .089 .010 .001 .114 .009 .001 .00  5.26 3.12 240185344 0 .016 .176 .120 .003 .00  .003 .106 .001 .00  .00 
ldv-regression/mutex_lock_struct.c_false-unreach-call.i 6.07 3.53 315338752 1 .120 .005 8.28 4.61 342355968 1 .235 .006 .006 6.23 3.62 331403264 .018 .151 .103 .011 .001 .098 .010 .001 .00  6.30 3.61 290930688 0 .012 .151 .097 .004 .00  .001 .103 .002 .00  .00 
ldv-regression/recursive_list.c_false-unreach-call.i 6.87 4.02 316170240 1 .189 .018 8.92 5.09 353988608 1 .475 .008 .010 6.77 3.93 347529216 .024 .200 .146 .004 .00  .147 .001 .00  .00  6.63 3.81 306798592 0 .015 .183 .113 .002 .00  .001 .166 .001 .00  .00 
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i 7.14 4.10 320397312 1 .656 .033 10.2  5.47 350490624 1 .405 1.01  .059 6.68 3.87 343175168 .020 .249 .151 .002 .00  .481 .00  .00  .00  7.01 3.99 317083648 0 .031 .214 .120 .002 .00  .00  .156 .001 .00  .00 
ldv-regression/rule60_list2.c_false-unreach-call_1.i 9.14 5.36 363061248 1 .891 .017 21.7  11.2  477933568 1 .752 1.62  .096 7.90 4.48 358162432 .080 .751 .144 .056 .027 .273 .054 .027 .00  7.52 4.29 321675264 0 .028 .364 .192 .004 .00  .001 .683 .00  .00  .00 
ldv-regression/stateful_check_false-unreach-call.i 8.03 4.53 337219584 4 .881 .050 .039 27.8  14.3  668270592 4 1.29  2.29  .727 .278 1.97  1.09  8.14 4.64 365740032 .304 .751 .184 .253 .075 .580 .110 .241 .054 .021 7.61 4.38 327557120 6 .189 .663 .163 .142 .058 .153 0 .283 .049 .132 .034 .002
ldv-regression/test_while_int.c_false-unreach-call.i 6.16 3.61 292646912 3 .114 .001 .00  8.59 4.76 344993792 3 .289 .007 .013 .002 .292 .047 6.55 3.80 323858432 .086 .235 .075 .051 .005 .114 .012 .047 .005 .00  5.54 3.25 240730112 3 .023 .178 .079 .006 .005 .024 0 .105 .002 .00  .00 
ldv-regression/test_while_int.c_false-unreach-call_1.i 6.51 3.79 298979328 3 .110 .001 .00  8.38 4.64 337551360 3 .226 .008 .00  .001 .236 .064 6.27 3.69 335355904 .091 .204 .071 .055 .006 .101 .015 .051 .005 .001 5.57 3.23 243421184 3 .035 .165 .070 .020 .010 .021 0 .095 .005 .017 .002 .00 
ldv-regression/alias_of_return.c_true-unreach-call.i 5.14 2.99 222052352 1 .116 .00  .001 7.15 3.98 303362048 1 .240 .503 .00  .001 4.99 2.93 223260672 .024 .154 .102 .011 .001 .044 .008 .001 .00  4.86 2.81 214253568 0 .014 .182 .123 .001 .00  .00  .047 .00  .00  .00 
ldv-regression/alias_of_return.c_true-unreach-call_1.i 5.27 3.04 220348416 1 .117 .00  .001 7.26 4.01 300752896 1 .293 .005 .00  .001 4.93 2.90 220983296 .024 .133 .088 .009 .001 .037 .008 .001 .00  4.96 2.90 208007168 0 .010 .141 .111 .003 .00  .00  .037 .00  .00  .00 
ldv-regression/alias_of_return_2.c_true-unreach-call.i 5.04 2.94 222113792 1 .145 .00  .003 7.04 3.92 305713152 1 .312 .005 .00  .006 5.36 3.12 224579584 .050 .190 .098 .014 .003 .044 .011 .003 .00  5.32 3.06 216326144 0 .016 .157 .086 .003 .00  .00  .048 .00  .00  .00 
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i 5.02 2.93 214933504 1 .116 .00  .001 6.99 3.85 312614912 1 .253 .005 .00  .001 5.17 3.01 216219648 .018 .140 .085 .009 .00  .041 .008 .00  .00  5.04 2.92 211296256 0 .007 .138 .106 .002 .00  .00  .036 .001 .00  .00 
ldv-regression/ex3_forlist.c_true-unreach-call.i 6.57 3.74 282873856 6 .288 .046 .00  29.4  15.9  652824576 6 .414 .011 .061 .002 5.64  5.57  902    894    460513280 889     890     .411 889     888     .736 888     889     1.48  886     9.78 5.92 310722560 20 .805 1.74  .373 .345 .583 .317 4 1.17  .275 .336 .227 .033
ldv-regression/just_assert.c_true-unreach-call.i 4.49 2.54 207622144 1 6.50 3.61 299753472 1 .358 4.94 2.82 219918336 .005 .054 .038 .001 .00  4.86 2.80 207233024 0 .004 .054 .034 .00  .00  .001
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i 4.94 2.88 214671360 1 .123 .00  .005 7.68 4.29 318119936 1 .336 .612 .00  .009 4.97 2.93 223674368 .028 .170 .095 .014 .001 .049 .012 .001 .00  5.48 3.13 215560192 0 .021 .170 .107 .003 .00  .00  .046 .001 .00  .00 
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i 5.23 3.03 216035328 1 .126 .00  .003 6.62 3.70 306126848 1 .288 .009 .00  .005 5.14 3.00 219471872 .046 .183 .107 .014 .001 .049 .013 .001 .00  5.16 2.94 210722816 0 .010 .169 .121 .002 .00  .00  .047 .001 .00  .00 
ldv-regression/nested_structure.c_true-unreach-call.i 5.07 2.98 219512832 1 .127 .00  .002 6.56 3.64 312582144 1 .091 .005 5.08 2.96 221188096 .021 .168 .114 .012 .002 .048 .010 .002 .00  4.85 2.84 209776640 0 .011 .141 .102 .002 .00  .00  .044 .001 .00  .00 
ldv-regression/nested_structure_noptr.c_true-unreach-call.i 5.04 2.91 218660864 1 .074 .00  .00  6.49 3.61 299134976 1 .112 .017 5.12 2.97 222314496 .023 .111 .065 .008 .00  .046 .006 .00  .00  4.95 2.87 209973248 0 .009 .101 .068 .001 .00  .001 .045 .001 .00  .00 
ldv-regression/nested_structure_noptr_true-unreach-call.i 5.07 2.94 214274048 1 .078 .00  .00  6.81 3.78 298455040 1 .126 .015 5.03 2.93 219955200 .030 .137 .060 .014 .001 .030 .007 .013 .001 .00  4.84 2.83 203411456 0 .018 .129 .061 .012 .001 .00  .038 .002 .011 .001 .00 
ldv-regression/nested_structure_ptr.c_true-unreach-call.i 5.18 2.97 218984448 1 .127 .00  .002 6.30 3.51 301535232 1 .062 .015 5.12 3.04 221159424 .025 .137 .088 .012 .002 .052 .011 .002 .00  4.99 2.86 210788352 0 .013 .170 .123 .003 .00  .00  .050 .001 .00  .00 
ldv-regression/nested_structure_ptr_true-unreach-call.i 5.19 3.03 217051136 1 .141 .00  .002 6.71 3.71 319119360 1 .122 .005 5.03 2.93 221339648 .030 .176 .101 .021 .002 .036 .009 .021 .002 .00  5.51 3.16 211009536 0 .023 .172 .112 .016 .004 .00  .034 .006 .015 .004 .00 
ldv-regression/nested_structure_true-unreach-call.i 4.99 2.92 217509888 1 .124 .00  .001 7.25 4.15 295788544 1 .004 5.67 3.26 228528128 .034 .176 .095 .027 .002 .037 .010 .025 .002 .00  5.25 3.02 216477696 0 .031 .179 .099 .026 .002 .00  .035 .003 .013 .002 .00 
ldv-regression/oomInt.c_true-unreach-call.i 5.00 2.89 213155840 1 .079 .00  .00  6.64 3.66 303263744 1 .117 .006 .00  .00  5.00 2.95 226144256 .038 .153 .068 .020 .001 .031 .008 .017 .001 .00  5.33 3.05 212512768 0 .033 .137 .055 .015 .001 .00  .037 .003 .013 .001 .00 
ldv-regression/oomInt.c_true-unreach-call_1.i 5.31 3.04 219049984 1 .071 .00  .00  6.38 3.52 303947776 1 .090 .014 .00  .001 5.01 2.90 225009664 .035 .135 .058 .023 .002 .032 .008 .018 .002 .00  5.34 3.06 213221376 0 .038 .159 .065 .013 .002 .00  .034 .003 .013 .002 .00 
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i 6.79 3.80 283009024 1 .666 .00  .023 8.65 4.75 331317248 1 .704 .722 .00  .064 7.07 3.96 313647104 .072 .343 .153 .049 .013 .493 .020 .046 .013 .00  5.84 3.32 223346688 0 .064 .379 .181 .037 .013 .004 .055 .015 .034 .013 .00 
ldv-regression/rule60_list.c_true-unreach-call.i 7.48 4.17 300376064 1 .782 .00  .016 8.73 4.74 328273920 1 .708 .708 .00  .179 7.33 4.11 320901120 .482 .739 .125 .466 .012 .076 .463 .012 .00  6.82 3.86 290869248 0 .019 .250 .138 .002 .00  .00  .075 .001 .00  .00 
ldv-regression/rule60_list2.c_true-unreach-call.i 7.45 4.18 301936640 1 .937 .00  .014 8.59 4.66 320380928 1 .496 .013 7.21 4.07 323239936 .084 .763 .125 .052 .024 .099 .050 .024 .00  7.33 4.06 284057600 0 .024 .340 .157 .002 .00  .00  .087 .00  .00  .00 
ldv-regression/sizeofparameters_test.c_true-unreach-call.i 6.58 3.69 293724160 1 .212 .001 .00  7.44 4.10 306847744 1 .231 .006 6.53 3.73 316854272 .030 .178 .078 .020 .001 .039 .012 .020 .001 .00  5.69 3.23 222670848 0 .031 .197 .062 .020 .001 .00  .028 .003 .011 .001 .00 
ldv-regression/structure_assignment.c_true-unreach-call.i 4.77 2.78 216023040 1 .094 .00  .00  6.62 3.67 306585600 1 .151 .006 .00  .00  5.02 2.91 219942912 .019 .106 .061 .007 .00  .047 .006 .00  .00  5.08 2.93 211259392 0 .014 .119 .085 .002 .00  .001 .045 .002 .00  .00 
ldv-regression/test_address.c_true-unreach-call.i 7.02 3.94 293548032 1 .707 .00  .00  9.27 5.07 316489728 1 .778 .757 .00  .00  6.70 3.73 314060800 .022 .201 .098 .008 .00  .041 .007 .00  .00  5.83 3.32 223195136 0 .012 .187 .116 .004 .00  .00  .045 .001 .00  .00 
ldv-regression/test_cut_trace.c_true-unreach-call.i 4.92 2.90 215572480 1 .080 .00  .001 6.47 3.59 301174784 1 .100 .006 4.96 2.93 217194496 .028 .111 .056 .007 .00  .061 .006 .00  .00  4.92 2.86 207548416 0 .014 .107 .061 .003 .00  .00  .051 .001 .00  .00 
ldv-regression/test_malloc-1_true-unreach-call.i 6.93 3.93 290717696 1 .748 .00  .008 9.25 4.99 348405760 1 .695 .715 .00  .024 6.58 3.75 317939712 .039 .579 .091 .024 .007 .034 .014 .024 .007 .00  5.69 3.22 223969280 0 .047 .267 .118 .022 .007 .00  .033 .008 .020 .007 .00 
ldv-regression/test_malloc-2_true-unreach-call.i 7.00 4.01 289533952 1 .644 .00  .009 9.11 4.97 324661248 1 .770 .005 .00  .034 6.56 3.73 318722048 .033 .574 .084 .025 .007 .036 .015 .023 .007 .00  5.70 3.27 226832384 0 .030 .246 .114 .020 .008 .00  .033 .010 .018 .008 .00 
ldv-regression/test_overflow.c_true-unreach-call.i 7.75 4.25 307437568 1 .721 .00  .00  8.02 4.38 315899904 1 .187 .008 7.41 4.16 324681728 .042 .227 .089 .032 .008 .033 .020 .031 .008 .00  6.33 3.51 230064128 0 .018 .236 .107 .011 .001 .00  .030 .003 .010 .001 .00 
ldv-regression/test_union.c_true-unreach-call.i 5.19 2.97 217419776 1 .066 .00  .00  6.57 3.67 311685120 1 .123 .011 .00  .00  4.98 2.90 217882624 .015 .096 .050 .009 .00  .051 .006 .00  .00  4.80 2.75 204726272 0 .015 .090 .052 .002 .00  .00  .063 .001 .00  .00 
ldv-regression/test_union.c_true-unreach-call_1.i 5.06 2.92 213839872 1 .079 .00  .00  6.80 3.76 304070656 1 .128 .488 .00  .00  5.23 3.09 249802752 .009 .065 .046 .001 .00  .056 .001 .00  .00  5.27 3.06 236916736 0 .007 .076 .044 .002 .00  .00  .074 .001 .00  .00 
ldv-regression/test_union_cast-1_true-unreach-call.i 5.14 2.93 217272320 1 .068 .00  .00  6.23 3.41 296452096 1 .144 .008 5.03 2.94 223690752 .025 .123 .059 .017 .00  .039 .007 .016 .00  .00  4.99 2.88 210214912 0 .021 .132 .069 .011 .001 .005 .049 .003 .010 .001 .00 
ldv-regression/test_union_cast-2_true-unreach-call.i 4.90 2.88 223232000 1 .102 .00  .010 6.46 3.60 293081088 1 .164 .012 5.25 3.07 230481920 .040 .141 .064 .030 .010 .040 .017 .030 .010 .00  5.20 3.02 217886720 0 .044 .197 .114 .030 .008 .012 .040 .010 .022 .008 .00 
ldv-regression/test_union_cast.c_true-unreach-call.i 5.29 3.05 216358912 1 .110 .00  .009 6.13 3.44 306085888 1 .074 .010 5.27 3.09 225947648 .026 .145 .080 .019 .007 .060 .016 .007 .00  5.12 2.96 212946944 0 .008 .123 .091 .001 .00  .001 .058 .001 .00  .00 
ldv-regression/test_union_cast.c_true-unreach-call_1.i 5.26 3.06 217497600 1 .072 .00  .00  6.63 3.67 298979328 1 .085 .007 5.15 3.05 218599424 .015 .101 .059 .007 .001 .045 .006 .001 .00  5.05 2.93 212717568 0 .010 .110 .071 .003 .00  .001 .032 .00  .00  .00 
ldv-regression/volatile_alias.c_true-unreach-call.i 5.11 2.93 220057600 1 .103 .00  .001 6.61 3.66 299167744 1 .154 .441 .00  .002 5.21 2.98 228089856 .034 .166 .107 .020 .002 .046 .008 .019 .002 .00  5.02 2.92 207847424 0 .021 .175 .133 .014 .002 .00  .031 .004 .013 .002 .00 
ldv-regression/volatile_alias.c_true-unreach-call_1.i 5.14 2.98 214966272 1 .110 .00  .001 6.65 3.70 311418880 1 .226 .468 .00  .003 5.25 3.02 224854016 .037 .142 .090 .021 .001 .032 .009 .019 .001 .00  5.21 2.98 210735104 0 .017 .149 .110 .011 .001 .00  .034 .003 .011 .001 .00 
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i 23.8  12.8  525156352 11 2.03  .949 .152 902    771    7573921792 5 3.26  .006 .709 .002 620     133     26.3  15.9  532942848 5.13  6.78  1.15  5.02  3.98  2.39  3.99  4.99  2.41  1.57  22.9  13.5  513548288 57 .451 5.43  1.28  .387 .384 2.86  1 2.80  .232 .370 .222 .004
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i 22.2  11.9  514420736 11 2.08  1.20  .096 932    797    7539605504 6 2.95  .003 .737 .00  639     142     25.3  15.0  522768384 4.85  6.51  1.14  4.76  3.76  2.27  3.75  4.72  2.31  1.45  22.3  13.1  489627648 56 .264 4.85  1.34  .185 .147 2.80  0 2.52  .089 .182 .080 .003
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i 21.9  11.9  519303168 11 1.70  1.01  .090 937    800    7624826880 5 2.78  .006 .668 .00  646     138     22.8  14.1  525000704 4.49  6.00  1.08  4.43  3.56  2.21  3.57  4.40  2.18  1.38  23.2  13.6  503234560 56 .369 5.01  1.31  .302 .238 2.93  0 2.83  .177 .300 .170 .001
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i 10.7  5.80 391868416 1 15.0  7.91 456908800 1 .915 15.7  8.34 448700416 .138 2.50  1.43  .022 .00  .004 .00  .00  16.3  8.60 442228736 0 .295 3.44  1.46  .037 .00  .019 .003 .00  .00 
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i 10.6  5.73 391188480 1 16.2  8.60 460615680 1 1.10  16.3  8.68 453853184 .177 2.73  1.51  .038 .00  .003 .00  .00  14.3  7.71 422969344 0 .169 2.69  1.24  .021 .00  .005 .001 .00  .00 
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i 10.6  5.76 389775360 1 15.5  8.17 457330688 1 .915 16.1  8.53 465805312 .190 2.76  1.53  .033 .00  .002 .00  .00  16.1  8.49 437280768 0 .665 3.31  1.51  .071 .00  .013 .00  .00  .00 
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i 10.6  5.71 388583424 1 14.1  7.47 451698688 1 .772 14.5  7.77 443301888 .142 2.15  1.27  .027 .00  .001 .00  .00  14.7  7.80 433893376 0 .222 2.87  1.32  .046 .00  .026 .00  .00  .00 
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i 11.0  5.96 387915776 1 15.3  8.08 450756608 1 .930 18.1  9.54 465625088 .286 3.37  1.76  .038 .00  .002 .00  .00  15.4  8.19 434278400 0 .221 3.11  1.34  .046 .00  .032 .001 .00  .00 
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i 10.7  5.79 387772416 1 15.0  7.88 451887104 1 .952 16.0  8.44 458387456 .230 3.01  1.53  .029 .00  .003 .00  .00  16.4  8.68 440614912 0 .510 3.33  1.53  .017 .00  .023 .001 .00  .00 
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i 10.9  5.88 393531392 1 15.1  7.93 445390848 1 .841 15.6  8.34 454176768 .193 2.60  1.42  .030 .00  .001 .00  .00  15.3  8.08 443416576 0 .203 3.31  1.40  .054 .00  .028 .034 .00  .00 
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i 10.8  5.85 399249408 1 15.3  8.03 462725120 1 .986 16.1  8.57 465485824 .199 3.05  1.63  .030 .00  .001 .00  .00  15.1  8.01 426209280 0 .177 2.90  1.28  .030 .00  .013 .003 .00  .00 
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i 10.6  5.81 388734976 1 14.5  7.72 452435968 1 .004 15.4  8.21 462307328 .230 2.83  1.50  .054 .00  .001 .00  .00  16.5  8.66 436019200 0 .327 3.19  1.65  .042 .00  .015 .001 .00  .00 
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i 11.0  5.93 397668352 1 15.8  8.31 461729792 1 .950 15.1  8.03 462610432 .192 2.62  1.46  .025 .00  .006 .00  .00  16.5  8.72 443396096 0 .674 3.68  1.77  .044 .00  .017 .013 .00  .00 
floats-cdfpl/newton_1_4_false-unreach-call.i 101    98.1  544468992 1 .111 5.39  111    106    588111872 1 .233 .008 6.17  172    169    810811392 .013 .149 .087 .003 .00  146     .00  .00  .00  151    148    803270656 0 .011 .139 .084 .001 .00  .00  127     .001 .00  .00 
floats-cdfpl/newton_1_5_false-unreach-call.i 171    167    549654528 1 .111 4.52  177    172    588316672 1 .194 .005 5.31  45.2  42.4  776343552 .019 .129 .074 .001 .00  27.9   .001 .00  .00  43.0  40.7  695975936 0 .024 .151 .071 .002 .00  .001 26.8   .001 .00  .00 
floats-cdfpl/newton_1_6_false-unreach-call.i 67.6  64.6  524525568 1 .112 29.8   71.4  67.3  556376064 1 .199 .005 30.9   910    905    14136164352 .012 .119 .076 .003 .00  902     .002 .00  .00  910    906    13768282112 0 .014 .162 .108 .002 .00  .00  902     .001 .00  .00 
floats-cdfpl/newton_1_7_false-unreach-call.i 75.3  72.4  525754368 1 .114 21.6   76.1  71.6  561704960 1 .242 .009 21.2   457    453    6103810048 .011 .124 .079 .003 .00  438     .001 .00  .00  425    421    6018973696 0 .022 .148 .082 .002 .00  .00  407     .001 .00  .00 
floats-cdfpl/newton_1_8_false-unreach-call.i 56.6  53.6  505962496 1 .111 5.86  59.0  54.6  549056512 1 .290 .005 6.57  42.7  39.7  524685312 .012 .149 .083 .003 .00  18.3   .002 .00  .00  38.2  35.7  552419328 0 .009 .144 .068 .002 .00  .001 16.7   .001 .00  .00 
floats-cdfpl/newton_2_6_false-unreach-call.i 394    390    765804544 1 .140 329     392    387    815443968 1 .233 .006 328     911    907    14765613056 .020 .157 .087 .002 .00  903     .00  .00  .00  911    907    14412693504 0 .025 .168 .094 .004 .00  .00  903     .001 .00  .00 
floats-cdfpl/newton_2_7_false-unreach-call.i 315    312    817139712 1 .138 102     289    284    853225472 1 .345 .013 91.8   909    905    12300140544 .021 .170 .107 .001 .00  901     .00  .00  .00  909    904    12253351936 0 .033 .164 .085 .013 .00  .00  901     .001 .00  .00 
floats-cdfpl/newton_2_8_false-unreach-call.i 120    117    741691392 1 .132 12.9   130    125    782159872 1 .205 .011 15.2   185    181    1223512064 .018 .160 .091 .002 .00  107     .001 .00  .00  168    165    1120907264 0 .018 .178 .102 .002 .00  .00  98.6   .00  .00  .00 
floats-cdfpl/newton_3_6_false-unreach-call.i 902    898    618659840 1 .146 894     903    895    731680768 1 .313 .006 891     908    903    10268987392 .021 .186 .111 .002 .00  900     .00  .00  .00  908    903    9789673472 0 .020 .189 .111 .001 .00  .00  900     .001 .00  .00 
floats-cdfpl/newton_3_7_false-unreach-call.i 984    978    1199562752 1 .156 7.78  972    965    1226461184 1 .237 .010 8.48  902    897    10023272448 .015 .175 .103 .003 .00  894     .001 .00  .00  902    898    10008207360 0 .025 .196 .088 .004 .00  .001 895     .001 .00  .00 
floats-cdfpl/newton_3_8_false-unreach-call.i 809    804    1201577984 1 .150 217     784    777    1236144128 1 .309 .005 207     909    904    10237014016 .020 .158 .096 .003 .00  900     .00  .00  .00  909    904    11497967616 0 .023 .182 .100 .004 .00  .00  901     .00  .00  .00 
floats-cdfpl/sine_1_false-unreach-call.i 224    221    456134656 1 .103 197     82.3  78.3  523935744 1 .184 .006 10.6   396    393    7190036480 .010 .123 .071 .001 .00  388     .001 .00  .00  410    406    7178952704 0 .009 .149 .096 .002 .00  .001 401     .001 .00  .00 
floats-cdfpl/sine_2_false-unreach-call.i 309    306    549953536 1 .111 4.88  19.7  16.0  473575424 1 .168 .005 3.92  220    217    4418318336 .007 .105 .063 .002 .00  208     .001 .00  .00  228    225    4410101760 0 .015 .121 .061 .002 .00  .00  216     .001 .00  .00 
floats-cdfpl/sine_3_false-unreach-call.i 364    361    566857728 1 .100 2.69  103    98.7  508592128 1 .202 .008 6.82  243    240    4856336384 .007 .117 .066 .002 .00  236     .001 .00  .00  272    269    4848197632 0 .008 .073 .037 .002 .00  .00  265     .001 .00  .00 
floats-cdfpl/square_1_false-unreach-call.i 56.1  53.3  420909056 1 .107 30.9   83.6  79.7  530104320 1 .281 .007 53.5   278    274    3188379648 .007 .123 .078 .003 .00  258     .002 .00  .00  203    200    3171082240 0 .009 .117 .071 .002 .00  .00  188     .001 .00  .00 
floats-cdfpl/square_2_false-unreach-call.i 84.4  81.5  491241472 1 .109 23.8   81.5  77.7  516362240 1 .192 .014 15.7   75.4  73.1  754536448 .008 .116 .087 .002 .00  63.0   .001 .00  .00  76.0  73.6  745869312 0 .012 .119 .080 .003 .00  .001 63.3   .001 .00  .00 
floats-cdfpl/square_3_false-unreach-call.i 114    111    475205632 1 .107 57.1   62.0  58.3  505470976 1 .202 .018 27.5   71.2  68.6  423370752 .010 .121 .056 .001 .00  47.2   .001 .00  .00  64.1  61.8  406450176 0 .012 .109 .069 .003 .00  .00  43.1   .002 .00  .00 
floats-cdfpl/newton_1_1_true-unreach-call.i 902    898    538701824 1 .107 895     902    896    647254016 1 .178 .004 892     910    906    14409367552 .012 .138 .078 .003 .00  902     .001 .00  .00  910    906    13829947392 0 .038 .152 .077 .002 .00  .002 902     .00  .00  .00 
floats-cdfpl/newton_1_2_true-unreach-call.i 902    898    528506880 1 .119 895     902    896    641081344 1 .204 .020 892     910    906    12720664576 .015 .121 .076 .001 .00  903     .001 .00  .00  909    905    12285673472 0 .015 .143 .068 .001 .00  .00  902     .001 .00  .00 
floats-cdfpl/newton_1_3_true-unreach-call.i 902    898    529149952 1 .106 895     902    896    633098240 1 .197 .004 892     910    906    14214103040 .010 .115 .060 .002 .00  902     .001 .00  .00  910    906    13899763712 0 .025 .146 .060 .002 .00  .00  902     .001 .00  .00 
floats-cdfpl/newton_2_1_true-unreach-call.i 902    897    525062144 1 .134 894     902    896    643805184 1 .278 .005 892     911    906    13625421824 .021 .147 .086 .002 .00  903     .001 .00  .00  911    906    14590103552 0 .013 .184 .102 .001 .00  .001 902     .001 .00  .00 
floats-cdfpl/newton_2_2_true-unreach-call.i 902    898    679989248 1 .134 895     903    895    798625792 1 .353 .010 891     911    906    14558150656 .024 .135 .076 .002 .00  903     .001 .00  .00  911    906    13931155456 0 .022 .172 .093 .003 .00  .00  903     .001 .00  .00 
floats-cdfpl/newton_2_3_true-unreach-call.i 902    898    671047680 1 .122 895     902    896    770252800 1 .204 .005 892     868    864    14999998464 878    874    14999998464
floats-cdfpl/newton_2_4_true-unreach-call.i 902    897    579112960 1 .141 894     902    895    682446848 1 .242 .005 892     911    907    14769876992 .013 .152 .089 .001 .00  903     .001 .00  .00  911    907    14517776384 0 .013 .168 .081 .002 .00  .001 903     .001 .00  .00 
floats-cdfpl/newton_2_5_true-unreach-call.i 902    898    569249792 1 .127 895     902    896    666808320 1 .200 .006 892     913    908    14411255808 912    907    14845575168 0 .014 .150 .074 .002 .00  .00  904     .001 .00  .00 
floats-cdfpl/newton_3_1_true-unreach-call.i 902    898    684789760 1 .150 895     903    895    794157056 1 .286 .008 892     843    838    14999998464 852    848    14999998464
floats-cdfpl/newton_3_2_true-unreach-call.i 902    898    656375808 1 .139 894     903    895    763670528 1 .305 .006 891     910    906    13933694976 .016 .184 .113 .002 .00  902     .00  .00  .00  910    906    14085378048 0 .018 .206 .123 .001 .00  .001 902     .00  .00  .00 
floats-cdfpl/newton_3_3_true-unreach-call.i 902    897    677576704 1 .154 894     903    895    792219648 1 .199 .017 891     883    879    14999998464 911    906    14898487296 0 .013 .194 .112 .002 .00  .003 903     .001 .00  .00 
floats-cdfpl/newton_3_4_true-unreach-call.i 902    897    704122880 1 .152 894     903    896    822640640 1 .258 .011 892     910    905    12587421696 .027 .170 .103 .003 .00  902     .00  .00  .00  909    905    12800274432 0 .011 .176 .105 .003 .00  .001 902     .001 .00  .00 
floats-cdfpl/newton_3_5_true-unreach-call.i 902    898    686948352 1 .138 895     903    895    810999808 1 .400 .005 891     911    906    14412431360 .035 .169 .083 .001 .00  903     .001 .00  .00  911    906    14225354752 0 .012 .183 .101 .003 .00  .00  903     .001 .00  .00 
floats-cdfpl/sine_4_true-unreach-call.i 902    897    500084736 1 .097 894     902    896    617365504 1 .189 .004 892     635    631    14999998464 732    728    14999998464
floats-cdfpl/sine_5_true-unreach-call.i 902    897    466710528 1 .108 894     902    896    489074688 1 .174 .010 893     768    763    14999998464 732    729    14999998464
floats-cdfpl/sine_6_true-unreach-call.i 196    193    353603584 1 .100 .00  190     519    514    478429184 1 .216 .006 .001 509     902    897    6862270464 537     537     .051 537     537     357     537     537     537     .00  902    897    6844710912 0 555     555     .090 555     555     .00  339     555     555     555     .00 
floats-cdfpl/sine_7_true-unreach-call.i 902    897    499834880 1 .100 894     902    896    495316992 1 .253 .005 893     902    897    4908314624 641     641     .078 641     641     253     641     641     641     .00  902    897    4900376576 0 677     677     .077 677     677     .00  218     677     677     677     .00 
floats-cdfpl/sine_8_true-unreach-call.i 902    897    434028544 1 .103 894     902    896    534360064 1 .189 .017 893     728    724    14999998464 738    734    14999998464
floats-cdfpl/square_4_true-unreach-call.i 902    897    540983296 1 .120 894     635    630    523935744 1 .146 .011 .00  624     896    892    14999998464 825    821    14999998464
floats-cdfpl/square_5_true-unreach-call.i 902    897    486940672 1 .108 894     902    896    600002560 1 .197 .022 892     848    844    14999998464 858    854    14999998464
floats-cdfpl/square_6_true-unreach-call.i 345    342    404242432 1 .110 .00  338     545    540    529575936 1 .174 .014 .00  535     902    897    12669632512 237     237     .048 237     237     658     237     237     237     .00  902    897    12661243904 0 216     216     .082 216     216     .001 678     216     216     216     .00 
floats-cdfpl/square_7_true-unreach-call.i 902    897    478400512 1 .111 894     588    583    583217152 1 .185 .010 .001 578     631    628    5397585920 310     310     .094 310     310     315     310     310     310     .00  637    633    5386371072 0 317     317     .092 317     317     .001 314     317     317     317     .00 
floats-cdfpl/square_8_true-unreach-call.i 14.0  11.8  285593600 1 .113 .001 8.67  58.4  54.9  406446080 1 .236 .011 .00  51.1   91.6  89.1  1289232384 23.1   23.2   .072 23.1   23.0   63.0   23.0   23.1   23.0   .00  97.9  95.5  1280032768 0 25.4   25.5   .081 25.4   25.3   .001 67.2   25.3   25.4   25.3   .00 
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 243    238    790953984 205    183    2680135680 1 2.14  .014 16.4   16.7  11.9  468082688 4.47  4.86  .217 4.45  3.66  2.23  4.09  4.43  3.66  .006 17.1  12.1  437891072 0 4.57  5.03  .241 4.53  3.69  .001 2.37  3.71  4.53  3.69  .005
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 4.88 2.90 217112576 1 .076 .00  .00  7.09 3.94 310530048 1 .135 .493 .00  .001 4.84 2.78 217731072 .006 .083 .052 .001 .00  .032 .001 .00  .00  5.16 2.91 208855040 0 .005 .091 .070 .002 .00  .00  .026 .00  .00  .00 
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 20.6  16.8  347639808 1 .774 .001 12.4   20.3  14.0  523948032 1 .776 .006 .001 8.70  12.4  8.96 359325696 4.08  4.30  .101 4.06  3.48  1.06  3.50  4.06  3.48  .00  11.6  8.57 263753728 0 3.69  3.95  .139 3.67  3.59  .00  1.12  3.59  3.67  3.59  .00 
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 4.81 2.79 215146496 1 .058 .00  .00  6.57 3.63 313597952 1 .147 .008 .00  .001 4.92 2.86 225447936 .007 .077 .057 .001 .00  .037 .001 .00  .00  4.91 2.82 212967424 0 .008 .055 .030 .001 .00  .00  .024 .00  .00  .00 
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 8.34 4.59 316858368 1 .920 .00  .040 10.2  5.48 343412736 1 .992 .842 .00  .111 7.98 4.50 337145856 .237 .839 .484 .227 .135 .048 .147 .224 .135 .00  6.83 3.90 248033280 0 .214 .505 .166 .194 .100 .00  .043 .104 .191 .100 .00 
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 5.06 2.93 213065728 1 .094 .00  .00  6.96 3.81 306884608 1 .152 .005 .00  .00  5.80 3.62 262987776 .043 .150 .066 .030 .002 .688 .012 .029 .002 .00  5.90 3.60 248782848 0 .026 .157 .089 .011 .001 .00  .687 .003 .011 .001 .00 
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 4.98 2.92 212680704 1 .066 .00  .00  6.83 3.79 304693248 1 .128 .005 .00  .00  5.26 3.10 238788608 .025 .104 .064 .017 .001 .119 .008 .016 .001 .00  5.00 2.95 224063488 0 .017 .130 .085 .013 .001 .00  .106 .002 .012 .001 .00 
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 8.01 4.43 308043776 1 .748 .00  .00  9.66 5.18 337096704 1 .646 .686 .001 .00  7.78 4.35 333930496 .551 .738 .083 .543 .058 .080 .525 .541 .058 .00  6.80 3.83 245415936 0 .067 .317 .108 .062 .038 .00  .080 .039 .061 .038 .00 
floats-cbmc-regression/float-rounding1_true-unreach-call.i 8.14 4.48 305311744 1 .904 12.0  6.40 378392576 1 2.09  .012 6.31 3.45 239398912 .006 .130 .067 .001 .00  6.18 3.43 228442112 0 .012 .164 .072 .00  .00  .00 
floats-cbmc-regression/float-to-double1_true-unreach-call.i 8.27 4.78 359288832 1 .623 .069 12.1  6.53 408219648 1 .704 .007 .138 8.43 4.85 365854720 .008 .169 .070 .001 .00  .643 .00  .00  .00  8.34 4.79 341098496 0 .009 .147 .066 .002 .00  .00  .251 .001 .00  .00 
floats-cbmc-regression/float-to-double2_true-unreach-call.i 4.93 2.88 214077440 1 .056 .00  .00  6.27 3.46 295063552 1 .135 .511 .00  .00  5.14 3.06 251691008 .011 .075 .049 .004 .00  .060 .003 .00  .00  5.31 3.13 244977664 0 .015 .102 .069 .002 .00  .00  .062 .001 .00  .00 
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 5.33 3.11 216961024 1 .093 .00  .00  6.80 3.76 308273152 1 .119 .449 .00  .00  6.27 3.66 318410752 .010 .121 .065 .001 .00  .056 .00  .00  .00  5.35 3.13 236863488 0 .025 .129 .061 .004 .00  .001 .049 .001 .00  .00 
floats-cbmc-regression/float11_true-unreach-call.i 4.85 2.80 209489920 1 6.38 3.55 293421056 1 .012 4.99 2.90 220471296 .006 .035 .009 .00  .00  4.94 2.84 209362944 0 .004 .036 .012 .001 .00  .00 
floats-cbmc-regression/float12_true-unreach-call.i 5.03 2.94 226234368 1 .086 .00  .015 6.94 3.83 306778112 1 .189 .546 .00  .048 4.98 2.89 219967488 .007 .100 .079 .002 .00  .048 .00  .00  .00  5.09 2.93 207368192 0 .005 .111 .079 .002 .00  .00  .060 .001 .00  .00 
floats-cbmc-regression/float13_true-unreach-call.i 5.28 3.08 218148864 1 .102 .00  .00  6.47 3.61 306900992 1 .251 .005 .00  .00  5.32 3.04 221679616 .058 .163 .070 .048 .002 .050 .010 .046 .002 .00  5.24 3.02 211566592 0 .059 .168 .077 .041 .002 .00  .073 .005 .038 .002 .00 
floats-cbmc-regression/float14_true-unreach-call.i 8.00 4.42 309411840 1 .358 .00  .00  9.04 4.87 324943872 1 .648 .691 .00  .001 7.43 4.15 332816384 .031 .200 .073 .025 .001 .040 .011 .024 .001 .00  6.60 3.65 233402368 0 .027 .229 .084 .020 .002 .00  .045 .003 .019 .002 .00 
floats-cbmc-regression/float18_true-unreach-call.i 8.66 4.73 327827456 10 .904 .003 .00  58.9  29.8  1568251904 10 .926 19.9   .031 .00  .848 23.0   8.03 4.67 347975680 .418 .616 .096 .408 .362 .203 .366 .408 .346 .016 7.08 4.24 254074880 1 .409 .732 .079 .400 .340 .119 0 .197 .343 .398 .327 .012
floats-cbmc-regression/float19_true-unreach-call.i 7.64 4.28 311001088 1 .751 .00  .010 10.7  5.68 336969728 1 .928 .929 .00  .036 7.26 4.11 328818688 .473 .695 .078 .469 .013 .046 .451 .467 .013 .00  7.15 3.99 301965312 0 .049 .268 .089 .035 .015 .00  .043 .016 .033 .015 .00 
floats-cbmc-regression/float1_true-unreach-call.i 5.06 2.95 214319104 1 .079 .00  .00  6.63 3.68 305197056 1 .110 .019 .00  .001 5.14 2.94 220528640 .019 .106 .074 .002 .00  .027 .001 .00  .00  4.99 2.89 208527360 0 .006 .085 .058 .002 .00  .00  .048 .001 .00  .00 
floats-cbmc-regression/float20_true-unreach-call.i 5.17 2.98 216023040 1 .111 .00  .001 6.62 3.68 300146688 1 .175 .008 .00  .001 6.13 3.98 258068480 .439 .546 .072 .422 .375 .650 .035 .420 .375 .00  5.96 3.73 250646528 0 .057 .199 .092 .042 .028 .002 .665 .030 .041 .028 .00 
floats-cbmc-regression/float22_true-unreach-call.i 5.55 3.22 220651520 1 .219 .00  .006 7.40 4.07 307412992 1 .414 .575 .00  .008 6.78 3.87 350011392 .055 .243 .118 .030 .002 .156 .014 .029 .002 .00  6.64 3.74 317005824 0 .029 .225 .123 .012 .00  .002 .179 .002 .010 .00  .00 
floats-cbmc-regression/float2_true-unreach-call.i 4.90 2.87 221351936 1 .075 .00  .00  6.93 3.84 319602688 1 .133 .545 .00  .001 5.30 3.10 221356032 .041 .145 .085 .033 .001 .074 .012 .032 .001 .00  5.27 3.02 220811264 0 .032 .143 .079 .025 .003 .00  .065 .006 .024 .003 .00 
floats-cbmc-regression/float3_true-unreach-call.i 5.12 3.02 237334528 1 .105 .00  .201 7.59 4.14 334196736 1 .208 .011 .00  .495 5.36 3.28 235450368 .011 .146 .095 .002 .00  .241 .001 .00  .00  5.48 3.19 227106816 0 .013 .125 .073 .003 .00  .00  .242 .002 .00  .00 
floats-cbmc-regression/float4_true-unreach-call.i 52.9  49.0  389279744 1 .949 .00  44.3   69.8  61.8  712019968 1 .640 .009 .00  56.6   25.3  21.9  384581632 15.0   15.2   .122 15.0   14.3   3.17  14.4   15.0   14.3   .00  23.8  20.8  376094720 0 14.0   14.3   .133 14.0   13.7   .001 3.05  13.7   14.0   13.7   .00 
floats-cbmc-regression/float5_true-unreach-call.i 5.11 3.04 219856896 1 .110 .00  .055 7.30 4.03 318709760 1 .164 .602 .00  .143 5.30 3.12 231870464 .098 .218 .079 .078 .052 .107 .059 .077 .052 .00  5.18 3.05 221495296 0 .091 .235 .108 .076 .054 .00  .106 .055 .073 .054 .00 
floats-cbmc-regression/float6_true-unreach-call.i 5.26 3.04 223404032 7.23 3.95 315949056 5.42 3.23 233037824 .254 .384 .069 .236 .137 .040 .150 .235 .137 .00  5.42 3.19 218406912 0 .252 .421 .091 .231 .133 .001 .049 .140 .230 .133 .00 
floats-cbmc-regression/float7_true-unreach-call.i 6.14 3.52 330915840 1 .111 .009 6.37 3.54 301195264 1 .155 .453 .00  .00  5.52 3.24 252059648 .006 .124 .103 .001 .00  .074 .001 .00  .00  5.30 3.08 242135040 0 .007 .120 .095 .002 .00  .00  .072 .00  .00  .00 
floats-cbmc-regression/float8_true-unreach-call.i 9.07 5.45 311136256 1 .783 .00  1.01  12.1  6.71 390029312 1 .614 .005 .00  1.57  9.26 6.03 344150016 .899 1.09  .069 .892 .866 1.05  .874 .892 .866 .00  8.29 5.45 259686400 0 .915 1.11  .083 .901 .877 .00  1.09  .878 .898 .877 .00 
float-benchs/float_int_inv_square_false-unreach-call.c 6.69 3.94 342409216 1 .110 .081 8.47 4.81 364527616 1 .160 .004 .136 6.50 3.86 326287360 .007 .107 .069 .002 .00  .235 .001 .00  .00  5.43 3.30 259813376 0 .021 .102 .052 .002 .00  .00  .255 .001 .00  .00 
float-benchs/inv_square_false-unreach-call.c 6.64 3.98 324284416 1 .121 .073 8.45 4.72 370171904 1 .184 .008 .228 5.38 3.21 264855552 .009 .106 .065 .002 .00  .224 .001 .00  .00  5.44 3.26 258981888 0 .009 .123 .068 .003 .00  .00  .234 .001 .00  .00 
float-benchs/nan_double_false-unreach-call.c 6.27 3.64 296570880 1 .085 .011 7.21 4.00 344018944 1 .121 .011 .013 5.38 3.17 251318272 .017 .119 .078 .001 .00  .066 .001 .00  .00  5.26 3.08 245182464 0 .007 .087 .052 .001 .00  .00  .091 .001 .00  .00 
float-benchs/nan_float_false-unreach-call.c 6.09 3.57 299593728 1 .088 .011 7.24 4.06 336195584 1 .129 .007 .010 5.17 3.05 252133376 .015 .094 .054 .003 .00  .063 .001 .00  .00  5.18 3.07 236507136 0 .011 .109 .081 .002 .00  .001 .078 .001 .00  .00 
float-benchs/sin_interpolated_index_false-unreach-call.c 13.4  9.82 434425856 1 .910 2.26  28.5  16.5  612548608 1 .822 .009 7.51  7.30 4.39 362074112 .014 .107 .068 .003 .00  .500 .001 .00  .00  7.37 4.36 328073216 0 .022 .130 .081 .004 .00  .002 .477 .001 .00  .00 
float-benchs/inv_square_int_true-unreach-call.c 5.10 3.01 230760448 1 .103 .00  .091 7.45 4.11 311652352 1 .184 .609 .00  .258 5.73 3.30 232124416 .010 .120 .078 .002 .00  .127 .00  .00  .00  5.06 2.97 219521024 0 .010 .138 .072 .001 .00  .002 .125 .001 .00  .00 
float-benchs/inv_square_true-unreach-call.c 5.35 3.10 235450368 1 .114 .00  .085 7.08 3.89 325361664 1 .309 .619 .00  .196 5.91 3.49 244576256 .180 .329 .102 .164 .135 .134 .143 .160 .135 .00  5.20 3.10 221507584 0 .171 .295 .069 .146 .129 .001 .127 .131 .145 .129 .00 
float-benchs/nan_double_range_true-unreach-call.c 4.85 2.87 218644480 1 .096 .00  .007 6.75 3.67 302538752 1 .208 .526 .00  .034 4.79 2.88 230084608 .036 .129 .051 .026 .006 .046 .013 .026 .006 .00  5.14 2.98 215941120 0 .036 .155 .078 .025 .008 .00  .046 .010 .024 .008 .00 
float-benchs/nan_float_range_true-unreach-call.c 5.01 2.94 222793728 1 .098 .00  .014 6.97 3.87 313245696 1 .151 .517 .00  .016 5.37 3.15 225386496 .044 .163 .074 .033 .010 .052 .016 .031 .010 .00  4.79 2.81 216809472 0 .039 .152 .065 .028 .011 .00  .061 .013 .026 .011 .00 
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 5.49 3.15 218492928 1 .042 14.4  7.57 367181824 1 3.62  .011 5.37 3.08 225558528 .002 .026 .018 .00  .00  5.04 2.93 213540864 0 .005 .033 .017 .00  .00  .00 
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 5.46 3.21 219279360 1 .042 15.8  8.41 420708352 1 4.67  .005 5.13 2.93 222949376 .004 .049 .030 .001 .00  5.35 3.10 213737472 0 .004 .033 .012 .00  .00  .00 
float-benchs/sin_interpolated_index_true-unreach-call.c 168    164    472367104 1 1.01  1.78  185    173    637992960 1 1.19  .006 6.23  5.63 3.36 250118144 .014 .099 .054 .002 .00  .276 .001 .00  .00  5.64 3.35 239382528 0 .020 .116 .064 .004 .00  .001 .290 .001 .00  .00 
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 5.47 3.10 223358976 1 .042 30.0  15.4  747769856 1 11.1   .006 5.15 3.00 219160576 .003 .019 .011 .00  .00  5.56 3.20 211124224 0 .003 .042 .017 .00  .00  .001
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c 42.4  30.1  771203072 1 3.23  .265 104    52.6  1623707648 1 9.61  .005 6.36  24.4  16.2  724299776 3.93  5.96  1.13  3.82  2.89  .951 2.99  3.80  2.88  .015 25.0  16.4  700706816 0 3.75  5.40  .754 3.58  2.64  .013 1.72  2.72  3.56  2.63  .015
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c 23.4  13.8  481185792 1 2.30  .156 79.2  40.1  1111945216 1 5.53  .005 3.79  14.6  8.79 454475776 2.13  3.07  .478 2.04  1.48  1.15  1.53  2.03  1.45  .028 14.3  8.58 432635904 1 2.13  3.49  .883 2.05  1.47  .034 1 .562 1.49  2.03  1.44  .016
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c 33.3  22.8  650575872 1 3.03  .462 115    58.2  2506530816 1 7.44  22.6   3.99  19.4  12.7  586756096 3.07  4.17  .536 2.97  2.22  1.19  2.30  2.96  2.18  .043 17.9  11.8  561319936 1 2.74  4.17  .903 2.66  2.01  .034 1 .745 2.04  2.65  1.97  .024
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c 11.9  6.72 398680064 1 1.60  .089 37.9  19.4  822841344 1 2.78  2.83  2.07  11.3  6.48 417042432 1.05  1.77  .358 .955 .584 .741 .614 .930 .579 .005 11.8  6.65 403079168 0 1.56  2.37  .421 1.50  .584 .006 .371 .625 1.45  .579 .005
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 17.9  9.59 546557952 1 3.10  .00  .253 54.7  27.8  991076352 1 10.8   .005 .029 4.78  18.0  10.7  479371264 4.55  6.57  1.18  4.41  3.33  .074 3.41  4.38  3.33  .00  18.3  10.8  477462528 0 4.61  6.33  .827 4.46  3.35  .011 .516 3.44  4.44  3.35  .00 
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 913    891    9991610368 38.0  19.5  913899520 1 5.80  3.32  .106 3.71  .764 .507 14.9  9.16 436019200 3.99  5.05  .505 3.90  2.99  .459 3.04  3.88  2.99  .00  14.8  9.05 421445632 0 4.42  5.48  .486 4.35  2.98  .009 .066 3.02  4.33  2.98  .00 
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 11.6  6.30 380514304 1 1.94  .001 .106 33.5  17.4  766300160 1 5.45  2.60  .001 3.15  12.5  7.15 418922496 2.23  3.15  .423 2.12  1.52  .519 1.61  2.11  1.50  .024 12.3  7.02 367136768 1 2.02  3.43  .921 1.92  1.39  .030 1 .130 1.42  1.91  1.37  .013
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 14.0  7.60 462000128 1 2.64  .00  .213 38.7  19.9  912932864 1 7.00  .017 .016 3.66  13.8  8.12 429293568 2.78  4.25  .472 2.68  2.01  .130 2.06  2.66  1.99  .023 14.0  8.24 411582464 1 3.12  4.28  .492 3.03  2.01  .040 1 .146 2.05  3.02  1.99  .012
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 8.54 4.69 310308864 1 1.21  .00  .017 13.7  7.30 414846976 1 2.22  1.10  .00  .144 8.80 4.87 338071552 .964 1.45  .234 .916 .255 .050 .285 .908 .255 .00  8.49 4.70 307412992 0 .477 1.03  .250 .430 .249 .001 .048 .281 .415 .249 .00 
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 10.1  5.46 342568960 1 1.41  .00  .041 19.2  10.1  466276352 1 3.48  1.50  .00  .886 10.4  5.72 370737152 .934 1.80  .472 .845 .538 .457 .575 .838 .538 .00  10.3  5.62 335675392 0 1.34  2.19  .450 1.22  .910 .011 .065 .927 1.20  .910 .00 
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 13.8  7.91 424247296 6 1.89  .310 .352 53.1  27.0  982220800 6 2.53  7.29  1.30  .394 8.29  4.01  16.3  9.42 464396288 2.69  4.14  .567 2.48  1.50  .978 2.12  2.42  .539 .962 14.6  8.93 425091072 15 .966 3.28  .556 .366 .325 1.14  0 1.03  .262 .347 .217 .035
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 13.9  7.90 439037952 6 1.98  .312 .190 50.8  25.8  1005252608 6 2.58  6.42  1.17  .272 6.91  4.66  15.1  8.71 471441408 1.22  2.92  .743 1.09  .769 1.15  .833 1.06  .393 .376 14.8  9.02 448675840 15 .475 3.48  1.05  .363 .318 1.32  0 1.04  .263 .349 .219 .039
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 14.6  8.40 426766336 6 2.10  .336 .348 53.9  27.4  992587776 6 2.37  7.42  1.43  .246 7.28  4.91  17.9  10.4  477908992 2.06  3.86  .708 1.79  1.28  1.66  1.37  1.75  .726 .551 15.8  9.87 441548800 15 .559 4.05  .651 .456 .381 1.71  0 1.20  .336 .441 .288 .043
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 13.6  7.69 428863488 6 1.99  .307 .190 48.6  24.7  1026678784 6 2.40  6.31  1.36  .387 6.75  3.81  15.1  8.79 461643776 1.15  2.76  .559 1.00  .683 1.41  .717 .973 .449 .234 14.6  9.10 432029696 15 .466 3.50  1.09  .362 .287 1.27  0 1.05  .238 .333 .204 .029
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 8.82 4.91 356548608 1 .800 .026 23.5  12.3  580366336 1 1.38  2.26  .184 9.24 5.18 395714560 .069 .584 .260 .009 .00  .774 .004 .00  .00  9.07 5.08 356937728 0 .069 .566 .234 .012 .00  .004 .772 .001 .00  .00 
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 22.4  15.4  524906496 7 2.78  .560 .840 86.3  43.6  1448988672 7 3.78  .004 2.69  1.78  8.13  7.45  227    210    1095458816 191     197     2.65  191     184     2.19  190     191     3.46  181     25.6  18.5  543289344 21 1.39  6.04  .893 1.29  1.22  2.46  0 2.27  .983 1.26  .762 .212
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 21.3  14.5  507088896 6 2.83  .330 .699 92.2  46.6  1435205632 6 5.46  .005 2.46  1.90  8.33  7.09  168    152    1060360192 134     141     3.12  133     128     1.48  132     133     4.00  124     24.0  17.2  532295680 15 1.20  5.23  1.37  1.02  .904 1.75  0 1.88  .783 .987 .604 .171
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 13.5  8.03 412520448 4 1.78  .115 .157 58.4  29.7  1006034944 4 3.45  6.64  1.14  .672 6.90  3.72  18.9  11.3  471179264 2.62  4.70  .808 2.44  1.96  1.16  2.03  2.39  .781 1.17  14.0  8.70 422690816 6 .893 2.94  .957 .776 .610 .442 0 .868 .588 .761 .378 .197
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 8.98 4.95 356311040 2 .838 .028 .030 28.5  14.6  632733696 2 1.49  2.28  .235 .106 3.89  .646 13.6  7.60 436658176 1.25  3.33  1.03  1.06  .709 .435 .762 1.03  .498 .211 11.6  6.50 386019328 3 .404 2.29  .684 .316 .224 .193 0 .529 .221 .305 .170 .048
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 11.6  6.55 397807616 4 1.64  .189 .059 45.3  23.0  899452928 4 3.80  4.50  .864 .381 5.99  3.15  13.2  7.61 440156160 .922 2.55  .908 .768 .424 .668 .464 .751 .345 .079 12.1  7.09 412397568 6 .824 2.35  .540 .746 .222 .461 0 .633 .227 .730 .179 .028
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 11.6  6.54 394039296 4 1.77  .113 .048 45.3  23.1  879964160 4 2.88  4.67  1.06  .181 6.70  4.05  12.8  7.38 441872384 1.04  2.55  .579 .922 .592 .757 .644 .855 .309 .283 11.6  6.75 420716544 6 .760 2.08  .410 .661 .149 .400 0 .703 .141 .646 .124 .014
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 8.68 4.87 337309696 1 .854 .016 23.0  12.0  564420608 1 1.32  .006 .068 7.56 4.29 357761024 .039 .296 .163 .009 .00  .499 .001 .00  .00  7.90 4.44 329994240 0 .034 .291 .163 .004 .00  .00  .142 .001 .00  .00 
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 22.0  14.6  496758784 15 3.42  3.92  2.80  49.7  25.3  962822144 7 3.19  7.11  2.20  .487 7.44  6.13  88.1  75.1  880013312 65.5   68.6   1.10  65.1   57.9   2.86  63.4   65.1   2.48  55.4   50.8  41.6  565952512 106 1.04  29.6   1.46  .884 4.16  25.7   1 8.59  .674 .861 .580 .087
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 22.3  14.8  509456384 15 3.63  4.05  2.69  50.0  25.5  989167616 7 2.59  7.26  1.90  .536 7.13  7.82  36.3  24.6  626692096 16.6   19.8   1.29  16.3   14.2   .975 15.1   16.3   1.40  12.8   54.2  44.2  565907456 106 1.08  32.5   .998 .937 3.78  28.6   1 8.36  .691 .904 .583 .104
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 25.1  17.5  589590528 15 3.84  5.30  3.69  56.6  28.8  1068466176 7 2.70  .005 2.48  .595 8.78  8.57  33.5  22.2  662732800 13.3   16.6   1.25  13.1   11.3   2.04  12.0   13.0   2.09  9.17  63.3  52.4  601137152 106 1.36  38.0   1.07  1.20  4.40  33.6   1 10.9   .961 1.17  .812 .133
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 22.0  14.8  498970624 15 3.47  4.12  2.84  46.9  23.8  1015021568 7 2.94  .005 1.98  .497 7.50  5.62  45.5  32.8  795271168 23.7   27.3   1.49  23.3   20.4   1.86  22.2   23.2   1.77  18.6   52.5  43.4  525103104 106 1.14  32.1   1.00  1.01  3.75  28.1   1 7.88  .787 .990 .667 .099
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 906    889    3821019136 70 9.83  386     463     44.2  22.5  893550592 4 3.47  4.34  1.48  .234 6.75  4.61  38.6  25.8  816431104 14.9   20.5   2.50  14.5   12.5   1.49  13.1   14.4   3.02  9.48  267    253    1111613440 266 2.34  203     1.53  1.73  23.6   196     1 46.3   1.38  1.70  1.19  .185
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 909    889    5323636736 256 9.85  695     133     11.7  6.28 383250432 2 .290 .006 .006 .00  1.46  .155 19.9  10.6  449691648 3.46  6.92  1.37  3.13  1.74  .259 2.08  3.07  1.08  .656 376    361    2209509376 1087 2.03  200     .931 1.86  78.9   196     1 158     1.50  1.82  1.30  .160
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 913    898    11869798400 8.47 4.63 321437696 1 .261 .012 .003 .00  7.40 4.16 334725120 .351 .777 .176 .274 .097 .083 .129 .264 .074 .023 6.65 3.79 235266048 9 .171 .660 .175 .113 .105 .155 1 .134 .065 .105 .047 .011
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 906    886    3485147136 72 9.79  370     478     52.3  26.6  986558464 6 3.72  .008 2.40  .665 8.43  5.79  58.6  43.4  982581248 26.8   34.1   3.27  26.4   22.2   5.08  24.1   26.3   4.48  17.7   417    403    1073676288 222 1.67  362     1.39  1.48  23.0   355     1 37.6   1.11  1.44  .948 .147
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 905    885    3520495616 72 9.92  368     478     53.4  27.2  1391304704 6 3.58  7.33  2.49  .638 7.88  6.39