-
Andrei Paskevich authored
we still keep bv_vars in the binders, so calculating the set of free variables only has to descend to the topmost binders. The difference on an example from BWare is quite striking: /usr/bin/time why3-replayer : with t_vars 505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k /usr/bin/time why3-replayer : without t_vars 242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k Not only we take 2/3 of memory, but we also gain in speed (less work for the GC, most probably). This patch should be tested on big WhyML examples, since src/whyml/mlw_*.ml are big users of t_vars. Thanks to Guillaume for the suggestion.
7abeba05