+let num_call_over_max_fixpoint = ref 0
+let num_miss_over_max_fixpoint = ref 0
+let () = at_exit(fun () -> Format.fprintf Format.err_formatter
+ "For bu_over_max: call %d, miss: %d\n%!" (!num_call_over_max_fixpoint)
+ (!num_miss_over_max_fixpoint))
+
+