sat_decide used to have an optimization such that it would only generate a proof term during reflection if the terms where not already defeq. This can enable a drastic reuse of proof term size and thus faster type checking on enormous proof goals.
We should add this to bv_decide of goal size becomes an issue again.
sat_decideused to have an optimization such that it would only generate a proof term during reflection if the terms where not already defeq. This can enable a drastic reuse of proof term size and thus faster type checking on enormous proof goals.We should add this to
bv_decideof goal size becomes an issue again.