"Another thing that we need to re-implement in dReal3 is the ordering of ODE pruning operators. For now, it always applies forward ODE pruning first and then backward ODE pruning later. In dReal2, we compare the widths of X_0 and X_t and decide what to apply first. Note that this is analogous to decision heuristics in SAT solving."